Authors
Nadeem Abdul Hamid
Zhong Shao
Valery Trifonov
Stefan Monnier
Zhaozhong Ni
Abstract
Proof-Carrying Code (PCC) is a general framework for verifying the
safety properties of machine-language programs. PCC proofs are usually
written in a logic extended with language-specific typing rules.
In Foundational Proof-Carrying Code (FPCC), on the other hand,
proofs are constructed and verified using strictly the foundations of
mathematical logic, with no type-specific axioms. FPCC is more flexible
and secure because it is not tied to any particular type system and it
has a smaller trusted base.
Foundational proofs, however, are much harder to construct. Previous
efforts on FPCC all required building sophisticated semantic models
for types. In this paper, we
present a syntactic approach to FPCC that avoids
the difficulties of previous work.
Under our new scheme, the foundational proof for a typed
machine program simply consists of the typing derivation plus the
formalized syntactic soundness proof for the underlying type system.
We give a translation from a typed assembly language into FPCC and
demonstrate the advantages of our new system via an implementation in
the Coq proof assistant.
Published
In
Proc. Seventeenth Annual
IEEE Symposium on Logic In Computer Science (LICS'02),
Copenhagen, Denmark, pages 89-100, July 2002. ©2002 IEEE.