AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We have shown that full, rigorous, formal verification is practically achievable for operating system microkernels with very reasonable effort compared to traditional development methods

seL4: formal verification of an OS kernel

SOSP, pp.207-220, (2009)

Cited by: 1828|Views381
EI

Abstract

Complete 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 its C implementation. We assume correctness of compiler, assembly code, and hardware, a...More

Code:

Data:

0
Introduction
  • The security and reliability of a computer system can only be as good as that of the underlying operating system (OS) kernel.
  • As a consequence, when security or reliability is paramount, the usual approach is to reduce the amount of privileged code, in order to minimise the exposure to bugs.
  • The Common Criteria [66] at the strictest evaluation level requires the system under evaluation to have a “simple” design
Highlights
  • The security and reliability of a computer system can only be as good as that of the underlying operating system (OS) kernel
  • We present the design of seL4, discuss the methodologies we used, and provide an overview of the approach used in the formal verification from high-level specification to the C implementation
  • We have evaluated the performance of seL4 by comparing inter-process communication performance with L4, which has a long history of data points to draw upon [47]
  • We have presented our experience in formally verifying seL4
  • We have shown that full, rigorous, formal verification is practically achievable for operating system microkernels with very reasonable effort compared to traditional development methods
  • We have not invested significant effort into optimisation, we have shown that optimisations are possible and that performance does not need to be sacrificed for verification
Methods
  • Memory management in seL4 is explicit: both in-kernel objects and virtual address spaces are protected and managed via capabilities.
  • Physical memory is initially represented by untyped capabilities, which can be subdivided or retyped into kernel objects such as page tables, thread control blocks, CNodes, endpoints, and frames.
  • The model guarantees all memory allocation in the kernel is explicit and authorised.
  • Initial development of seL4, and all verification work, was done for an ARMv6-based platform, with a subsequent port of the kernel to x86
Results
  • Even though the code size of this change was small, the comparative amount of conceptual cross-cutting was huge.
Conclusion
  • The authors have presented the experience in formally verifying seL4. The authors have shown that full, rigorous, formal verification is practically achievable for OS microkernels with very reasonable effort compared to traditional development methods.

    the authors have not invested significant effort into optimisation, the authors have shown that optimisations are possible and that performance does not need to be sacrificed for verification.
  • The authors observed a confluence of design principles from the formal methods and the OS side, leading to design decisions such as an event-based kernel that is mostly non-preemptable and uses interrupt polling.
  • These decisions made the kernel design simpler and easier to verify without sacrificing performance.
  • Evidence suggests that taking the detour via a Haskell prototype increased the productivity even without considering verification
Tables
  • Table1: Code and proof statistics
Download tables as Excel
Related work
  • We briefly summarise the literature on OS verification. Klein [40] provides a comprehensive overview.

    The first serious attempts to verify an OS kernel were in the late 1970s UCLA Secure Unix [67] and the Provably Secure Operating System (PSOS) [24]. Our approach mirrors the UCLA effort in using refinement and defining functional correctness as the main property to prove. The UCLA project managed to finish 90 % of their specification and 20 % of their proofs in 5 py. They concluded that invariant reasoning dominated the proof effort, which we found confirmed in our project.
Funding
  • We also would like to acknowledge the contribution of the former team members on this verification project: Jeremy Dawson, Jia Meng, Catherine Menon, and David Tsai. NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program
