Abstract
We formalise a simple assembly language with procedures and a safety policy for arithmetic overflow in Isabelle/HOL. To verify individual programs we use a safety logic. Such a logic can be realised in Isabelle/HOL either as shallow or deep embedding. In a shallow embedding logical formulas are written as HOL predicates, whereas a deep embedding models formulas as a datatype. This paper presents and discusses both variants pointing out their specific strengths and weaknesses.
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.
References
VeryPCC project, http://isabelle.in.tum.de/verypcc/ (2003)
Appel, A.W.: Foundational proof-carrying code. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), June 2001, pp. 247–258 (2001)
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 (POPL 2000), January 2000, pp. 243–253 (2000)
Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 21–38. Springer, Heidelberg (2003)
Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, p. 24. Springer, Heidelberg (2002)
Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 38–52. Springer, Heidelberg (2000)
Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound tal for back-end optimization. In: Programming Languages Design and Implementation (PLDI), ACM Sigplan (2003)
Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proc. ACM SIGPLAN conf. Programming Language Design and Implementation, pp. 95–107 (2000)
Gerwin, K., Tobias, N.: A machine-checked model for a Java-like language, virtual machine and compiler. Research report, National ICT Australia, Sydney (2004)
Hamid, N., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: Proc. 17th IEEE Symp. Logic in Computer Science, July 2002, pp. 89–100 (2002)
Homeier, P.V., Martin, D.F.: Secure mechanical verification of mutually recursive procedures, pp. 1–19 (2003)
Klein, G.: Verified Java Bytecode Verification. PhD thesis, Institut für Informatik, Technische Universität München (2003)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. In: Proc. 25th ACM Symp. Principles of Programming Languages, pp. 85–97. ACM Press, New York (1998)
Necula, G.C.: Proof-carrying code. In: Proc. 24th ACM Symp. Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)
Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (1998)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
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
Wildmoser, M., Nipkow, T. (2004). Certifying Machine Code Safety: Shallow Versus Deep Embedding. 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_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive