Abstraction-based certification of temporal properties of software modules

When an untrusted program (termed a module in the dissertation) is executed on a host system, the correctness of the integrated system, in particular, the security, is of concern. Many security or correctness properties can be expressed in temporal logic. Certification of temporal properties provides a piece of evidence (termed a certificate in the dissertation) that helps the host system reverify a property of concern. Examples of the applications of such certification include extensions of an operating system kernel with API safety guarantees. Previous solutions, where certificates are primarily proofs, suffer from the problem that the sizes of the certificate do not scale as the programs become larger and the properties become more complicated.; We propose Abstraction-carrying code (ACC) as an alternative certification method to the traditional proof based approaches. ACC uses an abstract interpretation of the module as a certificate. Using abstraction methods from the software model checking community, we can compute an abstract model that demonstrates that a program satisfies a temporal property; the size of such an abstract model tends to scale well when the complexity of problem increases. A module will carry this abstraction 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.; We report our efforts in building the ACC Evaluation and Prototype Toolkit (ACCEPT). Two versions of ACCEPT, ACCEPT/While and ACCEPT/C, target a simple While language and C, respectively. Novel aspects of our work include: (1) the use of a Boolean program (BP), a useful abstraction of a program, as a certificate, (2) the simultaneous compilation of the source program and the BP to generate a BP for compiled code, (3) the encoding of the BP as index types, a powerful type system that can specify and check strong program properties, and (4) the semantics-based validation of the BP through index type checking.; We report our experience of applying ACCEPT to various programs, including Linux and NT drivers. Our investigation shows that ACC tools generate certificates that scale better compared to those generated by other techniques of similar expressive power and that the time spent on model checking is acceptable for supporting many applications.