Xinyu Feng
Zhong Shao
ABSTRACT
Runtime stacks are critical components of any modern software--they are used to implement powerful control structures such as function call/return, stack cutting and unwinding, coroutines, and thread context switch. Stack operations, however, are very hard to reason about: there are no known formal specifications for certifying C-style setjmp/longjmp, stack cutting and unwinding, or weak continuations (in C--). In many proof-carrying code (PCC) systems, return code pointers and exception handlers are treated as general first-class functions (as in continuation-passing style) even though both should have more limited scopes.In this paper we show that stack-based control abstractions follow a much simpler pattern than general first-class code pointers. We present a simple but flexible Hoare-style framework for modular verification of assembly code with all kinds of stackbased control abstractions, including function call/return, tail call, setjmp/longjmp, weak continuation, stack cutting, stack unwinding, multi-return function call, coroutines, and thread context switch. Instead of presenting a specific logic for each control structure, we develop all reasoning systems as instances of a generic framework. This allows program modules and their proofs developed in different PCC systems to be linked together. Our system is fully mechanized. We give the complete soundness proof and a full verification of several examples in the Coq proof assistant.
- A. Ahmed and D. Walker. The logical approach to stack typing. In Proc. of the 2003 ACM SIGPLAN Int'l workshop on Types in Lang. Design and Impl., pages 74--85. ACM Press, 2003. Google Scholar
Digital Library
- A. W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992. Google ScholarDigital Library
- A. W. Appel. Foundational proof-carrying code. In Symp. on Logic in Comp. Sci. (LICS'01), pages 247--258. IEEE Comp. Soc., June 2001. Google ScholarDigital Library
- K. R. Apt. Ten years of Hoare's logic: A survey - part I. ACM Trans. on Programming Languages and Systems, 3(4):431--483, 1981. Google ScholarDigital Library
- N. Benton. A typed, compositional logic for a stack-based abstract machine. In Proc. Third Asian Symp. on Prog. Lang. and Sys., LNCS 3780, pages 364--380. Springer-Verlag, November 2005. Google ScholarDigital Library
- J. Berdine, P. O'hearn, U. Reddy, and H. Thielecke. Linear continuation-passing. Higher Order Symbol. Comput., 15(2-3):181--208, 2002. Google ScholarDigital Library
- D. Chase. Implementation of exception handling, Part I. The Journal of C Language Translation, 5(4):229--240, June 1994.Google Scholar
- W. D. Clinger. Proper tail recursion and space efficiency. In Proc. 1997 ACM Conf. on Prog. Lang. Design and Impl., pages 174--185, New York, 1997. ACM Press. Google ScholarDigital Library
- C. Colby, P. Lee, G. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for Java. In Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pages 95--107, New York, 2000. ACM Press. Google ScholarDigital Library
- M. E. Conway. Design of a separable transition-diagram compiler. Communications of the ACM, 6(7):396--408, July 1963. Google ScholarDigital Library
- K. Crary. Toward a foundational typed assembly language. Technical Report CMU-CS-02-196, Carnegie Mellon University, School of Computer Science, Dec. 2002.Google Scholar
- S. J. Drew, J. Gough, and J. Ledermann. Implementing zero overhead exception handling. Technical Report 95-12, Faculty of Information Technology, Queensland U. of Technology, Brisbane, Australia, 1995.Google Scholar
- X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. Technical Report YALEU/DCS/TR-1336 and Coq Implementation, Dept. of Computer Science, Yale University, New Haven, CT, Nov. 2005. http://flint.cs.yale.edu/publications/sbca.html.Google Scholar
- N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Proc. Seventeenth Annual IEEE Symposium on Logic In Computer Science (LICS'02), pages 89--100. IEEE Computer Society, July 2002. Google ScholarDigital Library
- D. R. Hanson. C Interface & Implementations. Add. Wesley, 1997.Google Scholar
- C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, Oct. 1969. Google ScholarDigital Library
- L. Jia, F. Spalding, D. Walker, and N. Glew. Certifying compilation for a language with stack allocation. In Proc. 20th IEEE Symposium on Logic in Computer Science, pages 407--416, June 2005. Google ScholarDigital Library
- C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 5(4):596--619, 1983. Google ScholarDigital Library
- C. B. Jones. Systematic software development using VDM. Prentice Hall International (UK) Ltd., 1986. Google ScholarDigital Library
- B. W. Kernighan and D. M. Ritchie. The C Programming Language (Second Edition). Prentice Hall, 1988. Google ScholarDigital Library
- L. Lamport. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 16(3):872--923, May 1994. Google ScholarDigital Library
- T. Lindholm and F. Yellin. The Java Virtual Machine Specification (Second Edition). Addison-Wesley, 1999. Google ScholarDigital Library
- G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In Proc. 1998 Int'l Workshop on Types in Compilation: LNCS Vol 1473, pages 28--52. Springer-Verlag, 1998. Google ScholarDigital Library
- G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Prog. Lang., pages 85--97. ACM Press, Jan. 1998. Google ScholarDigital Library
- D. A. Naumann. Predicate transformer semantics of a higher-order imperative language with record subtyping. Science of Computer Programming, 41(1):1--51, 2001. Google ScholarDigital Library
- G. Necula. Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ., Sept. 1998. Google ScholarDigital Library
- G. Necula and P. Lee. The design and implementation of a certifying compiler. In Proc. 1998 ACM Conf. on Prog. Lang. Design and Impl., pages 333--344, New York, 1998. Google ScholarDigital Library
- Z. Ni and Z. Shao. A translation from typed assembly languages to certified assembly programming. Technical report, Dept. of Computer Science, Yale Univ., New Haven, CT, Nov. 2005. http://flint.cs.yale.edu/flint/publications/talcap.html.Google Scholar
- Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. 33rd ACM Symp. on Principles of Prog. Lang., pages 320--333, Jan. 2006. Google ScholarDigital Library
- N. Ramsey and S. P. Jones. A single intermediate language that supports multiple implementations of exceptions. In Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pages 285--298, 2000. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science, pages 55--74. IEEE Computer Society, 2002. Google ScholarDigital Library
- O. Shivers and D. Fisher. Multi-return function call. In Proc. 2004 ACM SIGPLAN Int'l Conf. on Functional Prog., pages 79--89. ACM Press, Sept. 2004. Google ScholarDigital Library
- R. Stata and M. Abadi. A type system for java bytecode subroutines. In Proc. 25th ACM Symp. on Principles of Prog. Lang., pages 149--160. ACM Press, 1998. Google ScholarDigital Library
- G. L. Steele. Rabbit: a compiler for Scheme. Technical Report AI-TR-474, MIT, Cambridge, MA, 1978. Google ScholarDigital Library
- The Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.0, Oct. 2004.Google Scholar
- J. C. Vanderwaart and K. Crary. A typed interface for garbage collection. In Proc. 2003 ACM SIGPLAN International Workshop on Types in Language Design and Implementation, pages 109--122, 2003. Google ScholarDigital Library
- D. von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13):1173--1214, 2001.Google ScholarCross Ref
- A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994. Google ScholarDigital Library
- D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. In Proc. 2003 European Symposium on Programming, LNCS Vol. 2618, pages 363--379, 2003. Google ScholarDigital Library
- D. Yu and Z. Shao. Verification of safety properties for concurrent assembly code. In Proc. 2004 ACM SIGPLAN Int'l Conf. on Functional Prog., pages 175--188, September 2004. Google ScholarDigital Library
- Y. Yu. Automated Proofs of Object Code For A Widely Used Microprocessor. PhD thesis, University of Texas at Austin, 1992. Google ScholarDigital Library
Index Terms
- Modular verification of assembly code with stack-based control abstractions
Recommendations
Modular verification of assembly code with stack-based control abstractions
Proceedings of the 2006 PLDI ConferenceRuntime stacks are critical components of any modern software--they are used to implement powerful control structures such as function call/return, stack cutting and unwinding, coroutines, and thread context switch. Stack operations, however, are very ...
Modular Verification of SPARCv8 Code
AbstractInline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical ...
Certified assembly programming with embedded code pointers
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesEmbedded 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. ...
Comments