Announce

Download

announce@sel4.systems

December 2021

1 participants
2 discussions

Technology Innovation Institute joins the seL4 Foundation
by Announcements about seL4 -- low volume list 15 Dec '21

15 Dec '21

The seL4 Foundation is pleased to welcome the Technology Innovation Institute. Technology Innovation Institute’s (TII) Secure Systems Research Centre (SSRC) has obtained seL4 Foundation membership that will enable the Centre to participate in and contribute to driving the open source for a robust hypervisor technology. The critical technology will help build a secure software stack for many edge devices, such as secure communicators and drones. Through the membership, TII will research, contribute to and advance next-generation high-end edge device environments that focus on resilience, isolation, trust, and security. https://sel4.systems/news/2021#member-tii <https://sel4.systems/news/2021#member-tii> https://www.tii.ae <https://www.tii.ae/> June

1 0

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

01 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