Dear seL4 Community,
On behalf of the seL4 Foundation I’m pleased to announce that we have awarded interim endorsement to Proofcraft for providing commercial support, verification projects, training and consulting on formal verification of seL4 and seL4-based systems. Proofcraft is founded by the verification leaders of seL4 and has unrivalled expertise in this space.
See https://sel4.systems/Foundation/Services/ for details.
Following CSIRO’s abandoning of Trustworthy Systems (TS) and the seL4 technology TS developed, the seL4 community and the seL4 Foundation have grown a lot. This has led to concerns that the broader participation might have the potential to undermine the integrity of seL4. In my latest blog, I explain why there is no reason for such concern. seL4's open governance and technical leadership is based on technical merit and established trust, not money.
Founded by the seL4 verification leaders, Proofcraft offers commercial support, verification projects, training and consulting on formal verification in general, and involving seL4 specifically. By applying mathematical machine-checked software verification, Proofcraft increases critical software systems' reliability, safety and security, for a verified future.
We are very pleased to welcome Proofcraft to the seL4 Foundation!
Xcalibyte, a member of the seL4 Foundation, is hosting a webinar on Sep 16, 2021, given by Gernot Heiser, seL4 Foundation Chairman & Scientia Professor, UNSW Sydney, and Yuning Liang, CEO & co-founder, Xcalibyte. The topic will be ‘The seL4 Microkernel: Proved Security for Cyberphysical Systems’.
To register: https://www.bagevent.com/event/7771850
On behalf of the seL4 Foundation I’d like to thank Ghost for its generous contribution. Ghost's commitment strengthens the seL4 Foundation's mission to continue advancing the ecosystem, the code base, and the verification efforts of seL4, the world's most advanced and highly assured operating-system kernel.
As a founding member of the Foundation, Ghost is developing self-driving cars using seL4, aiming to make the first formally proven safety-critical system on the road into a reality for millions of drivers.
We warmly thank Ghost for its continued support!
Dear seL4 Community,
On behalf of the seL4 Foundation I’m pleased to announce that we have awarded interim endorsement to the seL4-based TRENTOS secure operating system from Foundation member HENSOLDT Cyber. This is the first time a product is endorsed, and marks a new milestone for the Foundation and the growth of the seL4 ecosystem.
HENSOLDT Cyber's training module for TRENTOS has also received interim endorsement, which constitutes another milestone, as the first endorsed training provided from outside the Trustworthy Systems group.
Details on interim-endorsed services and products are on our services and products page https://sel4.systems/Foundation/Services/
"Lotus is a leader in the Global Premium Sport Car market. We stand out as a brand dedicated to pure driving experience. Committed to advancing technology with precision and passion, Lotus continues to spearhead research into areas such as autonomous driving, connectivity, intelligence, electrification. Emira, Evija, Evora are representative models that in recent years drive Lotus’ world-wide reputation. Going forward, Lotus’ approach will be based on the principle of “EAS-IP” (Electrify, Amplify, Simplify, Intensify and Personify), a globally R&D strategy, and excellent autonomous driving solutions to create a novel, technology-based driving experience for future global users.
"In joining the seL4 Foundation, Lotus is committed to the development and deployment of the seL4 microkernel in the field of autonomous driving, advance Lotus' automotive operating system to meet the overall functional safety goals of the system, and realize the launch of safe and reliable autonomous driving products.”
Welcome to seL4, Lotus!
On 6 August DARPA brought the “SMACCMcopter” to DEF CON and invited the assembled hacker elite to attack it. The SMACCMcopter was the research vehicle of the Air Team at DARPA's HACMS program. The Trustworthy Systems team worked with project partners to deploy seL4 and leverage formal methods to protect the drone from cyber attacks.
The result? Predictably, sel4's verified security enforcement defeated the hackers comprehensively. As DARPA said: “Formal methods FTW!”
The assurance story for seL4 on RISC-V <https://riscv.org/>keeps building.
We first formally proved functional correctness: that the seL4 C code on RISC-V platforms behaves exactly as its specification says <https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/>.
We then established binary correctness: that the machine code running on the processor behaves exactly as the C code, and by extension, as the specification says <https://microkerneldude.wordpress.com/2021/05/05/sel4-on-risc-v-verified-to…>. We now have established the crucial integrity property for seL4 on RISC-V: that the specification, and by extension the kernel binary, prevents an application running on top from modifying data without authorisation. In seL4 speak: seL4 provably enforces capability-based access control.
“The integrity property is crucial for security: it is key to enforce the isolation of components running on top of the kernel”, says Gerwin Klein, seL4 verification expert and chair of the seL4 Foundation technical steering committee. “This is what allows critical components, like the network controller that has access to software-controlled brakes in a modern car, to securely run alongside untrusted software, like the entertainment system. With integrity proved, you know that an attack on or from a vulnerable untrusted part of the system cannot compromise the critical parts.”
Integrity had been proved in the original seL4 verification on the Arm32 architecture. It is now also established for RISC-V architecture, making it the only 64-bit architecture that has an OS with such a comprehensive verification and security story. We thank Ryan Barry <https://trustworthy.systems/people/?cn=Ryan+Barry> of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council <https://www.arc.gov.au/> through grant DP190103743 which has enabled this work.
See Gernot's blog <https://microkerneldude.wordpress.com/2021/08/04/sel4-integrity-enforcement…> for more details. The proof is available on GitHub <https://github.com/seL4/l4v/tree/master/proof/access-control>.