Adam Chlipala
ABSTRACT
We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack.
- A. W. Appel. Verified software toolchain. In Proc. ESOP, volume 6602 of LNCS, pages 1--17. Springer-Verlag, 2011. Google Scholar
Digital Library
- N. Benton, J. B. Jensen, and A. Kennedy. High-level separation logic for low-level code. In Proc. POPL, pages 301--314. ACM, 2013. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. FMCO, volume 4111 of LNCS, pages 115--137. Springer-Verlag, 2005. Google ScholarDigital Library
- B. N. Bershad, S. Savage, P. Pardyak, E. G. Sirer, M. E. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility, safety and performance in the SPIN operating system. In Proc. SOSP, pages 267--283. ACM, 1995. Google ScholarDigital Library
- H. Cai, Z. Shao, and A. Vaynberg. Certified self-modifying code. In Proc. PLDI, pages 66--77. ACM, 2007. Google ScholarDigital Library
- C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. In Proc. POPL, pages 289--300. ACM, 2009. Google ScholarDigital Library
- B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In Proc. POPL, pages 247--260. ACM, 2008. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Proc. PLDI, pages 234--245. ACM, 2011. Google ScholarDigital Library
- R. Cox, T. Bergan, A. T. Clements, F. Kaashoek, and E. Kohler. Xoc, an extension-oriented compiler for systems programming. In Proc. ASPLOS, pages 244--254. ACM, 2008. Google ScholarDigital Library
- X. Feng and Z. Shao. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. ICFP, pages 254--267. ACM, 2005. Google ScholarDigital Library
- X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. PLDI, pages 401--414. ACM, 2006. Google ScholarDigital Library
- X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying low-level programs with hardware interrupts and preemptive threads. In Proc. PLDI, pages 170--182. ACM, 2008. Google ScholarDigital Library
- S. E. Ganz, A. Sabry, and W. Taha. Macros as multi-stage computations: type-safe, generative, binding macros in MacroML. In Proc. ICFP, pages 74--85. ACM, 2001. Google ScholarDigital Library
- M. Grabmüller and D. Kleeblatt. Harpy: Run-time code generation in Haskell. In Proc. Haskell Workshop, page 94. ACM, 2007. Google ScholarDigital Library
- D. Greenaway, J. Andronick, and G. Klein. Bridging the gap: Automatic verified abstraction of C. In Proc. ITP, volume 7406 of LNCS, pages 99--115. Springer-Verlag, 2012.Google ScholarCross Ref
- R. Grimm. Better extensibility through modular syntax. In Proc. PLDI, pages 38--51. ACM, 2006. Google ScholarDigital Library
- D. Herman and M. Wand. A theory of hygienic macros. In Proc. ESOP, volume 4960 of LNCS, pages 48--62. Springer-Verlag, 2008. Google ScholarDigital Library
- G. C. Hunt and J. R. Larus. Singularity: Rethinking the software stack. ACM SIGOPS Operating Systems Review, 41 (2): 37--49, 2007. Google ScholarDigital Library
- T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In Proc. USENIX ATC, pages 275--288. USENIX Association, 2002. Google ScholarDigital Library
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In Proc. SOSP, pages 207--220. ACM, 2009. Google ScholarDigital Library
- X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. POPL, pages 42--54. ACM, 2006. Google ScholarDigital Library
- G. Mainland. Explicitly heterogeneous metaprogramming with MetaHaskell. In Proc. ICFP, pages 311--322. ACM, 2012. Google ScholarDigital Library
- A. McCreight, Z. Shao, C. Lin, and L. Li. A general framework for certifying garbage collectors and their mutators. In Proc. PLDI, pages 468--479. ACM, 2007. Google ScholarDigital Library
- M. O. Myreen. Verified just-in-time compiler on x86. In Proc. POPL, pages 107--118. ACM, 2010. Google ScholarDigital Library
- M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. In Proc. TACAS, volume 4424 of LNCS, pages 568--582. Springer-Verlag, 2007. Google ScholarDigital Library
- Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. POPL, pages 320--333. ACM, 2006. Google ScholarDigital Library
- M. Parkinson and G. Bierman. Separation logic and abstraction. In Proc. POPL, pages 247--258. ACM, 2005. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, pages 55--74. IEEE Computer Society, 2002. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24 (3): 217--298, May 2002. Google ScholarDigital Library
- W. Taha and T. Sheard. Multi-stage programming with explicit annotations. In Proc. PEPM, pages 203--217. ACM, 1997. Google ScholarDigital Library
- T. Tuerk. Local reasoning about while-loops. In Proc. VSTTE Theory Workshop, 2010.Google Scholar
- H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. O'Hearn. Scalable shape analysis for systems code. In Proc. CAV, volume 5123 of LNCS, pages 385--398. Springer-Verlag, 2008. Google ScholarDigital Library
Index Terms
- The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier
Recommendations
Mostly-automated verification of low-level programs in computational separation logic
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationSeveral recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying ...
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier
ICFP '13We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is ...
Mostly-automated verification of low-level programs in computational separation logic
PLDI '11Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying ...
Comments