Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code

Last modified: Mon Oct 25 21:16:15 2004 GMT.

Authors

Abstract

In this paper, we introduce a Foundational Proof-Carrying Code (FPCC) framework for constructing certified code packages from typed assembly language that will interface with a similarly certified runtime system. Our framework permits the typed assembly language to have a ``foreign function'' interface, in which stubs, initially provided when the program is being written, are eventually compiled and linked to code that may have been written in a language with a different type system, or even certified directly in the FPCC logic using a proof assistant. We have increased the potential scalability and flexibility of our FPCC system by providing a way to integrate programs compiled from different source type systems. In the process, we are explicitly manipulating the interface between Hoare logic and a syntactic type system.

To our knowledge, this is the first account of combining such certification proofs from languages at different levels of abstraction. While type systems such as TAL facilitate reasoning about many programs, they are not sufficient for certifying the most low-level system libraries. Hoare logic-style reasoning, on the other hand, can handle low-level details very well but cannot account for embedded code pointers in data structures, a feature common to higher-order and object-oriented programming. We outline for the first time a way to allow both methods of verification to interact, gaining the advantages of both and circumventing their shortcomings.

Published

In Proc. 17th International Conference on the Applications of Higher Order Logic Theorem Proving (TPHOLs'04), Park City, Utah, September 2004. Lecture Notes in Computer Science Vol. 3223, pages 118-135. © 2004 Springer-Verlag.

PDF [264k]
Coq (v8.0) prototype code (tar.gz) [32k]

colophon