A syntactic approach to foundational proof-carrying code
Proceedings - Symposium on Logic in Computer Science - Trang 89-100
Tóm tắt
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.
Từ khóa
#Logic #Safety #Computer science #Buildings #Assembly systems #Computer bugs #ProposalsTài liệu tham khảo
10.1007/BFb0037116
10.1145/238721.238781
10.1145/277650.277752
10.1145/263699.263712
necula, 1998, Compiling with proofs
morrisett, 1998, Stack-based typed assembly language, Proc 1998 International Workshop on Types in Compilation, 1473, 28
10.1145/268946.268954
league, 2002, Precision in practice A type-preserving Java compiler
michael, 2000, Machine instruction syntax and semantics in higher order logic, Proc 17th International Conference on Automated Deduction, 7
swadi, 2001, Typed machine language and its semantics
10.1145/503272.503293
2001, The Coq proof assistant reference manual The Coq release v7 1
werner, 1994, Une The?orie des Constructions Inductives
10.1006/inco.1994.1093
10.1145/507635.507657
10.1109/LICS.2001.932501
10.1109/LICS.2002.1029818
howard, 1980, The formulae-as-types notion of constructions, To H B Curry Essays on Computational Logic Lambda Calculus and Formalism
ahmed, 2000, Mutable fields in a semantic model of types, 2000 PCC Workshop
10.1016/0890-5401(88)90005-3
10.1145/349299.349315
10.1145/504709.504712
10.1145/325694.325727
10.1109/LICS.2002.1029819
felty, 2000, Semantic models of types and machine instructions for proof-carrying code, 2000 PCC Workshop