- Announce - lists.sel4.systems

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

29 Jul '24

Happy seL4 day! This year marks a very special seL4 day anniversary. 20 years ago, the L4.verified project started, with the ambitious aim to formally verify an entire microkernel of the L4 family. seL4 was born. 15 years ago, on the 29th of 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. 10 years ago, on the 29th of July 2014, seL4 was open-sourced, an instrumental step towards its adoption in a number of sectors. To celebrate these key anniversaries, a special panel will gather at the seL4 summit 2024 [0] to reflect on the journey over the past 20 years and discuss the future ahead. Stay tuned for more info. [0] https://sel4.systems/Foundation/Summit/2024/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

The seL4 summit Program is available
by Announcements about seL4 -- low volume list 14 Jun '24

14 Jun '24

Have a look at the program [0] of the seL4 summit 2024 [1]. We have a great line-up of interesting seL4 work, with a combination of technical research and development, experience reports of seL4 in the field, technical discussions and birds-of-a-feather sessions. [0] https://sel4.systems/Foundation/Summit/2024/program [1] https://sel4.systems/Foundation/Summit/2024/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Keynotes for seL4 summit 2024 announced
by Announcements about seL4 -- low volume list 12 Jun '24

12 Jun '24

We are pleased to announce that the two keynotes for the seL4 summit 2024 [0] will be Darren Cofer [1] from Collins Aerospace [2] and Ning Qu [3] from NIO [4] . Darren will talk about Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA) [5] and Ning about seL4 in Software-Defined Vehicles: Vision, Roadmap, and Impact at NIO [6]. Darren Cofer is a Principal Fellow at Collins Aerospace. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin. His area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-integrity systems. His background includes work with formal methods for system and software analysis, the design of real-time embedded systems for safety-critical applications, and the development of nuclear propulsion systems in the U.S. Navy. Dr. Cofer has served as principal investigator on many government-sponsored research programs, developing and using formal methods for verification of safety and security properties. He served on RTCA committee SC-205 developing new certification guidance for airborne software (DO-178C) and was one of the developers of the Formal Methods Supplement (DO-333). He is currently a member of SAE committee G-34 developing certification guidance for the use of machine learning technologies onboard aircraft. Ning Qu is a seasoned technical leader with extensive experience in operating systems, high-performance runtime frameworks, and hardware-software co-design. Currently Ning is Sr. Director of the SkyOS team at NIO, he is leading the development of SkyOS, a suite of platform software (hypervisor, operating systems, and middleware) for Software Defined Vehicles, showcased at NIO IN 2023. Before NIO, Ning managed Waymo's ML Runtime team, significantly contributing to the Jaguar EV launch. At Baidu, he directed the Apollo OS team, developing Cyber RT and leading Baidu's fully driverless launch in 2020. Ning holds a PhD from Peking University and has conducted research at CMU. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://www.linkedin.com/in/darren-cofer-07824a5/ [2] https://www.collinsaerospace.com/ [3] https://www.linkedin.com/in/quning/ [4] https://www.nio.com/ [5] https://sel4.systems/Foundation/Summit/2024/abstracts2024.html#a-inspecta [6] https://sel4.systems/Foundation/Summit/2024/abstracts2024.html#a-software-d… Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Sponsor the seL4 summit in Sydney!
by Announcements about seL4 -- low volume list 07 Jun '24

07 Jun '24

Join Proofcraft and UNSW as a sponsor of this 2024 edition, and support the seL4 technology, like sponsors of last editions did: NIO, Kry10, Collins Aerospace, Technology Innovation Institute, DornerWorks, Horizon Robotics and Xcalibyte. https://events.linuxfoundation.org/sel4-summit/sponsor/ https://sel4.systems/Foundation/Summit/2024/#summit-sponsors

1 0

Welcome UNSW, Bronze sponsor of the seL4 Summit 2024
by Announcements about seL4 -- low volume list 31 May '24

31 May '24

