The seL4 Foundation is pleased to welcome Technical University of Munich as Associate Member. The TUM, home of the Isabelle theorem prover used in the verification of seL4, has been a collaborator of the Trustworthy Systems team for many years.
The seL4 Foundation welcomes Second State as a member.
Second State is the creator and maintainer of WasmEdge, a CNCF / Linux Foundation project, which provides a high-performance, lightweight, cross-platform, polyglot, and secure software runtime/sandbox for edge computing. Based on the WebAssembly standard, WasmEdge could be 100 times faster than Docker and hypervisor-based solutions. It supports multiple programming languages, including DSLs, and can be embedded into multiple hosting environments.
Second State is currently porting WasmEdge to seL4. It will be one of the first software runtimes in the seL4 ecosystem. By working with members in the seL4 Foundation, Second State aims to create a real-time software sandbox for automotive and industrial (ie smart factories) applications.
With four new Premium Members joining the seL4 Foundation during the past few weeks, we now welcome their representatives on the seL4 Board. The new Board Members are:
|Dr. Feng Zhou represents Horizon Robotics, where he is a Fellow. He has 15 years of academic as well as 15 years of industry experience in video/image compression & processing, computer vision, artificial intelligence, and ASIC processor architecture.|
|Ian Xu represents Li Auto, where he serves as Vice President, leading Computing Platform design and development including hardware, OS and run-time environment. His experience is in the design and development of networking and wireless communication products.|
|Dr Matthew P. Grosvenor represents Jump Trading, where he specializes on measurement and optimization of high-performance and low-latency network systems. Matthew is a former member of the Trustworthy Systems research group that developed seL4.|
|Qiyan Wang represents NIO, where he leads a global R&D team responsible for Vehicle Operating System, Connected Vehicle Cloud, Vehicle Digital Architecture, Cyber Security, and Vehicle Software Integration and Validation.|
The four new members join five continuing members on the seL4 Board, taking the size of the Board to nine.
The seL4 Foundation welcomes Jump Trading as a Premium Member.
Jump is a research-based organization that is committed to applying cutting edge technology to trading global financial markets. Jump has the full spectrum of technology challenges from machine learning models and HPC at massive scale to cybersecurity and trusted compute requirements that come from being a major market participant in many asset classes. Jump was founded in 1999 and has over 20 global offices including Sydney, Shanghai and Singapore in Asia.
The seL4 Foundation welcomes Horizon Robotics as a Premium Member.
Horizon Robotics is a global leader in the development of artificial intelligence computing platforms. Its mission is to make driving safer and more convenient as drivers transition to intelligent and self-driving vehicles. Founded in Beijing in 2015, Horizon Robotics develops next-generation autonomous driving technology integrating edge-AI processors, algorithms, and toolkits. Horizon has reinvented the automotive-grade AI processor with Horizon Journey SOC and its Brain Processing Unit AI engine (Horizon BPU), to offer the ultimate balance of high-performance, low power, and cost effectiveness for inference at the edge. Horizon's state-of-the-art AI toolkit and model zoo enable developers to optimize and deploy their own neural network models to Journey BPU with ease. Horizon also offers vision perception algorithms to accelerate time-to-production in the dynamic and highly competitive ADAS/AD market.
The evolution of automotive E/E architecture continues rapidly. With complicated hardware consolidation, software consolidation and separation happen simultaneously. “To address the challenges of safety, security and realtime in autonomous software, a fundamental high quality state-of-the-art microkernel is needed. We are looking forward to working with members of seL4 Foundation to build mixed-critical platform and solution for next-generation autonomous driving vehicles.”
The seL4 Foundation welcomes Li Auto Inc. as a Premium Member.
Li Auto is an innovator in China's new energy vehicle market. The Company designs, develops, manufactures, and sells premium smart electric vehicles. Through innovations in product, technology, and business model, the Company provides families with safe, convenient, and refined products and services. Li Auto is a pioneer to successfully commercialize extended-range electric vehicles in China. Its first model, Li ONE, is a six-seat, large premium electric SUV equipped with a range extension system and advanced smart vehicle solutions. The Company started volume production of Li ONE in November 2019 and released the 2021 Li ONE in May 2021. The Company leverages technology to create value for its users. It concentrates its in-house development efforts on its proprietary range extension system, next-generation electric vehicle technology, and smart vehicle solutions. Beyond Li ONE, the Company aims to expand its product line by developing new vehicles, including BEVs and EREVs, to target a broader consumer base.
Li Auto's team will develop a secure highly extensible real-time open platform for next generation self-driving vehicles based on the micro-kernel OS seL4. The platform will enable an ecosystem for third party application developers.
The seL4 Foundation welcomes Xcalibyte as a member.
Xcalibyte's mission is to improve the quality of software by creating easy-to-use tools that help developers build and deploy reliable and secure code. Founded by world-class software experts with decades of experience in compiler optimization and software development, Xcalibyte was established in 2018 and has offices in Shenzhen, Shanghai, Beijing and Hong Kong. Xcalibyte enhances the speed and accuracy of code auditing, code evaluation, and code defect detection. We use advanced static code analysis to help reduce costs, improve productivity, and ensure software developers in China and all over the world have the proper capabilities to develop better, more reliable software.
“As we are actively working with members of the seL4 Foundation, it makes perfect sense for us to be part of the organisation. Our code analysis tools are being used by community members and we are aiming to ensure they develop high quality and secure code.”
The seL4 Foundation welcomes NIO Inc as a Premium member.
NIO is a pioneer in China's premium electric vehicle market. We design, jointly manufacture, and sell smart and connected premium electric vehicles, driving innovations in next generation technologies in connectivity, autonomous driving, and artificial intelligence. Redefining user experience, we provide users with comprehensive, convenient, and innovative charging solutions and other user-centric service offerings. NIO went public in the U.S. in 2018. So far, NIO has launched 3 mass-production vehicle models: ES8, ES6, and EC6, and accumulated deliveries to users are over 120,000. Starting September, NIO will start delivering to users in Norway. NIO invests heavily in in-house R&D to build full-stack cutting-edge technologies around intelligent and autonomous driving EV. Its engineering teams are distributed across the globe, including US, UK, Germany and China.
The Digital Systems department at NIO is missioned to develop the most advanced software platform for the next-generation autonomous driving vehicles in the industry from the ground up. This platform is internally named NIO Vehicle Operating System (NVOS) and based off seL4. It involves solving a wide range of technical challenges, such as seamless app development on heterogeneous hardware chipsets, low-latency & high throughput data processing, powerful AI framework, automobile-grade safety and security guarantee, and complete toolchains to provide Android alike development experience.
The seL4 Foundation has released the following updates:
Various repositories with support libraries and tools have also been updated. Please refer to the following release manifests:
The seL4 Foundation has appointed Dr June Andronick as (part time) CEO. June, already a permanent board member as one of the founders of the seL4 technology, continues to fullfil the role of Treasurer.
The seL4 Foundation welcomes New-Zealand based Kry10 as our latest member.
“We believe that formal methods and proven code is the only viable option for software, whether it is AI, Industrial controls, or really anything else. seL4 is the first, and only real practical kernel to show the world how it should be done,” says Boyd Multerer, CEO and Founder of Kry10.
“At Kry10, we are building a full-featured operating system on top of the seL4 Kernel, along with tooling, services, key management and more. We are aiming at industrial use, but it is suitable for consumer devices and more. Combined with the Erlang BEAM VM for applications, we intend to deliver systems with great security and minimal downtime, even across upgrades.”
It has been heart-warming to see the response of the seL4 community to the news of the dismantlement of the Trustworthy Systems group (TS), creator of seL4.
The seL4 Foundation, as well as its members and ecosystem, want to reinforce their commitment to the success and support of seL4. The TS team will be rebuilding at UNSW and a number of Foundation-endorsed seL4 services providers as well as the newly created Proofcraft verification company are dedicated to support seL4 in the future.
With this recent news, it’s never been more important to work together as a community to support seL4 and the transition of the support and development to the Foundation and its members. People have been asking how to help. Offers of support keep coming. We are looking at various options for sustainable support, with a priority of keeping the team together. There are options on the table that we are exploring that may allow us to do that. Please help us with that, the existing TS team is the best base for stable seL4 support.
In the meantime, here are 4 concrete things that can be done now. Spread the word to people who care about seL4’s future, and contact us if you want to discuss.
The community has expressed a need to more easily find seL4 experts to hire. The Foundations has created a "Jobs in seL4 ecosystem" page where members can post offers for positions with seL4 expertise.
Today, the seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by CSIRO’s Data61, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC.
Within and across open collaboration communities it is essential to work together on areas of mutual interest. RISC-V and seL4 are pleased to announce their progress and their alliances as they join forces to enable stronger overall security, combining security-oriented architecture and operating system design.
“We are excited to be one of the first architectures with secure operating system kernels with such a strong formal verification story,” said Mark Himelstein, CTO of RISC-V International. “RISC-V is continuing to increase the security features that encompass the ISA and the secure seL4 kernel is a natural complement.”
“This is another milestone for seL4, which continues to define the state of the art in OS security,” added Prof Gernot Heiser, Chairman of the seL4 Foundation. “Stronger aligning the two open ecosystems makes a lot of sense.”
“The verified seL4 microkernel forms the core of TRENTOS, our secure operating system for our MiG-V chip, a RISC-V processor with supply chain security”, said Sascha Kegreiß”, CTO of HENSOLDT Cyber GmbH. “This unique combination of hardware and software security can protect critical assets from advanced persistent cyber threats.”
”Translation validation ties all of our verification efforts together,” said Dr Zoltan Kocsis, CSIRO Verification Engineer. “Bringing translation validation to a modern, 64-bit processor presented significant scalability challenges but, in the end, we were able to overcome them.”
For more details on binary verification of seL4 on RISC-V see Gernot's blog: seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an alliance).
The seL4 Foundation is pleased to welcome ETH Zurich as associate member, and is looking forward to further strengthening of ETH's engagement with seL4.
The seL4 Foundation now has an easy way for the general public to support financially the development of seL4 and its open-source ecosystem, using the Linux Foundation's LFX portal.
The seL4 Foundation welcomes Raytheon Technologies as our latest member.
Members of the Raytheon Technologies team have been long-time core participants in the seL4 ecosystem, predating the company’s formation in 2020, which brought together Raytheon Company and United Technologies’ aerospace businesses, Collins Aerospace and Pratt & Whitney. Collins Aerospace 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 Raytheon Technologies team now leads 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.
The seL4 Foundation has commenced providing interim endorsement for trusted service providers for seL4. These may apply to consulting and development services as well as for training. In a first step, the Foundation has given interim endorsement to the following trusted service providers (in the order of approval):
Interim endorsement is intended to lead to full certification; the Foundation will work with interim endorsees and the general membership on developing certification schemes. More detail.
The seL4 Foundation welcomes Penten Pty Ltd as our newest member. Penten is based in Canberra, Australia, and specialises in secure communications technology and artificial intelligence. Penten has been developing seL4-based products for a number of years, some of which are in daily use in multiple defence forces.
There is now a YouTube channel run by the seL4 Foundation. It presently has two playlists, one with the recordings of the seL4 material from this year’s UNSW Advanced Operating Systems course, and one with seL4 Summit talks from Trustworthy Systems. More to come, enjoy.
Announcing the releases of seL4, CAmkES and CapDL under the seL4 Foundation. Below you can find links to release notes with updates to other supporting projects to come before the end of the year. Versioned Releases:
The 3rd seL4 Summit will take place (virtually) on 15–18 November (US East Coast time). The program features a tutorial and 3 days packed with great talks and panels. Presentations will be streamed according to the schedule and available for download right after, and there will be an on-line discussion forum. Registration is only $80US
We’re happy to announce the newest member of the seL4 Foundation: Minneapolis-based company Adventium Labs. Adventium Labs develops solutions for safe and secure software-intensive complex systems, with specialties in separation architectures, model-based system engineering, and mathematical analysis technologies. They are leveraging these capabilities to extend seL4 into safety and security critical industries, including medical devices, defense and commercial avionics, and industrial control.
RISC-V (RV64) is the third ISA with verified seL4. The functional correctness proof of seL4 on the RV64 ISA has completed. Congratulations to the awesome Proof Engineering Team of the Trustworthy Systems group on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. More on this in this blog post.
Yet another contribution of UNSW Sydney to the seL4 community: This year Gernot Heiser is making the seL4-related videos from his UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel. At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site.
The whitepaper "The seL4 Microkernel – An Introduction" 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 here.
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.
The Trustworthy Systems group is excited to announce the creation of the seL4 Foundation. 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 has a high-profile Board consisting of Gernot Heiser (Chair), June Andronick, Gerwin Klein, John Launchbury, Sascha Kegreiß, Daniel Potts. It 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. The seL4 Foundation is set up under the Linux Foundation, which provides a mature and well-known framework.