Thomas Arthur Leck Sewell
ABSTRACT
We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware.
More generally, we present an approach for proving refinement between the formal semantics of a program on the C source level and its formal semantics on the binary level, thus checking the validity of compilation, including some optimisations, and linking, and extending static properties proved of the source code to the executable. We make use of recent improvements in SMT solvers to almost fully automate this process.
We handle binaries generated by unmodified gcc 4.5.1 at optimisation level 1, and can handle most of seL4 even at optimisation level 2.
- E. Alkassar, W. Paul, A. Starostin, and A. Tsyban. Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In P. O'Hearn, G. T. Leavens, and S. Rajamani, editors, VSTTE 2010, volume 6217 of LNCS, pages 71--85, Edinburgh, UK, Aug 2010. Springer. Google Scholar
Digital Library
- A. W. Appel. Verified software toolchain?(invited talk). In G. Barthe, editor, Proc. 20th ESOP, volume 6602 of LNCS, pages 1--17, Saarbrücken, Germany, Mar. 2011. Springer. Google ScholarDigital Library
- W. R. Bevier. Kit: A study in operating system verification. IEEE Trans. Softw. Engin., 15(11):1382--1396, 1989. Google ScholarDigital Library
- J. O. Blech, I. Schaefer, and A. Poetzsch-Heffter. Translation validation of system abstractions. In Proc. 7th Int. Conf. on Runtime verification, RV'07, pages 139--150, Vancover, Canada, 2007. Springer. Google ScholarDigital Library
- A. Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In J. Ferrante and K. S. McKinley, editors, Proc. PLDI'07, pages 54--65. ACM, 2007. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Proc. 32nd PLDI, pages 234--245, San Jose, California, USA, 2011. ACM. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and J. Rehof, editors, 14th TACAS, volume 4963 of LNCS, pages 337--340, Budapest, Hungary, Mar. 2008. Springer. Google ScholarDigital Library
- A. Fox and M. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In M. Kaufmann and L. C. Paulson, editors, 1st Int. Conf. Interactive Theorem Proving, volume 6172 of LNCS, pages 243--258, Edinburgh, UK, July 2010. Springer. Google ScholarDigital Library
- B. Goldberg, L. D. Zuck, and C. W. Barrett. Into the loops: Practical issues in translation validation for optimizing compilers. Proc 3rd Int.Workshop on Compiler Optimization Meets Compiler Verification (COCV '04). Electr. Notes Theor. Comput. Sci., 132(1):53--71, 2005. Google ScholarDigital Library
- ISO/IEC. Programming languages C. Technical Report 9899:TC2, ISO/IEC JTC1/SC22/WG14, May 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 Proc. 22nd SOSP, pages 207--220, Big Sky, MT, USA, 2009. ACM. Google ScholarDigital Library
- S. Kundu, S. Lerner, and R. K. Gupta. Translation validation of highlevel synthesis. Trans. Comp.-Aided Des. Integ. Cir. Sys., 29(4):566--579, Apr. 2010. 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, Proc. 33rd POPL, pages 42--54. ACM, 2006. Google ScholarDigital Library
- X. Leroy. A formally verified compiler back-end. J. Automated Reasoning, 43(4):363--446, 2009. Google ScholarDigital Library
- T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. seL4: from general purpose to a proof of information flow enforcement. In IEEE Symp. Security & Privacy, Oakland, CA, May 2013.Google ScholarDigital Library
- M. O. Myreen. Formal verification of machine-code programs. PhD thesis, University of Cambridge, 2009.Google Scholar
- M. O. Myreen, M. J. C. Gordon, and K. Slind. Machine-code verification for multiple architectures - an application of decompilation into logic. In A. Cimatti and R. B. Jones, editors, Formal Methods in Computer-Aided Design (FMCAD), pages 1--8. IEEE, 2008. Google ScholarDigital Library
- M. O. Myreen, M. J. C. Gordon, and K. Slind. Decompilation into logic -- improved. In G. Cabodi and S. Singh, editors, Formal Methods in Computer-Aided Design (FMCAD), pages 78--81. IEEE, 2012.Google Scholar
- G. C. Necula. Translation validation for an optimizing compiler. In Proc. PLDI'00, pages 83--94, Vancouver, BC, Canada, 2000. ACM. Google ScholarDigital Library
- Z. Ni, D. Yu, and Z. Shao. Using XCAP to certify realistic systems code: machine context management. In Proc. 20th TPHOLs, volume 4732 of LNCS, pages 189--206. Springer, 2007. Google ScholarDigital Library
- T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google ScholarDigital Library
- Open Kernel Labs. seL4 research and evaluation download. http://ertos.nicta.com.au/software/seL4/, 2011.Google Scholar
- J. Peleska, E. Vorobev, and F. Lapschies. Automated test case generation with SMT-solving and abstract interpretation. In Proc 3rd Int. Conf. NASA Formal methods, NFM'11, pages 298--312, Pasadena, CA, 2011. Springer. Google ScholarDigital Library
- A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In B. Steffen, editor, Proc. 4th TACAS, volume 1384 of LNCS, pages 151--166. Springer, 1998. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS), pages 55--74. IEEE Computer Society, 2002. Google ScholarDigital Library
- M. Ryabtsev and O. Strichman. Translation validation: From Simulink to C. In Proc. 21st Int. Conf. on Computer Aided Verification, CAV '09, pages 696--701, Grenoble, France, 2009. Springer. Google ScholarDigital Library
- N. Schirmer. Verification of Sequential Imperative Programs in Isabelle/ HOL. PhD thesis, Technische Universität München, 2006.Google Scholar
- T. Sewell, S. Winwood, P. Gammie, T. Murray, J. Andronick, and G. Klein. seL4 enforces integrity. In M. C. J. D. van Eekelen, H. Geuvers, J. Schmaltz, and F. Wiedijk, editors, 2nd Int. Conf. on Interactive Theorem Proving, volume 6898 of LNCS, pages 325--340, Nijmegen, The Netherlands, Aug. 2011. Springer. Google ScholarDigital Library
- K. Slind and M. Norrish. A brief overview of HOL4. In 20th Int. Conf. on Theorem Proving in Higher Order Logics, pages 28--32, Montreal, Canada, Aug. 2008. Google ScholarDigital Library
- J.-B. Tristan, P. Govereau, and G. Morrisett. Evaluating value-graph translation validation for llvm. In Proc. 32nd PLDI, pages 295--305, San Jose, CA, USA, 2011. ACM. Google ScholarDigital Library
- H. Tuch. Formal verification of C systems code: Structured types, separation logic and theorem proving. J. Automated Reasoning: Special Issue on OS Verification, 42(2-4):125--187, Apr. 2009. Google ScholarDigital Library
- H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In M. Hofmann and M. Felleisen, editors, Proc. 34th POPL, pages 97--108, Nice, France, Jan. 2007. ACM. Google ScholarDigital Library
- J. Yang and C. Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proc. PLDI'10, pages 99--110, Toronto, Canada, 2010. ACM. Google ScholarDigital Library
- X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In M. W. Hall and D. A. Padua, editors, Proc. 32nd PLDI, pages 283--294, San Jose, CA, USA, June 2011. ACM. Google ScholarDigital Library
- L. D. Zuck, A. Pnueli, Y. Fang, B. Goldberg, and Y. Hu. Translation and run-time validation of optimized code. Runtime Verification 2002 (RV'02). Electr. Notes Theor. Comput. Sci., 70(4):179--200, 2002.Google ScholarCross Ref
- L. D. Zuck, A. Pnueli, and B. Goldberg. VOC: A methodology for the translation validation of optimizing compilers. J. UCS, 9(3):223--247, 2003.Google Scholar
Index Terms
- Translation validation for a verified OS kernel
Recommendations
seL4: formal verification of an OS kernel
SOSP '09: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principlesComplete formal verification is the only known way to guarantee that a system is free of programming errors.
We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to ...
Comprehensive formal verification of an OS microkernel
We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel.
We discuss the kernel design we used to make its verification tractable. We then describe the functional ...
Translation validation for a verified OS kernel
PLDI '13We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently ...
Comments