The seL4 Foundation thanks UNSW Sydney [0] for becoming a Bronze sponsor of the seL4 Summit 2024 [1]. seL4 was created by the Trustworthy Systems (TS) [2] team, 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. The seL4 Summit 2024 [1] will take place in Sydney, the hometown of Trustworthy Systems [2] and UNSW [0]. See here [3] if you are interested in sponsoring the seL4 summit 2024. [0] https://www.unsw.edu.au/ [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://trustworthy.systems/ [3] https://events.linuxfoundation.org/sel4-summit/sponsor/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Welcome Proofcraft, Bronze sponsor of the seL4 Summit 2024
by Announcements about seL4 -- low volume list 24 May '24

24 May '24

The seL4 Foundation thanks Proofcraft [0] for becoming a Bronze sponsor of the seL4 Summit 2024 [1]. Founded by the seL4 verification leaders, Proofcraft [0] 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. The seL4 Summit 2024 [1] will take place in Sydney, the hometown of Proofcraft [0]. See [2] if you are interested in sponsoring the seL4 summit 2024. [0] https://proofcraft.systems/ [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://events.linuxfoundation.org/sel4-summit/sponsor/ Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Register for the seL4 summit 2024
by Announcements about seL4 -- low volume list 17 May '24

17 May '24

The seL4 summit 2024 [0] will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: * Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions * Networking with other seL4 experts and enthusiasts * Reception and dinner Register here [1] The early bird cut-off date is 15 September 2024. Local seL4 Sydney-siders will look into organising some informal activities for Monday 14 October 2024, before the summit kicks off, for anyone who wants to join. Gernot may also organise a bush walk for the weekend before the summit. Stayed tuned for more info! [0] https://sel4.systems/Foundation/Summit/2024 [1] https://events.linuxfoundation.org/sel4-summit/ Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Apple joins the seL4 Foundation
by Announcements about seL4 -- low volume list 30 Apr '24

30 Apr '24

The seL4 Foundation is pleased to welcome Apple as our latest member. We are excited to see their interest in seL4 and look forward to seeing their work with seL4. https://sel4.systems/news/#member-apple June -- June Andronick CEO of the seL4 Foundation https://sel4.systems/Foundation

1 0

First Lions OS release
by Announcements about seL4 -- low volume list 16 Apr '24

16 Apr '24

Hello seL4 Community, Trustworthy Systems @UNSW is pleased to announce the release 0.1 of Lions OS, the new, high-performance, highly adaptable, seL4-based OS we are developing from scratch. Aimed embedded/cyberphysical/IoT system, Lions OS is meant to be easily usable (built on top of the Microkit and its SDK) and at the same time designed to be formally verified. Key to achieving all these objectives is a principled, highly-modular design, driven by ruthless adherence to the time-honoured KISS principle, an approach we have already applied successfully to the seL4 Device Driver Framework (sDDF) that is one of foundations of Lions OS. LionsOS is still in its early stages but we are at the point where we have a non-trivial example system and initial documentation. We expect both functionality and documentation to evolve rapidly. We also anticipate significant progress on the verification of Lions OS over the next 12 months. Project overview: https://trustworthy.systems/projects/LionsOS/ Lions OS web site: https://lionsos.org/ Source code (2-clause BSD): https://github.com/au-ts/lionsos Gernot on behalf of Trustworthy Systems

1 0

First release of the seL4 Device Driver Framework
by Announcements about seL4 -- low volume list 09 Apr '24

09 Apr '24

Hello seL4 Community, Trustworthy Systems @UNSW is pleased to announce the release 0.4 of the seL4 Device Driver Framework (sDDF). sDDF is designed for high performance while featuring a highly modular architecture that aims to enable formal verification. For more details see: * the announcement on the developer mailing list https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/6QKUK5… * the document describing the design https://trustworthy.systems/projects/drivers/sddf-design.pdf * the GitHub code and documentation repository https://github.com/au-ts/sddf/releases/tag/0.4.0 Gernot on behalf of Trustworthy Systems

1 0