Communications of the ACM

Home/Magazine Archive/April 2020 (Vol. 63, No. 4)/seL4 in Australia: From Research to Real-World Trustworthy.../Abstract

East Asia and Oceania Region special section: Big trends

seL4 in Australia: From Research to Real-World Trustworthy Systems

By Gernot Heiser, Gerwin Klein, June Andronick
Communications of the ACM, April 2020, Vol. 63 No. 4, Pages 72-75
10.1145/3378426
Comments

View as: Print Mobile App ACM Digital Library In the Digital Edition Share:

key with notches spelling seL4, illustration — Credit: Andrij Borys Associates

Ten years ago, the functional correctness proof of the seL4 microkernel marked the first time a complete operating system (OS) kernel had been verified to the source-code level.⁴ This means there was a machine-checked proof that the implementation in the C language satisfied the kernel's specification, expressed in mathematical logic.

Much has happened since then: We have extended the verification to show the kernel enforces desired security and safety properties, we have removed the need to trust the compiler, and we verified implementations for processor architectures other than the original Arm v6. We used experience from deploying seL4 in a number of real-world systems to evolve the kernel and its proofs to support a broader class of use cases, and we have made significant progress toward extending the assurance to systemwide properties. We will provide a brief overview of these developments, as well as ongoing research.

No entries found

Log in to Read the Full Article

Sign In

Sign in using your ACM Web Account username and password to access premium content if you are an ACM member, Communications subscriber or Digital Library subscriber.

Need Access?

Please select one of the options below for access to premium content and features.

Create a Web Account

If you are already an ACM member, Communications subscriber, or Digital Library subscriber, please set up a web account to access premium content on this site.

Join the ACM

Become a member to take full advantage of ACM's outstanding computing information resources, networking opportunities, and other benefits.

Subscribe to Communications of the ACM Magazine

Get full access to 50+ years of CACM content and receive the print version of the magazine monthly.

Purchase the Article

Non-members can purchase this article or a copy of the magazine in which it appears.