Andrew W. Appel
David McAllester
Abstract
The proofs of "traditional" proof carrying code (PCC) are type-specialized in the sense that they require axioms about a specific type system. In contrast, the proofs of foundational PCC explicitly define all required types and explicitly prove all the required properties of those types assuming only a fixed foundation of mathematics such as higher-order logic. Foundational PCC is both more flexible and more secure than type-specialized PCC.For foundational PCC we need semantic models of type systems on von Neumann machines. Previous models have been either too weak (lacking general recursive types and first-class function-pointers), too complex (requiring machine-checkable proofs of large bodies of computability theory), or not obviously applicable to von Neumann machines. Our new model is strong, simple, and works either in λ-calculus or on Pentiums.
- APPEL,A.W.AND FELTEN, E. W. 2001. Models for security policies in proof-carrying code. Tech. Rep. TR-636-01, Computer Science, Princeton University.]]Google Scholar
- APPEL,A.W.AND FELTY, A. P. 2000. A semantic model of types and machine instructions for proof-carrying code. In POPL '00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 243-253.]] Google Scholar
- BIRKEDAL,L.AND HARPER, R. 1997. Relational interpretations of recursive types in an operational setting. In Theoretical Aspects of Computer Software. Springer-Verlag, Berlin.]] Google Scholar
- COLBY, C., LEE, P., NECULA,G.C.,BLAU, F., CLINE, K., AND PLESKO, M. 2000. A certifying compiler for Java. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '00). ACM Press, New York, NY.]] Google Scholar
- CONSTABLE, R. L., ALLEN,S.F.,BROMLEY, H. M., CLEAVELAND, W. R., CREMER,J.F.,HARPER,R.W., HOWE,D.J.,KNOBLOCK,T.B.,MENDLER,N.P.,PANANGADEN, P., SASAKI,J.T.,AND SMITH, S. F. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ.]] Google Scholar
- HARPER, R., HONSELL,F.,AND PLOTKIN, G. 1993. A framework for defining logics. J. ACM 40,1 (Jan.), 143-184.]] Google Scholar
- MACQUEEN, D., PLOTKIN,G.,AND SETHI, R. 1986. An ideal model for recursive polymophic types. Information and Computation 71, 1/2, 95-130.]] Google Scholar
- MICHAEL,N.G.AND APPEL, A. W. 2000. Machine instruction syntax and semantics in higher-order logic. In 17th International Conference on Automated Deduction. Springer-Verlag, Berlin. LNAI 1831.]] Google Scholar
- MILNER, R. 1977. Fully abstract models of typed -calculi. Theoretical Computer Science 4, 1-22.]]Google Scholar
- MINAMIDE, Y., MORRISETT,G.,AND HARPER, R. 1996. Typed closure conversion. In POPL '96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 271-283.]] Google Scholar
- MITCHELL,J.C.AND VISWANATHAN, R. 1996. Effective models of polymorphism, subtyping and recursion. In 23rd International Colloquium on Automata, Languages, and Programming. Springer-Verlag, Berlin.]] Google Scholar
- MORRISETT, G., CRARY, K., GLEW,N.,AND WALKER, D. 1998a. Stack-based typed assembly language. In ACM Workshop on Types in Compilation. Springer-Verlag, Berlin. LNCS 1473.]] Google Scholar
- MORRISETT, G., WALKER, D., CRARY, K., AND GLEW, N. 1998b. From System F to typed assembly language. In POPL '98: 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Pro-gramming Languages. ACM Press, New York NY, 85-97.]] Google Scholar
- NECULA, G. 1997. Proof-carrying code. In 24th ACMSIGPLAN-SIGACTSymposium on Principles of Programming Languages. ACM Press, New York, NY, 106-119.]] Google Scholar
- NECULA, G. C. 1998. Compiling with proofs. Ph.D. dissertation, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA.]] Google Scholar
- PFENNING, F. 1994. Elf: A meta-language for deductive systems. In Proceedings of the 12th Inter-national Conference on Automated Deduction, A. Bundy, Ed. Springer-Verlag LNAI 814, Nancy, France, 811-815.]] Google Scholar
- PFENNING,F.AND SCHURMANN, C. 1999. System description: Twelf-a meta-logical framework for deductive systems. In The 16th International Conference on Automated Deduction. Springer-Verlag, Berlin.]] Google Scholar
- PITTS, A. M. 1996. Relational properties of domains. Information and Computation 127, 2, 66-90.]]Google Scholar
- SCHMIDT, D. A. 1986. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Boston, MA.]] Google Scholar
- SCOTT, D. S. 1976. Data types as lattices. SIAM J. Comput. 5, 3, 522-87.]]Google Scholar
- WINSKEL, G. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA.]] Google Scholar
Index Terms
- An indexed model of recursive types for foundational proof-carrying code
Recommendations
A Syntactic Approach to Foundational Proof-Carrying Code
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; they certify safety but only if there is no bug in ...
A Syntactic Approach to Foundational Proof-Carrying Code
LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer ScienceProof-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 ...
Comments