- Announce - lists.sel4.systems

Proof that seL4 enforces confidentiality established for RISC-V
by Announcements about seL4 -- low volume list 02 Dec '21

02 Dec '21

In July, we announced that the assurance story for seL4 on RISC-V keeps building, with the completion of the proof that seL4 enforces integrity, following the earlier proofs of functional correctness and binary correctness for seL4 on RISC-V. The next step in the assurance stack is now also completed for RISC-V with the proof that seL4 enforces confidentiality, i.e. that seL4 provably enforces information flow control, when it is correctly configured to do so. "This completes the 3 big CIA security properties for seL4 on RISC-V: confidentiality, integrity and availability. While integrity ensures there is no unauthorised interference with private data, confidentiality ensures there is no unauthorised access to private data”, says Gernot Heiser, chair of the seL4 Foundation. We thank Ryan Barry of the Trustworthy Systems group at UNSW, main author of these proofs! We also gratefully acknowledge funding from the Australian Research Council through grant DP190103743 which has enabled this work. The proof is available on GitHub. https://sel4.systems/news/2021 https://github.com/seL4/l4v/tree/master/proof/infoflow#readme June

1 0

Interim endorsement for Proofcraft as a trusted service provider
by Announcements about seL4 -- low volume list 14 Oct '21

14 Oct '21

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

1 0

seL4 is safe – don't believe the FUD!
by Announcements about seL4 -- low volume list 28 Sep '21

28 Sep '21

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. Details: https://microkerneldude.wordpress.com/2021/09/28/where-is-sel4-heading/

1 0

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

14 Sep '21

Please note that the original registration link no longer works outside China. Please use this link instead: http://xcalscan.mikecrm.com/Uw4y9HU Apologies for that. Gernot

1 0

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