August 2021 - Announce - lists.sel4.systems

Thank you for your donation, Ghost!
by Announcements about seL4 -- low volume list 31 Aug '21

31 Aug '21

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! Gernot

1 0

Interim endorsement for HENSOLDT Cyber product and training
by Announcements about seL4 -- low volume list 25 Aug '21

25 Aug '21

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/ Gernot

1 0

The seL4 Foundation welcomes new member Lotus Cars
by Announcements about seL4 -- low volume list 18 Aug '21

18 Aug '21

"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! Gernot

1 0

seL4 defeats DEF CON hackers
by Announcements about seL4 -- low volume list 13 Aug '21

13 Aug '21

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!” https://sel4.systems/news.pml Gernot

1 0

Proof that seL4 enforces integrity established for RISC-V
by Announcements about seL4 -- low volume list 04 Aug '21

04 Aug '21

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>. June

1 0

Kansas State Joins the seL4 Foundation
by Announcements about seL4 -- low volume list 03 Aug '21

03 Aug '21

We are pleased to welcome Kansas State University as Associate Member of the se4 Foundation. KSU has for years been collaborating for years on seL4-based projects with a number of Foundation members under multiple DARPA projects and we are looking forward to their continued involvement. Welcome KSU! Gernot

1 0