Jonas B. Jensen
ABSTRACT
Separation logic is a powerful tool for reasoning about structured, imperative programs that manipulate pointers. However, its application to unstructured, lower-level languages such as assembly language or machine code remains challenging. In this paper we describe a separation logic tailored for this purpose that we have applied to x86 machine-code programs.
The logic is built from an assertion logic on machine states over which we construct a specification logic that encapsulates uses of frames and step indexing. The traditional notion of Hoare triple is not applicable directly to unstructured machine code, where code and data are mixed together and programs do not in general run to completion, so instead we adopt a continuation-passing style of specification with preconditions alone. Nevertheless, the range of primitives provided by the specification logic, which include a higher-order frame connective, a novel read-only frame connective, and a 'later' modality, support the definition of derived forms to support structured-programming-style reasoning for common cases, in which standard rules for Hoare triples are derived as lemmas. Furthermore, our encoding of scoped assembly-language labels lets us give definitions and proof rules for powerful assembly-language 'macros' such as while loops, conditionals and procedures.
We have applied the framework to a model of sequential x86 machine code built entirely within the Coq proof assistant, including tactic support based on computational reflection.
Supplemental Material
- R. Affeldt, D. Nowak, and K. Yamada. Certifying assembly with formal security proofs: the case of BBS. Sci. Comput. Prog., 77(10--11), 2012. Google Scholar
Digital Library
- A. W. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 2001. Google ScholarDigital Library
- A. W. Appel, P.-A. Melliès, C. D. Richards, and J. Vouillon. A very modal model of a modern, major, general type system. In Proceedings of POPL, 2007. Google ScholarDigital Library
- J. Bengtson, J. B. Jensen, and L. Birkedal. Charge! -- a framework for higher-order separation logic in Coq. In Proc. of ITP, 2012.Google Scholar
- N. Benton. A typed, compositional logic for a stack-based abstract machine. In APLAS, volume 3780 of LNCS, 2005. Google ScholarDigital Library
- N. Benton. Abstracting allocation: The new new thing. In Computer Science Logic (CSL 2006), volume 4207 of LNCS, 2006. Google ScholarDigital Library
- N. Benton and N. Tabareau. Compiling functional types to relational specifications for low level imperative code. In TLDI, 2009. Google ScholarDigital Library
- L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame rules. In Proc. of LICS, 2005. Google ScholarDigital Library
- L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. Logical Methods in Computer Science, 2006.Google ScholarCross Ref
- L. Birkedal and H. Yang. Relational parametricity and separation logic. Logical Methods in Computer Science, 2008.Google ScholarCross Ref
- F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin, and X. Shi. Designing a CPU model: from a pseudo-formal document to fast code. In 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO 2011), 2011.Google Scholar
- R. Bornat, C. Calcagno, P. W. O'Hearn, and M. J. Parkinson. Permission accounting in separation logic. In Proceedings of POPL, 2005. Google ScholarDigital Library
- R. M. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7, 1972.Google Scholar
- H. Cai, Z. Shao, and A. Vaynberg. Certified self-modifying code. In Proc. of PLDI, 2007. Google ScholarDigital Library
- C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. In Proc. of LICS, 2007. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Proc. of PLDI, 2011. Google ScholarDigital Library
- A. Chlipala. Certified Programming with Dependent Types. MIT Press, to appear.Google Scholar
- R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics, Providence, Rhode Island, 1967. AMS.Google Scholar
- A. C. J. Fox and M. O. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In 1st International Conference on Interactive Theorem Proving (ITP 2010), volume 6172 of LNCS, 2010. Google ScholarDigital Library
- G. Gonthier, A. Mahboubi, and E. Tassi. A small scale reflection extension for the Coq system. Technical Report 6455, INRIA, 2011.Google Scholar
- C. Hawblitzel and E. Petrank. Automated verification of practical garbage collectors. In POPL, 2009. Google ScholarDigital Library
- J. B. Jensen and L. Birkedal. Fictional separation logic. In Proc. of ESOP, volume 7211 of LNCS. Springer, 2012. Google ScholarDigital Library
- N. R. Krishnaswami. Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis, Carnegie Mellon University, 2012.Google Scholar
- J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics. AMS, 1967.Google Scholar
- J. Strother Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5, 1989. Google ScholarDigital Library
- G. Morrisett, G. Tan, J. Tassarotti, J.B. Tristan, and E. Gan. Rocksalt: Better, faster, stronger SFI for the x86. In 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2012). ACM, 2012. Google ScholarDigital Library
- G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3), 1999. Google ScholarDigital Library
- M. O. Myreen. Verified just-in-time compiler on x86. In Proc. of POPL, 2010. Google ScholarDigital Library
- M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. In Proc. of TACAS, 2007. Google ScholarDigital Library
- H. Nakano. A modality for recursion. In Proc. of LICS, 2000. Google ScholarDigital Library
- Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. of POPL, 2006. Google ScholarDigital Library
- P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In Proc. of POPL, 2004. Google ScholarDigital Library
- F. Pottier. Hiding local state in direct style: a higher-order anti-frame rule. In Proc. of LICS, 2008. Google ScholarDigital Library
- J. C. Reynolds. An introduction to specification logic. In Logics of Programs, 1983. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. of LICS, 2002. Google ScholarDigital Library
- A. Saabas and T. Uustalu. A compositional natural semantics and Hoare logic for low-level languages. Theor. Comput. Sci., 373(3), 2007. Google ScholarDigital Library
- M. Sozeau and N. Oury. First-class type classes. In Proc. of TPHOLs, 2008. Google ScholarDigital Library
- G. Tan and A. W. Appel. A compositional logic for control flow. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), 2006. Google ScholarDigital Library
- A. M. Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, 1949.Google Scholar
- X. Jiang W. Wang, Z. Shao and Y. Guo. A simple model for certifying assembly programs with first-class function pointers. In Proc. of TASE, 2011. Google ScholarDigital Library
- W. D. Young. A mechanically verified code generator. Journal of Automated Reasoning, 5, 1989. Google ScholarDigital Library
Index Terms
- High-level separation logic for low-level code
Recommendations
High-level separation logic for low-level code
POPL '13Separation logic is a powerful tool for reasoning about structured, imperative programs that manipulate pointers. However, its application to unstructured, lower-level languages such as assembly language or machine code remains challenging. In this ...
Interactive proofs in higher-order concurrent separation logic
POPL '17When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Comments