- Announce - lists.sel4.systems

The seL4 Foundation welcomes new member Proofcraft
by Announcements about seL4 -- low volume list 14 Sep '21

14 Sep '21

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

1 0

Xcalibyte webinar by Gernot Heiser on seL4 on Sep 16, 2021
by Announcements about seL4 -- low volume list 10 Sep '21

10 Sep '21

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

1 0

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

Happy seL4 day!
by Announcements about seL4 -- low volume list 29 Jul '21

29 Jul '21

On 29th July 2009, the original functional correctness proof of seL4 was completed, a widely-recognised research breakthrough and the first big milestone in seL4's history. We obviously had a party then, and have since celebrated its anniversary, calling it, tongue-in-cheek, “International Proof Day”. On the fifth anniversary we open-sourced seL4, which was another major milestone, which we referred to as “seL4 Freedom Day”. Today marks the 12th anniversary of the proof, and the 7th anniversary of open-sourcing, and from now on we’ll refer to the date simply as "seL4 Day”. The seL4 community is now definitely global. Still we would normally have a physical party in Sydney, but won’t be able to due to the renewed Covid-19 restrictions – so we’ll all be remote ;-) Happy seL4 day everyone! A virtual toast to you all, and a big thank-you to all for your continued support! June -- June Andronick CEO of the seL4 Foundation https://sel4.systems/Foundation

1 0

TU Munich joins the seL4 Foundation
by Announcements about seL4 -- low volume list 20 Jul '21

20 Jul '21

The seL4 Foundation is pleased to welcome Technical University of Munich as an associate member. The TUM, home of the Isabelle theorem prover used in the verification of seL4, has been a collaborator of the Trustworthy Systems team for many years. Gernot

1 0