Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code

• Autorzy: Felty A.P.
• Języki publikacji: EN

Abstrakty

EN

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 two running examples. The examples, 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.

Słowa kluczowe

EN

proof-carrying code; encoding machine semantics directly

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 303--330
• Opis fizyczny: bibliogr. 21 poz.

Twórcy

autor

Felty A.P.

• SITE, University of Ottawa, 800 King Edward Ave., Ottawa, Ontario, Canada KIN 6N5,

Bibliografia

• [1] Ahmed, A. J., Appel, A.W., Virga, R.: A Stratified Semantics of General References Embeddable in Higher-Order Logic, Proc. Seventeenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 2002.
• [2] Appel, A. W., Felty, A. P.: A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, Proc. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 2000.
• [3] Appel, A.W., McAllester, D.: An IndexedModel of Recursive Types for Foundational Proof-Carrying Code, ACM Transactions on Programming Languages and Systems, 13(5), September 2001, 657-683.
• [4] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, Springer, 2004.
• [5] Chang, B.-Y. E., Chlipala, A., Necula, G. C., Schneck, R. R.: The Open Verifier Framework for Foundational Verifiers, Proc. ACM SIGPLAN International Workshop on Types in Language Design and Implementation, ACM Press, 2005.
• [6] Coq Development Team, LogiCal Project: The Coq Proof Assistant Reference Manual: Version 8.0, Technical report, INRIA, 2006.
• [7] Crary, K.: Toward a Foundational Typed Assembly Language, Proc. 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 2003.
• [8] Felty, A. P.: A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code, Proc. Sixteenth International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 3465, Springer-Verlag, 2005.
• [9] Hamid, N. A., Shao, Z.: Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code, Proc. Seventeenth International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 3223, Springer-Verlag, 2004.
• [10] Hamid, N. A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A Syntactic Approach to Foundational Proof-Carrying Code, Journal of Automated Reasoning, 31(3-4), November 2003, 191-229.
• [11] Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics, Journal of the ACM, 40(1), January 1993, 143-184.
• [12] Huth, M. R. A., Ryan, M. D.: Logic in Computer Science: Modelling and Reasoning about Systems, Second edition, Cambridge University Press, 2004.
• [13] Michael, N. G., Appel, A. W.: Machine Instruction Syntax and Semantics in Higher Order Logic, Proc. Seventeenth International Conference on Automated Deduction, Lecture Notes in Computer Science 1831, Springer-Verlag, 2000.
• [14] Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to Typed Assembly Language, ACM Transactions on Programming Languages and Systems, 21(3),May 1999, 527-568.
• [15] Nadathur, G., Miller, D.: An Overview of _Prolog, Proc. Fifth International Conference and Symposium on Logic Programming,MIT Press, 1988.
• [16] Nadathur, G., Mitchell, D. J.: System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of _Prolog, Proc. Sixteenth International Conference on Automated Deduction, Lecture Notes in Computer Science 1632, Springer-Verlag, 1999.
• [17] Necula, G.: Proof-carryingCode, Proc. 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 1997.
• [18] Necula, G. C.: Compiling with Proofs, Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, PA, 1998.
• [19] Necula, G. C., Lee, P.: Proof-Carrying Code, Technical Report CMU-CS-96-165, Carnegie Mellon University, November 1996.
• [20] Swadi, K. N.: Typed Machine Language, Ph.D. Thesis, Princeton University, Princeton, NJ, 2003.
• [21] Tan, G., Appel, A. W., Swadi, K. N., Wu, D.: Construction of a Semantic Model for a Typed Assembly Language, Proc. Fifth International Conference on Verification,Model Checking and Abstract Interpretation, Lecture Notes in Computer Science 2937, Springer-Verlag, 2004.