skip to main content
research-article
Free access

seL4: formal verification of an operating-system kernel

Published: 01 June 2010 Publication History
First page of PDF

References

[1]
Alkassar, E., Schirmer, N., Starostin, A. Formal pervasive verification of a paging mechanism. TACAS. C.R. Ramakrishnan and J. Rehof, eds. Volume 4963 of LNCS (2008). Springer, 109--123.
[2]
Dennis, J.B., Van Horn, E.C. Programming semantics for multiprogrammed computations. CACM 9 (1966), 143--155.
[3]
Elkaduwe, D., Klein, G., Elphinstone, K. Verified protection model of the seL4 microkernel. VSTTE 2008---Verified Software: Theories, Tools & Experiments. J. Woodcock and N. Shankar eds. Volume 5295 of LNCS (Toronto, Canada, Oct 2008), Springer, 99--114.
[4]
ISO/IEC. Programming languages---C. Technical Report 9899:TC2, ISO/IEC JTC1/SC22/WG14, May 2005.
[5]
Leroy, X. Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. 33rd POPL. J.G. Morrisett and S.L.P. Jones, eds. (New York, NY, USA, 2006), ACM, 42--54.
[6]
Liedtke, J. Towards real microkernels. CACM 39, 9 (Sept 1996), 70--77.
[7]
Ni, Z., Yu, D., Shao. Z. Using XCAP to certify realistic system code: Machine context management. 20th TPHOLs, volume 4732 of LNCS (Kaiserslautern, Germany, Sept 2007), Springer, 189--206.
[8]
Nipkow, T., Paulson, L., Wenzel, M. Isabelle/HOL---A Proof Assistant for Higher-Order Logic. Volume 2283 of LNCS (2002), Springer.
[9]
Ormandy, T., Tinnes, J. Linux null pointer dereference due to incorrect proto_ops initializations. http://www.cr0.org/misc/CVE-2009-2692.txt, 2009.
[10]
Saltzer, J.H., Schroeder, M.D. The protection of information in computer systems. Proc. IEEE 63 (1975), 1278--1308.
[11]
Shapiro, J.S., Smith, J.M., Farber, D.J. EROS: A fast capability system. 17th SOSP (Charleston, SC, USA, Dec 1999), 170--185.

Cited By

View all
  • (2025)Deductive Verification of Solidity Smart Contracts with SSCalcScience of Computer Programming10.1016/j.scico.2025.103267(103267)Online publication date: Jan-2025
  • (2024)Analysis and Control of Partially Observed Discrete-Event Systems via Positively Constructed FormulasComputation10.3390/computation1205009512:5(95)Online publication date: 9-May-2024
  • (2024)Formal Methods in IndustryFormal Aspects of Computing10.1145/368937437:1(1-38)Online publication date: 21-Aug-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image Communications of the ACM
Communications of the ACM  Volume 53, Issue 6
June 2010
148 pages
ISSN:0001-0782
EISSN:1557-7317
DOI:10.1145/1743546
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2010
Published in CACM Volume 53, Issue 6

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Research-article
  • Popular
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1,014
  • Downloads (Last 6 weeks)108
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Deductive Verification of Solidity Smart Contracts with SSCalcScience of Computer Programming10.1016/j.scico.2025.103267(103267)Online publication date: Jan-2025
  • (2024)Analysis and Control of Partially Observed Discrete-Event Systems via Positively Constructed FormulasComputation10.3390/computation1205009512:5(95)Online publication date: 9-May-2024
  • (2024)Formal Methods in IndustryFormal Aspects of Computing10.1145/368937437:1(1-38)Online publication date: 21-Aug-2024
  • (2024)Toast: A Heterogeneous Memory Management SystemProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques10.1145/3656019.3676944(53-65)Online publication date: 14-Oct-2024
  • (2024)Securing Verified IO Programs Against Unverified Code in F*Proceedings of the ACM on Programming Languages10.1145/36329168:POPL(2226-2259)Online publication date: 5-Jan-2024
  • (2024)Verifying Rust Implementation of Page Tables in a Software Enclave HypervisorProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640398(1218-1232)Online publication date: 27-Apr-2024
  • (2024)Deep learning-based software engineering: progress, challenges, and opportunitiesScience China Information Sciences10.1007/s11432-023-4127-568:1Online publication date: 24-Dec-2024
  • (2024)Microprocessor Assurance and the Role of Theorem ProvingHandbook of Computer Architecture10.1007/978-981-97-9314-3_38(1321-1363)Online publication date: 21-Dec-2024
  • (2024)Formal Modeling and Verification of the Design Layer of Space Operating SystemsSignal and Information Processing, Networking and Computers10.1007/978-981-97-2120-7_63(516-525)Online publication date: 3-May-2024
  • (2024)Secure Smart Contracts with Isabelle/SoliditySoftware Engineering and Formal Methods10.1007/978-3-031-77382-2_10(162-181)Online publication date: 4-Nov-2024
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Magazine Site

Login options

Full Access

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media