# A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code

## Abstract

Proof-carrying code provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. Foundational proof-carrying code (FPCC) provides increased security and greater flexibility in the construction of proofs of safety. Proofs of safety are constructed from the smallest possible set of axioms and inference rules. For example, typing rules are not included. In our semantic approach to FPCC, we encode a semantics of types from first principles and the typing rules are proved as lemmas. In addition, we start from a semantic definition of machine instructions and safety is defined directly from this semantics. Since FPCC starts from basic axioms and low-level definitions, it is necessary to build up a library of lemmas and definitions so that reasoning about particular programs can be carried out at a higher level, and ideally, also be automated. We describe a high-level organization that involves Hoare-style reasoning about machine code programs. This organization is presented using a detailed example. The example, as well as illustrating the above mentioned approach to organizing proofs, is designed to provide a tutorial introduction to a variety of facets of our FPCC approach. For example, it illustrates how to prove safety of programs that traverse input data structures as well as allocate new ones.

## Keywords

Memory Location Proof Obligation Typing Rule Machine Instruction Semantic Approach## Preview

Unable to display preview. Download preview PDF.

## References

- 1.Ahmed, A.J., Appel, A.W., Virga, R.: A stratified semantics of general references embeddable in higher-order logic. In: Seventeenth Annual IEEE Symposium on Logic in Computer Science, July 2002, pp. 75–86 (2002)Google Scholar
- 2.Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 243–253 (2000)Google Scholar
- 3.Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 13(5), 657–683 (2001)CrossRefGoogle Scholar
- 4.Chang, B.-Y.E., Chlipala, A., Necula, G.C., Schneck, R.R.: The open verifier framework for foundational verifiers. In: ACM SIGPLAN Workshop on Types in Language Design and Implementation (January 2005)Google Scholar
- 5.Coq Development Team. The Coq Proof Assistant reference manual: Version 7.4. Technical report, INRIA (2003)Google Scholar
- 6.Crary, K., Sarkar, S.: Toward a foundational typed assembly language. In: Thirtieth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 198–212 (2003)Google Scholar
- 7.Hamid, N.A., Shao, Z.: Interfacing hoare logic and type systems for foundational proof-carrying code. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 118–135. Springer, Heidelberg (2004)CrossRefGoogle Scholar
- 8.Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code (extended version). Journal of Automated Reasoning 31(3-4), 191–229 (2003)zbMATHCrossRefGoogle Scholar
- 9.Michael, N.G., Appel, A.W.: Machine instruction syntax and semantics in higher order logic. In: Seventeenth International Conference on Automated Deduction, June 2000. LNCS, pp. 7–24. Springer, Heidelberg (2000)Google Scholar
- 10.Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems 21(3), 528–569 (1999)CrossRefGoogle Scholar
- 11.Nadathur, G., Miller, D.: An overview of
*λ*Prolog. In: Bowen, K., Kowalski, R. (eds.) Fifth International Conference and Symposium on Logic Programming, MIT Press, Cambridge (1988)Google Scholar - 12.Nadathur, G., Mitchell, D.J.: System description: Teyjus — a compiler and abstract machine based implementation of
*λ*Prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)CrossRefGoogle Scholar - 13.Necula, G.: Proof-carrying code. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1997, pp. 106–119. ACM Press, New York (1997)CrossRefGoogle Scholar
- 14.Swadi, K.N., Appel, A.W.: Foundational semantics for TAL syntactic rules via typed machine language (March 2002), http://www.cs.princeton.edu/kswadi/papers/tml.ps
- 15.Tan, G., Appel, A.W., Swadi, K.N., Wu, D.: Construction of a semantic model for a typed assembly language. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 30–43. Springer, Heidelberg (2004)CrossRefGoogle Scholar