Workshop on Foundations of Computer Security - FCS'03
 Ottawa, Canada, 26-27 June 2003

An Implementation of Abstraction-carrying Code

Songtao Xia and James Hook (OGI - USA)

Abstract

Abstraction-carrying code (ACC) provides a mechanism to certify temporal properties of mobile programs. This certification has many potential applications, including high confidence extension of an operating system kernel. The size of a traditional, proof-based certificate tends to expand drastically because of the state explosion problem. In ACC, we use an abstract interpretation of the mobile program as a certificate. A client receiving the code and the certificate will first validate the abstraction and then run a model checker to verify the temporal property. The size of a typical certificate for a non-trivial temporal property is usually significantly smaller than the size of the program.

We have developed ACCEPT, a prototype certifier for programs whose properties can be expressed as LTL formulas which do not use the next-operator. ACCEPT produces certificates for assembly programs; but it also assumes access to the higher level language source code as well. Several novel aspects of ACCEPT are: 1) the certifier produces a predicate abstraction which is used as a certificate; 2) the abstraction is valid for the source level program and the compiler maintains this validity for the assembly level program; 3) an index-typed assembly language SDTAL is adopted to encode the certificate; and 4) the abstraction is validated by type-checking the SDTAL program. This paper focuses on the representation of a predicate abstraction as type annotations on the assembly level program. The soundness of SDTAL's type system guarantees the soundness of the abstraction validation. We also report on our initial experience with ACCEPT.

Iliano Cervesato