article

Certified assembly programming with embedded code pointers

Authors:

Zhong ShaoAuthors Info & Claims

ACM SIGPLAN Notices, Volume 41, Issue 1

Pages 320 - 333

https://doi.org/10.1145/1111320.1111066

Published: 11 January 2006 Publication History

Abstract

Embedded code pointers (ECPs) are stored handles of functions and continuations commonly seen in low-level binaries as well as functional or higher-order programs. ECPs are known to be very hard to support well in Hoare-logic style verification systems. As a result, existing proof-carrying code (PCC) systems have to either sacrifice the expressiveness or the modularity of program specifications, or resort to construction of complex semantic models. In Reynolds's LICS'02 paper, supporting ECPs is listed as one of the main open problems for separation logic.In this paper we present a simple and general technique for solving the ECP problem for Hoare-logic-based PCC systems. By adding a small amount of syntax to the assertion language, we show how to combine semantic consequence relation with syntactic proof techniques. The result is a new powerful framework that can perform modular reasoning on ECPs while still retaining the expressiveness of Hoare logic. We show how to use our techniques to support polymorphism, closures, and other language extensions and how to solve the ECP problem for separation logic. Our system is fully mechanized. We give its complete soundness proof and a full verification of Reynolds's CPS-style "list-append" example in the Coq proof assistant.

References

[1]

A. Ahmed, L. Jia, and D. Walker. Reasoning about hierarchical storage. In Proc. 18th IEEE Symposium on Logic in Computer Science, pages 33--44, June 2003.

Digital Library

[2]

A. Ahmed and D. Walker. The logical approach to stack typing. In Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 74--85. ACM Press, 2003.

Digital Library

[3]

A. J. Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004.

Digital Library

[4]

A. W. Appel. Foundational proof-carrying code. In Proc. 16th Annual IEEE Symposium on Logic in Computer Science, pages 247--258, June 2001.

Digital Library

[5]

A. W. Appel and A. P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Proc. 27th ACM Symposium on Principles of Programming Languages, pages 243--253, Jan. 2000.

Digital Library

[6]

A. W. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems, 23(5):657--683, Sept. 2001.

Digital Library

[7]

M. Berger, K. Honda, and N. Yoshida. A logical analysis of aliasing in imperative higher-order functions. In Proc. 10th ACM SIGPLAN International Conference on Functional Programming, pages 280--293, Sept. 2005.

Digital Library

[8]

R. S. Boyer and Y. Yu. Automated proofs of object code for a widely used microprocessor. J. ACM, 43(1):166--192, 1996.

Digital Library

[9]

B.-Y. E. Chang, G. C. Necular, and R. R. Schneck. Extensible code verification. Unpublished manuscript, 2003.

[10]

J. Chen, D. Wu, A. W. Appel, and H. Fang. A provably sound tal for back-end optimization. In Proc. 2003 ACM Conference on Programming Language Design and Implementation, pages 208--219. ACM Press, 2003.

Digital Library

[11]

C. Colby, P. Lee, G. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for Java. In Proc. 2000 ACM Conference on Programming Language Design and Implementation, pages 95--107, New York, 2000. ACM Press.

Digital Library

[12]

K. Crary. Toward a foundational typed assembly language. In Proc. 30th ACM Symposium on Principles of Programming Languages, page 198, Jan. 2003.

Digital Library

[13]

K. Crary and J. C. Vanderwaart. An expressive, scalable type theory for certified code. In Proc. 7th ACM SIGPLAN International Conference on Functional Programming, pages 191--205, 2002.

Digital Library

[14]

N. G. de Bruijn. Lambda calculus notation with nameless dummies. Indagationes Mathematicae, 34:381--392, 1972.

[15]

X. Feng and Z. Shao. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. 2005 International Conference on Functional Programming, pages 254--267, Sept. 2005.

Digital Library

[16]

R. W. Floyd. Assigning meaning to programs. Communications of the ACM, Oct. 1967.

[17]

M. Gordon. A mechanized Hoare logic of state transitions. In A. W. Roscoe, editor, A Classical Mind--Essays in Honour of C.A.R. Hoare, pages 143--160. Prentice Hall, 1994.

