- Announce - lists.sel4.systems

seL4 Whitepaper Released
by Announcements about seL4 -- low volume list 25 May '20

25 May '20

Dear seL4 community, I’m pleased to announce the seL4 Foundation whitepaper: The seL4 Microkernel – An Introduction This white paper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems. You can download it at https://sel4.systems/About/ Feedback welcome. Gernot PS: Some of you may have seen a pre-release version that was up on the Foundation web site since the Foundation launch. This is the complete version.

1 0

The seL4 Foundation Welcomes Breakaway Consulting!
by Announcements about seL4 -- low volume list 22 May '20

22 May '20

Dear seL4 community, We’re happy to announce the first new member since the launch of the seL4 Foundation: Sydney-based company Breakaway Consulting. Through Founder and Managing Director Ben Leslie, Breakaway comes with 20 years of experience in L4 microkernels and systems based on various L4 kernels. Prior to founding Breakaway, Ben was a student with what is now the TS Group, and then VP Engineering of Open Kernel Labs. Breakaway offers consulting services on architecture, design and implementation of seL4-based systems. Gernot seL4 Foundation Chair

1 0

The seL4 Foundation Welcomes Breakaway Consulting!
by Announcements about seL4 -- low volume list 22 May '20

22 May '20

Dear seL4 community, We’re happy to announce the first new member since the launch of the seL4 Foundation: Sydney-based company Breakaway Consulting. Through Founder and Managing Director Ben Leslie, Breakaway comes with 20 years of experience in L4 microkernels and systems based on various L4 kernels. Prior to founding Breakaway, Ben was a student with what is now the TS Group, and then VP Engineering of Open Kernel Labs. Breakaway offers consulting services on architecture, design and implementation of seL4-based systems. Gernot seL4 Foundation Chair

1 0

The seL4 Foundation is set up and open for business
by Announcements about seL4 -- low volume list 08 Apr '20

08 Apr '20

The Trustworthy Systems group is excited to announce the creation of the seL4 Foundation: https://www.csiro.au/en/News/News-releases/2020/seL4-developers-create-open… Its aim is to provide a neutral and independent organisation to ensure the longevity of seL4, and grow its ecosystem of adopters and contributors. It is set up under the Linux Foundation, which provides a mature and well-known framework for us. My blog provides a detailed explanation of why we are taking this step and what we expect the Foundation to achieve, as well as how community engagement will work: https://microkerneldude.wordpress.com/2020/04/07/the-sel4-foundation-what-a… The seL4 Foundation has a high-profile Board, consisting of individuals with a strong track record of supporting seL4. Besides Gernot Heiser (Chair), June Andronick and Gerwin Klein from Trustworthy Systems, members are: • Dr John Launchbury from Galois, who as Program Manager and later I2O Director at DARPA funded seL4's development and real-world adoption • Sascha Kegreiß, CTO of HENSOLDT Cyber, the company funding the RISC-V port of seL4 and its verification, to protect their highly secure RIC-V based platforms • Dr Daniel Potts, who has over 20 years experience with L4 microkernels, served as VP Engineering of Open Kernel Labs, then CEO of Cog Systems, now Engineering Director at Ghost Locomotion, who use seL4 to protect the safety of self-driving cars. The seL4 Foundation already has a number of members, including major adopters HENSOLDT Cyber and Ghost Systems, and providers of services for seL4, Cog Systems and DornerWorks. Please check the membership page for details and how to join: https://sel4.systems/Foundation/Membership/ We specifically encourage developers to help extend the seL4 ecosystem. If you want to contribute, we suggest looking at the list of userlevel components, and add/enhance/adopt: https://docs.sel4.systems/projects/available-user-components.html Looking forward to working with all of you to take the world's most secure, most advanced, and fastest microkernel OS to the next level! Gernot on behalf of Trustworthy Systems

1 0

The seL4 Foundation is coming!
by Announcements about seL4 -- low volume list 25 Oct '19

25 Oct '19

Dear seL4 community, With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. This was originally announced at the seL4 Summit in the US last month. I apologise for the delay in this posting (side-tracked with various issues). Gernot on behalf of the Trustworthy Systems team

1 0

seL4 Training and ARMv8 virtualization release
by Announcements about seL4 -- low volume list 19 Jan '19

19 Jan '19

