August 2026 - Announce - lists.sel4.systems

seL4 security proofs now complete on AArch64
by Announcements about seL4 -- low volume list 24 Aug '26

24 Aug '26

The verification of seL4 on the 64-bit Arm architecture has reached another milestone. After completing the proofs of functional correctness and integrity, Proofcraft has now established the proof that seL4 enforces confidentiality on AArch64, providing a formal mathematical proof that the kernel prevents an application running on top of seL4 from learning information without authorisation. This milestone completes the formal proof that the seL4 implementation code on AArch64 enforces security isolation of the applications running on top (under the assumptions listed here [0]). This isolation prevents attacks on non-critical applications from propagating to critical applications and compromising them. https://proofcraft.systems/news-2026/#2026-08-21 [0] https://sel4.systems/Verification/assumptions.html June

1 0

Thank you UNSW Sydney, bronze sponsor of the seL4 Summit 2026
by Announcements about seL4 -- low volume list 17 Aug '26

17 Aug '26

The seL4 Foundation thanks UNSW Sydney [0] for becoming a Bronze sponsor of the seL4 Summit 2026 [1]. seL4 was created by the Trustworthy Systems (TS) team [2], which is now part of the UNSW [0], a founding member of the seL4 Foundation. The team has a track record of designing and implementing systems software for performance and reliability, and using rigorous formal methods to prove that they meet their security and reliability goals. Their aims are to: shift the software industry away from ad-hoc, unreliable engineering practices, and towards more principled and trustworthy methods; and make verified software a default choice, especially in safety- and security-critical systems. The team works with government and commercial partners, as well as the broader software engineering community, to drive this change. [0] https://www.unsw.edu.au/ [1] https://sel4.systems/Summit/2026/ [2] https://trustworthy.systems/ -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

Thank you DornerWorks, sponsor of the seL4 Summit 2026 AM & PM Break
by Announcements about seL4 -- low volume list 14 Aug '26

14 Aug '26

The seL4 Foundation thanks DornerWorks [0], sponsor of the seL4 Summit 2026 AM & PM Break [1]. DornerWorks is an embedded technology partner, a founding member of the seL4 Foundation [2], and one of its endorsed service providers [3]. Our dedicated team of seL4 experts helps organizations accelerate the integration of seL4 as the trusted software foundation for secure, safety-critical embedded systems and products. [0] https://www.dornerworks.com/ [1] https://sel4.systems/Summit/2026/ [2] https://sel4.systems/Foundation/ [3] https://sel4.systems/Services/ -- Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0