Digital Library

[18]

J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.

Digital Library

[19]

N. A. Hamid and Z. Shao. Interfacing hoare logic and type systems for foundational proof-carrying code. In Proc. 17th International Conference on Theorem Proving in Higher Order Logics, volume 3223 of LNCS, pages 118--135. Springer-Verlag, Sept. 2004.

[20]

N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science, pages 89--100, July 2002.

Digital Library

[21]

H. Herbelin, F. Kirchner, B. Monate, and J. Narboux. Faq about coq. http://pauillac.inria.fr/coq/doc/faq.html#htoc38.

[22]

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, Oct. 1969.

Digital Library

[23]

K. Honda and N. Yoshida. A compositional logic for polymorphic higher-order functions. In Proc. 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 191--202, Aug. 2004.

Digital Library

[24]

K. Honda, N. Yoshida, and M. Berger. An observationally complete program logic for imperative higher-order functions. In Proc. 20th IEEE Symposium on Logic in Computer Science, June 2005.

Digital Library

[25]

R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, Cambridge, Massachusetts, 1997.

Digital Library

[26]

Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proc. 23rd ACM Symposium on Principles of Programming Languages, pages 271--283. ACM Press, 1996.

Digital Library

[27]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symposium on Principles of Programming Languages, pages 85--97. ACM Press, Jan. 1998.

Digital Library

[28]

D. A. Naumann. Predicate transformer semantics of a higher-order imperative language with record subtyping. Science of Computer Programming, 41(1):1--51, 2001.

Digital Library

[29]

G. Necula. Proof-carrying code. In Proc. 24th ACM Symposium on Principles of Programming Languages, pages 106--119, New York, Jan. 1997. ACM Press.

Digital Library

[30]

G. Necula. Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ., Sept. 1998.

Digital Library

[31]

G. C. Necula and R. R. Schneck. A sound framework for untrustred verification-condition generators. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 248--260. IEEE Computer Society, July 2003.

Digital Library

[32]

Z. Ni and Z. Shao. Implementation for certified assembly programming with embedded code pointers. http://flint.cs.yale.edu/publications/xcap.html, Oct. 2005.

[33]

P. W. O'Hearn and R. D. Tennent. Algol-Like Languages. Birkhauser, Boston, 1997.

Digital Library

[34]

C. Paulin-Mohring. Inductive definitions in the system Coq--rules and properties. In M. Bezem and J. Groote, editors, Proc. TLCA, volume 664 of LNCS. Springer-Verlag, 1993.

Digital Library

[35]

F. Pfenning. Automated theorem proving. http://www-2.cs.cmu.edu/~fp/courses/atp/, Apr. 2004.

[36]

F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proc. 1988 ACM Conference on Programming Language Design and Implementation, pages 199--208. ACM Press, 1988.

Digital Library

[37]

J. Reynolds. Separation logic: a logic for shared mutable data structures. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science, 2002.

Digital Library

[38]

Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In Proc. 29th ACM Symposium on Principles of Programming Languages, pages 217--232. ACM Press, Jan. 2002.

Digital Library

[39]

G. Tan. A Compositional Logic for Control Flow and its Application in Foundational Proof-Carrying Code. PhD thesis, Princeton University, 2005.

Digital Library

[40]

The Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.0, Oct. 2005.

[41]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.

Digital Library

[42]

H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. 26th ACM Symposium on Principles of Programming Languages, pages 214--227. ACM Press, 1999.

Digital Library

[43]

D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 50(1-3):101--127, Mar. 2004.

Digital Library

[44]

D. Yu and Z. Shao. Verification of safety properties for concurrent assembly code. In Proc. 2004 International Conference on Functional Programming, Sept. 2004.

Digital Library

[45]

Y. Yu . Automated Proofs of Object Code For A Widely Used Microprocessor. PhD thesis, University of Texas at Austin, 1992.

Digital Library

Cited By

