Authors
Nadeem Abdul Hamid
Zhong Shao
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.