Certificate size reduction in Abstraction-Carrying Code
Elvira Albert, Puri Arenas, Germ\'an Puebla, Manuel Hermenegildo

TL;DR
This paper proposes a method to significantly reduce the size of certificates in Abstraction-Carrying Code by identifying the minimal information needed for validation, ensuring efficiency without sacrificing correctness.
Contribution
It introduces the concept of reduced certificates and provides a generic analysis algorithm to identify the essential abstraction subset for single-pass validation.
Findings
Certificates size is greatly reduced in practice.
The approach maintains correctness and completeness.
Implemented and benchmarked within the ciaopp system.
Abstract
Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct)…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Software Testing and Debugging Techniques