Rao XGeorges ALegoupil MWatt CPichon-Pharabod JGardner PBirkedal L(2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591265
Georges AGuéneau AVan Strydonck TTimany ATrieu AHuyghebaert SDevriese DBirkedal L(2021)Efficient and provable local capability revocation using uninitialized capabilitiesProceedings of the ACM on Programming Languages10.1145/34342875:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434287
Itzhaky SPeleg HPolikarpova NRowe RSergey I(2021)Deductive Synthesis of Programs with Pointers: Techniques, Challenges, OpportunitiesComputer Aided Verification10.1007/978-3-030-81685-8_5(110-134)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_5
Show More Cited By

Index Terms

Certified assembly programming with embedded code pointers
1. Software and its engineering
2. Theory of computation

Recommendations

Certified assembly programming with embedded code pointers
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Embedded code pointers (ECPs) are stored handles of functions and continuations commonly seen in low-level binaries as well as functional or higher-order programs. ECPs are known to be very hard to support well in Hoare-logic style verification systems. ...
From process logic to program logic
ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

We present a process logic for the p -calculus with the linear/affine type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding studies on logics for programs and processes, simple systems of assertions are developed, capturing the classes of ...
Inductive Completeness of Logics of Programs

We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 41, Issue 1

Proceedings of the 2006 POPL Conference

January 2006

421 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1111320

Issue’s Table of Contents

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2006
432 pages
ISBN:1595930272
DOI:10.1145/1111037
General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Published in SIGPLAN Volume 41, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

96
Total Citations
View Citations
572
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)3

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rao XGeorges ALegoupil MWatt CPichon-Pharabod JGardner PBirkedal L(2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591265
Georges AGuéneau AVan Strydonck TTimany ATrieu AHuyghebaert SDevriese DBirkedal L(2021)Efficient and provable local capability revocation using uninitialized capabilitiesProceedings of the ACM on Programming Languages10.1145/34342875:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434287
Itzhaky SPeleg HPolikarpova NRowe RSergey I(2021)Deductive Synthesis of Programs with Pointers: Techniques, Challenges, OpportunitiesComputer Aided Verification10.1007/978-3-030-81685-8_5(110-134)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_5
Zha JFeng XQiao L(2020)Modular Verification of SPARCv8 CodeJournal of Computer Science and Technology10.1007/s11390-020-0536-935:6(1382-1405)Online publication date: 30-Nov-2020
https://doi.org/10.1007/s11390-020-0536-9
Lundberg DGuanciale RLindner ADam M(2020)Hoare-Style Logic for Unstructured ProgramsSoftware Engineering and Formal Methods10.1007/978-3-030-58768-0_11(193-213)Online publication date: 8-Sep-2020
https://doi.org/10.1007/978-3-030-58768-0_11
Zha JFeng XQiao L(2018)Modular Verification of SPARCv8 CodeProgramming Languages and Systems10.1007/978-3-030-02768-1_14(245-263)Online publication date: 22-Oct-2018
https://doi.org/10.1007/978-3-030-02768-1_14
Fox AMyreen MTan YKumar RBertot YVafeiadis V(2017)Verified compilation of CakeML to multiple machine-code targetsProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs10.1145/3018610.3018621(125-137)Online publication date: 16-Jan-2017
https://dl.acm.org/doi/10.1145/3018610.3018621
Azevedo de Amorim ACollins NDeHon ADemange DHriţcu CPichardie DPierce BPollack RTolmach A(2016)A verified information-flow architectureJournal of Computer Security10.3233/JCS-1578424:6(689-734)Online publication date: 1-Dec-2016
https://doi.org/10.3233/JCS-15784
Shao ZLeroy XTiu A(2015)Clean-Slate Development of Certified OS KernelsProceedings of the 2015 Conference on Certified Programs and Proofs10.1145/2676724.2693180(95-96)Online publication date: 13-Jan-2015
https://dl.acm.org/doi/10.1145/2676724.2693180
Reus BCharlton NHorsfall B(2015)Symbolic Execution Proofs for Higher Order Store ProgramsJournal of Automated Reasoning10.1007/s10817-014-9319-854:3(199-284)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1007/s10817-014-9319-8
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents