Abstract
Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then used to prove that the code adheres to its specification.
In this paper, we explore the overlap between formal verification and code optimization. We propose two approaches to reuse the invariants derived in formal proofs and integrate them into compilation. The first applies invariants extracted from the proof, while the second leverages the property of program safety (i.e., the absence of bugs). We reuse this information to improve the performance of generated object code.
We evaluated these methods on seL4, a real-world formally-verified microkernel, and obtained improvements in average runtime performance (up to 28%) and in worst-case execution time (up to 25%). In macro-benchmarks, we found the performance of para-virtualized Linux running on the microkernel improved by 6-16%.
- E. Alkassar, M. Hillebrand, D. Leinenbach, N. Schirmer, and A. Starostin. The Verisoft approach to systems verification. In N. Shankar and J. Woodcock, editors, VSTTE 2008, volume 5295 of LNCS, pages 209--224. Springer, 2008. Google ScholarDigital Library
- J. Andronick, B. Chetali, and C. Paulin-Mohring. Formal Verification of Security Properties of Smart Card Embedded Source Code. In J. Fitzgerald, I. J. Hayes, and A. Tarlecki, editors, FM, volume 3582 of LNCS, pages 302--317, Newcastle, UK, Jul 2005. Springer. Google ScholarDigital Library
- Y. Bertot, B. Gregoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, Workshop TYPES 2004, volume 3839 of LNCS, pages 66--81, 2006. Google ScholarDigital Library
- B. Blackham and G. Heiser. Correct, fast, maintainable - choose any three! In 3rd APSys, pages 13:1--13:7, Seoul, Korea, Jul 2012. Google ScholarDigital Library
- B. Blackham, Y. Shi, S. Chattopadhyay, A. Roychoudhury, and G. Heiser. Timing analysis of a protected operating system kernel. In 32nd RTSS, pages 339--348, Vienna, Austria, Nov 2011. Google ScholarDigital Library
- S. Blazy and X. Leroy. Formal verification of a memory model for C-like imperative languages. In International Conference on Formal Engineering Methods, vol. 3785 of LNCS, pages 280--299, 2005. Google ScholarDigital Library
- S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a C compiler front-end. In 14th FM, volume 4085 of LNCS, pages 460--475. Springer, 2006. Google ScholarDigital Library
- M. Daum, N. W. Schirmer, and M. Schmidt. From operating-system correctness to pervasively verified applications. In IFM, volume 6396 of LNCS, pages 105--120, Nancy, France, 2010. Springer. Google ScholarDigital Library
- R. J. Feiertag and P. G. Neumann. The foundations of a provably secure operating system (PSOS). In AFIPS Conf. Proc., 1979 National Comp. Conf., pages 329--334, New York, NY, USA, Jun 1979.Google ScholarCross Ref
- L. Gu, A. Vaynberg, B. Ford, Z. Shao, and D. Costanzo. CertiKOS: A certified kernel for secure cloud computing. In 2nd APSys, 2011. Google ScholarDigital Library
- C. L. Heitmeyer, M. Archer, E. I. Leonard, and J. McLean. Formal specification and verification of data separation in a separation kernel for an embedded system. In CCS, pages 346--355, Alexandria, VA, USA, 2006. Google ScholarDigital Library
- M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In 2nd PLOS, Glasgow, UK, Jul 2005.Google Scholar
- 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 22nd SOSP, pages 207--220, Big Sky, MT, USA, Oct 2009. ACM. Google ScholarDigital Library
- X. Leroy. Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In J. G. Morrisett and S. L. P. Jones, editors, 33rd POPL, pages 42--54, Charleston, SC, USA, 2006. ACM. Google ScholarDigital Library
- J. Liedtke. On μ-kernel construction. In 15th SOSP, pages 237--250, Copper Mountain, CO, USA, Dec 1995. Google ScholarDigital Library
- A. Ramirez, J. l. Larriba-pey, C. Navarro, J. Torrellas, and M. Valero. Software trace cache. In 13th Intl. Conference on Supercomputing, 1999. Google ScholarDigital Library
- S. Rideau and X. Leroy. Validating register allocation and spilling. In Compiler Construction, volume 6011 of LNCS, pages 224--243, 2010. Google ScholarDigital Library
- T. Sewell, M. Myreen, and G. Klein. Translation validation for a verified OS kernel. In PLDI, pages 471--481, Seattle, Washington, USA, Jun 2013. ACM. Google ScholarDigital Library
- H. Tews, T. Weber, and M. Völp. A formal model of memory peculiarities for the verification of low-level operating-system code. In R. Huuck, G. Klein, and B. Schlich, editors, 3rd SSV, volume 217 of ENTCS, pages 79--96, Sydney, Australia, Feb 2008. Elsevier. Google ScholarDigital Library
- The GCC Team. GCC 4.8 release series: Changes, new features, and fixes. http://gcc.gnu.org/gcc-4.8/changes.html, 2013.Google Scholar
- J.-B. Tristan and X. Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In 35th POPL, pages 17--27, 2008. Google ScholarDigital Library
- J.-B. Tristan and X. Leroy. Verified validation of lazy code motion. In 2009 PLDI, pages 316--326, 2009. Google ScholarDigital Library
- J.-B. Tristan and X. Leroy. A simple, verified validator for software pipelining. In 37th POPL, pages 83--92, 2010. Google ScholarDigital Library
- M. T. Vandevoorde. Specifications can make programs run faster. In Theory and Practice of Software Development, LNCS, volume 668, pages 215--229, 1993. Google ScholarDigital Library
- B. J. Walker, R. A. Kemmerer, and G. J. Popek. Specification and verification of the UCLA Unix security kernel. CACM, 23 (2): 118--131, 1980. Google ScholarDigital Library
- X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich, and M. F. Kaashoek. Undefined behavior: what happened to my code? In 3rd APSys, pages 9:1--9:7, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In 2004 PLDI, 2004. Google ScholarDigital Library
- R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström. The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Emb. Comput. Syst., 7 (3): 1--53, 2008. ISSN 1539-9087. Google ScholarDigital Library
Index Terms
- Code optimizations using formally verified properties
Recommendations
Code optimizations using formally verified properties
OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applicationsFormal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Verdi: a framework for implementing and formally verifying distributed systems
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationDistributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex ...
Comments