- Announce - lists.sel4.systems

Training day @ UNSW
by Announcements about seL4 -- low volume list 23 Aug '24

23 Aug '24

As an addition to the seL4 summit 2024, we are offering an extra day on the Friday 18 October 2024 at UNSW for training[0] , on Lions OS and Rust. 18 October 2024 Room G10 in the Electrical Engineering Building [1] **Registration for training day** Register for the LionsOS, Rust or both tutorials [2] Training day @ UNSW is free, but please register by 15 September 2024 so that we can account for numbers. **Using LionsOS** Ivan Velickovic, UNSW Sydney 10:00 - 12:30 LionsOS is a new Operating Systems developed at Trustworthy Systems aimed at embedded, IoT, and cyberphysical systems. LionsOS is based on the seL4 Microkit and is desgined to formally verifiable, performant, and adaptable to a wide class of use-cases. LionsOS, by design, is not a conventional OS and hence it may be overwhelming for users who want to get started and are not familiar with the ideas and goals of LionsOS. This hands-on tutorial aims to ease people into creating a LionsOS-based system. We will be using the components and tools provided by LionsOS to, step-by-step, transform a minimal boilerplate system to a functional system involving various drivers, virtual machines and other components. What to bring: Your own laptop **Using Rust in seL4 Userspace** Nick Spinale, Colias Group, LLC 14:00 - 16:30 Rust logoRust has been an officially supported language for use in seL4 userspace since last year's summit. In this workshop, participants will be led through a tutorial that demonstrates how to leverage Rust and its ecosystem to rapidly build memory-safe components for seL4-based systems. This tutorial will cover a range of scenarios, including Microkit protection domains as well as building on seL4 directly. What to bring: Your own laptop with Docker installed. [0] https://sel4.systems/Foundation/Summit/2024/#summit-training-day [1] https://www.learningenvironments.unsw.edu.au/physical-spaces/electrical-eng… [2] https://form.jotform.com/242312058251850 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

Check out the seL4 summit 2024 program and abstracts
by Announcements about seL4 -- low volume list 19 Aug '24

19 Aug '24

We have an exciting line-up of speakers [0] and talks [1] for the seL4 summit 2024 [2]. There will be a wide variety of presentations, including technical discussions, research and development and experience reports of seL4 in the field. Register here [3] for the seL4 summit 2024. We look forward to seeing you in Sydney, in October! [0] https://sel4.systems/Foundation/Summit/2024/program [1] https://sel4.systems/Foundation/Summit/2024/abstracts2024 [2] https://sel4.systems/Foundation/Summit/2024/ [3] https://events.linuxfoundation.org/sel4-summit/register/ 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 Collins, Bronze sponsor of the seL4 Summit 2024
by Announcements about seL4 -- low volume list 16 Aug '24

16 Aug '24

The seL4 Foundation thanks Collins Aerospace [0] for becoming a Bronze sponsor of the seL4 Summit 2024 [1]. Collins Aerospace [0], part of seL4 Foundation member Raytheon Technologies [2], has been a long-time core participant in the seL4 ecosystem. seL4 summitIt was a prime contractor in the DARPA HACMS program, which demonstrated the seL4-based incremental cyber retrofit of autonomous military vehicles. This was a major milestone in the growth of seL4, demonstrating that it protects against cyber attacks on real systems in operation. The same team also led the follow-on DARPA CASE program, aiming at designed-in cyber-resiliency, including the seL4-based framework for verified initialisation and configuration of systems architectures. Collins Aerospace is now leading the INSPECTA team as part of DARPA's PROVERS program, which aims at developing formal methods tools to guide software engineers through designing proof-friendly software systems and reduce the proof repair workload. See [3] if you are interested in sponsoring the seL4 summit 2024. [0] https://www.collinsaerospace.com/ [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://www.rtx.com/ [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 TII, Bronze sponsor of the seL4 Summit 2024
by Announcements about seL4 -- low volume list 14 Aug '24

14 Aug '24

The seL4 Foundation thanks TII [0] for becoming a Bronze sponsor of the seL4 Summit 2024 [1]. The Technology Innovation Institute’s (TII) Secure Systems Research Centre (SSRC) aims to drive end-to-end security and resilience in cyber-physical and autonomous systems that will ensure safety. The research center adopts an applied research approach, emphasizing practical applications. By employing seL4 as both a microkernel and a hypervisor, SSRC seamlessly aligns its dedication to security with the foundational technology crucial to achieving its objectives. This critical technology forms the cornerstone of secure software stacks for diverse edge devices, including secure communicators and drones. TII’s research not only contributes to but propels the evolution of cutting-edge high-end edge device environments. TII’s SSRC focus centers on resilience, isolation, trust, and security, all with the intention of fostering a more secure digital landscape. See [2] if you are interested in sponsoring the seL4 summit 2024. [0] https://www.tii.ae/ [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

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