Reference
  • M. Accetta, R. Baron, W. Bolosky, D. Golub, R. Rashid, A. Tevanian, and M. Young. Mach: A new kernel foundation for UNIX development. In 1986 Summer USENIX, pages 93–112, 1986.
    Google ScholarLocate open access versionFindings
  • E. Alkassar, M. Hillebrand, D. Leinenbach, N. Schirmer, A. Starostin, and A. Tsyban. Balancing the load — leveraging a semantics stack for systems verification. JAR, 42(2–4), 2009.
    Google ScholarLocate open access versionFindings
  • E. Alkassar, N. Schirmer, and A. Starostin. Formal pervasive verification of a paging mechanism. In C. R. Ramakrishnan and J. Rehof, editors, Tools and Alg. for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 109–123.
    Google ScholarLocate open access versionFindings
  • J. Alves-Foss, P. W. Oman, C. Taylor, and S. Harrison. The MILS architecture for high-assurance embedded systems. Int. J. Emb. Syst., 2:239–247, 2006.
    Google ScholarLocate open access versionFindings
  • M. Archer, E. Leonard, and M. Pradella. Analyzing security-enhanced Linux policy specifications. In POLICY ’03: Proc. 4th IEEE Int. WS on Policies for Distributed Systems and Networks, pages 158–169. IEEE Computer Society, 2003.
    Google ScholarLocate open access versionFindings
  • T. Ball and S. K. Rajamani. SLIC: A specification language for interface checking. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.
    Google ScholarFindings
  • 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 15th SOSP, Dec 1995.
    Google ScholarLocate open access versionFindings
  • W. R. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382–1396, 1989.
    Google ScholarLocate open access versionFindings
  • W. R. Bevier and L. Smith. A mathematical model of the Mach kernel: Atomic actions and locks. Technical Report 89, Computational Logic Inc., Apr 1993.
    Google ScholarFindings
  • I. T. Bowman, R. C. Holt, and N. V. Brewster. Linux as a case study: its extracted software architecture. In ICSE ’99: Proc. 21st Int. Conf. on Software Engineering, pages 555–563. ACM, 1999. Elsevier, Jun 2009.
    Google ScholarLocate open access versionFindings
  • [12] P. Brinch Hansen. The nucleus of a multiprogramming operating system. CACM, 13:238–250, 1970.
    Google ScholarLocate open access versionFindings
  • [13] D. Cock. Bitfields and tagged unions in C: Verification through automatic generation. In B. Beckert and G. Klein, editors, VERIFY’08, volume 372 of CEUR Workshop Proceedings, pages 44–55, Aug 2008.
    Google ScholarLocate open access versionFindings
  • [14] D. Cock, G. Klein, and T. Sewell. Secure microkernels, state monads and scalable refinement. In O. A. Mohamed, C. Munoz, and S. Tahar, editors, 21st TPHOLs, volume 5170 of LNCS, pages 167–182. Springer, Aug 2008.
    Google ScholarLocate open access versionFindings
  • [15] B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In 34th POPL. ACM, 2007.
    Google ScholarFindings
  • [16] J. Criswell, A. Lenharth, D. Dhurjati, and V. Adve. Secure virtual architecture: A safe execution environment for commodity operating systems. In 16th SOSP, pages 351–366, Oct 2007.
    Google ScholarLocate open access versionFindings
  • [18] W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.
    Google ScholarFindings
  • [19] P. Derrin, K. Elphinstone, G. Klein, D. Cock, and M. M. T. Chakravarty. Running the manual: An approach to high-assurance microkernel development. In ACM SIGPLAN Haskell WS, Sep 2006.
    Google ScholarLocate open access versionFindings
  • [20] D. Elkaduwe, P. Derrin, and K. Elphinstone. Kernel design for isolation and assurance of physical memory. In 1st IIES, pages 35–40. ACM SIGOPS, Apr 2008.
    Google ScholarLocate open access versionFindings
  • [21] D. Elkaduwe, G. Klein, and K. Elphinstone. Verified protection model of the seL4 microkernel. In J. Woodcock and N. Shankar, editors, VSTTE 2008 — Verified Softw.: Theories, Tools & Experiments, volume 5295 of LNCS, pages 99–114. Springer, Oct 2008.
    Google ScholarLocate open access versionFindings
  • [22] K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. Towards a practical, verified kernel. In 11th HotOS, pages 117–122, May 2007.
    Google ScholarLocate open access versionFindings
  • [23] M. Fahndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. C. Hunt, J. R. Larus, and S. Levi. Language support for fast and reliable message-based communication in Singularity OS. In 1st EuroSys Conf., pages 177–190, Apr 2006.
    Google ScholarLocate open access versionFindings
  • [24] R. J. Feiertag and P. G. Neumann. The foundations of a provably secure operating system (PSOS). In AFIPS Conf. Proc., 1979 National Comp. Conf., Jun 1979.
    Google ScholarLocate open access versionFindings
  • [25] B. Ford, M. Hibler, J. Lepreau, R. McGrath, and P. Tullmann. Interface and execution models in the Fluke kernel. In 3rd OSDI. USENIX, Feb 1999.
    Google ScholarLocate open access versionFindings
  • [26] T. Garfinkel, B. Pfaff, J. Chow, M. Rosenblum, and D. Boneh. Terra: A virtual machine-based platform for trusted computing. In 19th SOSP, Oct 2003.
    Google ScholarLocate open access versionFindings
  • [27] Green Hills Software, Inc. INTEGRITY-178B separation kernel security target version 1.0. http://www.niap-ccevs.org/cc-scheme/st/st vid10119-st.pdf, 2008.
    Findings
  • [28] Greenhills Software, Inc. Integrity real-time operating system. http://www.ghs.com/products/rtos/integrity.html, 2008.
    Findings
  • [29] J. D. Guttman, A. L. Herzog, J. D. Ramsdell, and C. W. Skorupka. Verifying information flow goals in security-enhanced Linux. Journal of Computer Security, 13(1):115–134, 2005.
    Google ScholarLocate open access versionFindings
  • [30] J. T. Haigh and W. D. Young. Extending the noninterference version of MLS for SAT. IEEE Trans. on Software Engineering, 13(2):141–150, 1987.
    Google ScholarLocate open access versionFindings
  • [31] D. S. Hardin, E. W. Smith, and W. D. Young. A robust machine code proof framework for highly secure applications. In ACL2’06: Proc. Int. WS on the ACL2 theorem prover and its applications. ACM, 2006.
    Google ScholarFindings
  • [32] G. Heiser. Hypervisors for consumer electronics. In 6th IEEE CCNC, 2009.
    Google ScholarLocate open access versionFindings
  • [33] 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 ’06: Proc. 13th Conf. on Computer and Communications Security, pages 346–355. ACM, 2006.
    Google ScholarLocate open access versionFindings
  • [34] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In SPIN’03, Workshop on Model Checking Software, 2003.
    Google ScholarLocate open access versionFindings
  • [35] M. Hohmuth, M. Peter, H. Hartig, and J. S. Shapiro. Reducing TCB size by using untrusted components — small kernels versus virtual-machine monitors. In 11th SIGOPS Eur. WS, Sep 2004.
    Google ScholarLocate open access versionFindings
  • [36] M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In 2nd PLOS, Jul 2005.
    Google ScholarLocate open access versionFindings
  • [37] Iguana. http://www.ertos.nicta.com.au/software/kenge/iguana-project/latest/.
    Findings
  • [38] Information Assurance Directorate. U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Jun 2007. Version 1.03. http://www.niap-ccevs.org/cc-scheme/pp/pp.cfm/id/pp skpp hr v1.03/.
    Findings
  • [39] ISO/IEC. Programming languages — C. Technical Report 9899:TC2, ISO/IEC JTC1/SC22/WG14, May 2005.
    Google ScholarFindings
  • [40] G. Klein. Operating system verification — an overview. Sadhana, 34(1):27–69, Feb 2009.
    Google ScholarLocate open access versionFindings
  • [41] G. Klein, P. Derrin, and K. Elphinstone. Experience report: seL4 — formally verifying a high-performance microkernel. In 14th ICFP, Aug 2009.
    Google ScholarLocate open access versionFindings
  • [42] R. Kolanski and G. Klein. Types, maps and separation logic. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Proc. TPHOLs’09, volume 5674 of LNCS. Springer, 2009.
    Google ScholarLocate open access versionFindings
  • [43] L4HQ. http://l4hq.org/arch/arm/.
    Findings
  • [44] 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. ACM, 2006.
    Google ScholarLocate open access versionFindings
  • [45] J. Liedtke. Improving IPC by kernel design. In 14th SOSP, pages 175–188, Dec 1993.
    Google ScholarLocate open access versionFindings
  • [46] J. Liedtke. Towards real microkernels. CACM, 39(9):70–77, Sep 1996.
    Google ScholarLocate open access versionFindings
  • [47] J. Liedtke, K. Elphinstone, S. Schonberg, H. Hartig, G. Heiser, N. Islam, and T. Jaeger. Achieved IPC performance (still the foundation for extensibility). In 6th HotOS, pages 28–31, May 1997.
    Google ScholarLocate open access versionFindings
  • [48] W. B. Martin, P. White, A. Goldberg, and F. S. Taylor. Formal construction of the mathematically analyzed separation kernel. In ASE ’00: Proc. 15th IEEE Int. Conf. on Automated software engineering, pages 133–141. IEEE Computer Society, 2000.
    Google ScholarLocate open access versionFindings
  • [49] Z. Ni, D. Yu, and Z. Shao. Using XCAP to certify realistic system code: Machine context management. In Proc. TPHOLs’07, volume 4732 of LNCS, pages 189–206. Springer, Sep 2007.
    Google ScholarLocate open access versionFindings
  • [50] T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
    Google ScholarFindings
  • [51] OKL4 web site. http://okl4.org.
    Findings
  • [52] T. Perrine, J. Codd, and B. Hardy. An overview of the kernelized secure operating system (KSOS). In Proceedings of the Seventh DoD/NBS Computer Security Initiative Conference, pages 146–160, Sep 1984.
    Google ScholarLocate open access versionFindings
  • [53] Rockwell Collins, Inc. AAMP7r1 Reference Manual, 2003.
    Google ScholarFindings
  • [54] J. M. Rushby. Design and verification of secure systems. In 8th SOSP, pages 12–21, 1981.
    Google ScholarLocate open access versionFindings
  • [55] O. Saydjari, J. Beckman, and J. Leaman. Locking computers securely. In 10th National Computer Security Conference, pages 129–141, Sep 1987.
    Google ScholarLocate open access versionFindings
  • [56] A. Seshadri, M. Luk, N. Qu, and A. Perrig. SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes. In 16th SOSP, pages 335–350, Oct 2007.
    Google ScholarLocate open access versionFindings
  • [57] J. S. Shapiro, D. F. Faber, and J. M. Smith. State caching in the EROS kernel—implementing efficient orthogonal peristence in a pure capability system. In 5th IWOOOS, pages 89–100, Nov 1996.
    Google ScholarLocate open access versionFindings
  • [58] J. S. Shapiro, J. M. Smith, and D. J. Farber. EROS: A fast capability system. In 17th SOSP, Dec 1999.
    Google ScholarLocate open access versionFindings
  • [59] L. Singaravelu, C. Pu, H. Hartig, and C. Helmuth. Reducing TCB complexity for security-sensitive applications: Three case studies. In 1st EuroSys Conf., pages 161–174, Apr 2006.
    Google ScholarLocate open access versionFindings
  • [60] R. Spencer, S. Smalley, P. Loscocco, M. Hibler, D. Andersen, and J. Lepreau. The Flask security architecture: System support for diverse security policies. In 8th USENIX Security Symp., Aug 1999.
    Google ScholarLocate open access versionFindings
  • [61] H. Tews, T. Weber, and M. Volp. A formal model of memory peculiarities for the verification of low-level operating-system code. In R. Huuck, G. Klein, and B. Schlich, editors, Proc. 3rd Int. WS on Systems Software Verification (SSV’08), volume 217 of ENTCS, pages 79–96. Elsevier, Feb 2008.
    Google ScholarLocate open access versionFindings
  • [62] H. Tuch. Formal Memory Models for Verifying C Systems Code. PhD thesis, UNSW, Aug 2008.
    Google ScholarFindings
  • [63] H. Tuch. Formal verification of C systems code: Structured types, separation logic and theorem proving. JAR, 42(2–4):125–187, 2009.
    Google ScholarLocate open access versionFindings
  • [64] H. Tuch, G. Klein, and G. Heiser. OS verification — now! In 10th HotOS, pages 7–12. USENIX, Jun 2005.
    Google ScholarLocate open access versionFindings
  • [65] H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In M. Hofmann and M. Felleisen, editors, 34th POPL, pages 97–108, Jan 2007.
    Google ScholarLocate open access versionFindings
  • [66] US National Institute of Standards. Common Criteria for IT Security Evaluation, 1999. ISO Standard 15408. http://csrc.nist.gov/cc/.
    Findings
  • [67] 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 ScholarLocate open access versionFindings
  • [68] D. A. Wheeler. SLOCCount. http://www.dwheeler.com/sloccount/, 2001.
    Findings
  • [69] A. Whitaker, M. Shaw, and S. D. Gribble. Scale and performance in the Denali isolation kernel. In 5th OSDI, Dec 2002.
    Google ScholarLocate open access versionFindings
  • [70] S. Winwood, G. Klein, T. Sewell, J. Andronick, D. Cock, and M. Norrish. Mind the gap: A verification framework for low-level C. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Proc. TPHOLs’09, volume 5674.
    Google ScholarLocate open access versionFindings
  • [71] W. Wulf, E. Cohen, W. Corwin, A. Jones, R. Levin, C. Pierson, and F. Pollack. HYDRA: The kernel of a multiprocessor operating system. CACM, 17:337–345, 1974.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科