All, We at DornerWorks wanted to let the seL4 community know about some seL4 training opportunities that we will be providing on behalf of the seL4 Center of Excellence (CoE). First, we will be providing an introductory webinar that provides an overview and explains the basics of seL4. Webinar: Intro to seL4 Thursday, February 7 11 a.m. EST Register Now: https://dornerworks.clickmeeting.com/intro-to-sel4/register Second, a more advanced two day training will take place on March 7th. This is a paid training that will provide information on seL4, libraries, CAmkES, the proof, and supported platforms. The training will also have hands-on labs that will include configuring CAmkES applications, debugging seL4 applications with GDB, and writing an HTTP server application to serve as a real life example. You can see more information and sign up here: https://www.sae.org/learn/content/c1874/ Finally, we wanted to let people know about our release of our ARMv8 virtualization feature. We recently received approval to release these features to the public. We have a press release providing additional details, a link to the code, and user instructions: https://dornerworks.com/news/new-commits-to-open-source-sel4. Currently, the release is on the DornerWorks github and based on an earlier version of seL4 and its libraries. We are working with Data61 to update to the latest versions and then mainline into the Data61 repositories. This may take some time as we integrate our ARMv8 virtualization code with Data61's ARMv8 virtualization code. Cheers, Robbie VanVossen DornerWorks, Ltd.

1 0

seL4 with proof on x64
by Announcements about seL4 -- low volume list 30 Jul '18

30 Jul '18

Dear seL4 community, it’s my pleasure to announce that even more proofs have become available for seL4. In particular, the Intel x64 version of seL4 now has a functional correctness proof from abstract specification down to the C code. This brings the number of architecture configurations seL4 is verified for up to three (ARMv7, ARMv7 with hypervisor extensions, Intel x64) with a fourth one (RISC-V) in progress. The x64 functional correctness proof does not yet include the fast path, VT-x, or VT-d extensions, nor binary verification or the security proofs we have for ARM, but functional correctness is the core part for all of these other properties and is in itself a big step forward for reliability of the x64 code base. As usual, the proofs and code for seL4 are available on https://github.com/seL4/l4v and https://github.com/seL4/seL4. Enjoy! Gerwin for the Trustworthy Systems Team

1 0

seL4 supports RISC-V
by Announcements about seL4 -- low volume list 18 Apr '18

18 Apr '18

Dear seL4 community, We are extremely pleased to announce that seL4 now supports the RISC-V architecture, making it the third seL4 architecture besides ARM and x86. This is a major step in the seL4 story. For details see https://sel4.systems/pipermail/devel/2018-April/001928.html Gernot for the Trustworthy Systems Team

1 0

Paper describing temporal integrity / MCS scheduling support
by Announcements about seL4 -- low volume list 16 Mar '18

16 Mar '18

A new peer-reviewed paper is now available that describes the motivation, design, implementation and evaluation of our support for temporal integrity enforcement, as required for mixed-criticality systems (MCS). We believe this makes seL4 the first real-world OS with temporal integrity enforcement that goes beyond the simplistic, and highly inefficient, strict time-and-space partitioning (TSP) approach. Furthermore, CPU access is now controlled by capabilities, just like access to spatial resources, resulting in a consistent approach to resource control that we believe is also unique, and will support formal reasoning about temporal system properties. The new model is still in a branch, separate to mainline, until verification is complete, at which time it will supersede the present mainline version. Verification is in progress and should be completed sometime next year (but no guarantees yet). Compared to the earlier announcement (http://sel4.systems/pipermail/announce/2017/000017.html) the model has matured and is now fairly stable, we anticipate no major changes. The paper will appear at next month’s EuroSys conference and is available from https://ts.data61.csiro.au/publications/csiroabstracts/Lyons_MAH_18.abstrac… Gernot for the Trustworthy Systems team

1 0

US seL4 Center of Excellence
by Announcements about seL4 -- low volume list 09 Mar '18

09 Mar '18

We’re pleased to announce that DARPA, in conjunction with Intelligent Automation Inc. and DornerWorks, has created a seL4 Center of Excellence (CoE). The CoE will serve as a USA-based clearing house and ecosystem hub for seL4-related development efforts in the USA. For further information, please contact: Nick Evancich nevancich(a)i-a-i.com Gernot

1 0