Abstract
In this paper, we introduce a Foundational Proof-Carrying Code (FPCC) framework for constructing certified code packages from typed assembly language that will interface with a similarly certified runtime system. Our framework permits the typed assembly language to have a “foreign function” interface, in which stubs, initially provided when the program is being written, are eventually compiled and linked to code that may have been written in a language with a different type system, or even certified directly in the FPCC logic using a proof assistant. We have increased the potential scalability and flexibility of our FPCC system by providing a way to integrate programs compiled from different source type systems. In the process, we are explicitly manipulating the interface between Hoare logic and a syntactic type system.
This research is based on work supported in part by DARPA OASIS grant F30602-99-1-0519, NSF grant CCR-9901011, NSF ITR grant CCR-0081590, and NSF grant CCR-0208618. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ahmed, A., Appel, A.W., Virga, R.: A stratified semantics of general references embeddable in higher-order logic. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science, June 2002, pp. 75–86 (2002)
Ahmed, A.J.: Mutable fields in a semantic model of types. In: Talk presented at 2000 PCC Workshop (June 2000)
Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th Annual IEEE Symposium on Logic in Computer Science, June 2001, pp. 247–258 (2001)
Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proofcarrying code. In: Proc. 27th ACM Symp. on Principles of Prog. Lang., pp. 243–253. ACM Press, New York (2000)
Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proofcarrying code. ACM Trans. on Programming Languages and Systems 23(5), 657–683 (2001)
Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound tal for back-end optimization. In: Proc. 2003 ACM Conf. on Prog. Lang. Design and Impl., pp. 208–219. ACM Press, New York (2003)
Colby, C., Lee, P., Necula, G., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pp. 95–107. ACM Press, New York (2000)
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76, 95–120 (1988)
Crary, K.: Towards a foundational typed assembly language. In: Proc. 30th ACM Symp. on Principles of Prog. Lang., January 2003, pp. 198–212. ACM Press, New York (2003)
Crary, K., Sarkar, S.: A metalogical approach to foundational certified code. Technical Report CMU-CS-03-108, Carnegie Mellon University (January 2003)
Felty, A.: Semantic models of types and machine instructions for proof-carrying code. Talk presented at 2000 PCC Workshop (June 2000)
Hamid, N.A., Shao, Z.: Coq code for interfacing hoare logic and type systems for fpcc, Available at flint.cs.yale.edu/flint/publications (May 2004)
Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof carrying-code. Journal of Automated Reasoning, Special issue on Proof- Carrying Code (to appear)
Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof carrying-code. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science, June 2002, pp. 89–100 (2002)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. In: Proc. 25th ACM Symp. on Principles of Prog. Lang., January 1998, pp. 85–97. ACM Press, New York (1998)
Necula, G.: Proof-carrying code. In: Proc. 24th ACM Symp. on Principles of Prog. Lang., January 1997, pp. 106–119. ACM Press, New York (1997)
Necula, G.: Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ. (September 1998)
Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: Proc. 2nd USENIX Symp. on Operating System Design and Impl., pp. 229–243 (1996)
Necula, G.C., Schneck, R.R.: A sound framework for untrustred verification-condition generators. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science, June 2003, pp. 248–260 (2003)
Paulin-Mohring, C.: Inductive definitions in the system Coq—rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, Springer, Heidelberg (1993)
Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Swadi, K.N., Appel, A.W.: Typed machine language and its semantics, Unpublished manuscript available at www.cs.princeton.edu/~appel/papers (July 2001)
Tan, G., Appel, A.W., Swadi, K.N., Wu, D.: Construction of a semantic model for a typed assembly language. In: 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2004) (January 2004) (to appear)
The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1 (October 2001)
Werner, B.: Une Théorie des Constructions Inductives. PhD thesis, A L’Université Paris 7, Paris, France (1994)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: Dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363–379. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamid, N.A., Shao, Z. (2004). Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive