- Announce - lists.sel4.systems

Proof that seL4 enforces integrity established for RISC-V
by Announcements about seL4 -- low volume list 04 Aug '21

04 Aug '21

The assurance story for seL4 on RISC-V <https://riscv.org/>keeps building. We first formally proved functional correctness: that the seL4 C code on RISC-V platforms behaves exactly as its specification says <https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/>. We then established binary correctness: that the machine code running on the processor behaves exactly as the C code, and by extension, as the specification says <https://microkerneldude.wordpress.com/2021/05/05/sel4-on-risc-v-verified-to…>. We now have established the crucial integrity property for seL4 on RISC-V: that the specification, and by extension the kernel binary, prevents an application running on top from modifying data without authorisation. In seL4 speak: seL4 provably enforces capability-based access control. “The integrity property is crucial for security: it is key to enforce the isolation of components running on top of the kernel”, says Gerwin Klein, seL4 verification expert and chair of the seL4 Foundation technical steering committee. “This is what allows critical components, like the network controller that has access to software-controlled brakes in a modern car, to securely run alongside untrusted software, like the entertainment system. With integrity proved, you know that an attack on or from a vulnerable untrusted part of the system cannot compromise the critical parts.” Integrity had been proved in the original seL4 verification on the Arm32 architecture. It is now also established for RISC-V architecture, making it the only 64-bit architecture that has an OS with such a comprehensive verification and security story. We thank Ryan Barry <https://trustworthy.systems/people/?cn=Ryan+Barry> of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council <https://www.arc.gov.au/> through grant DP190103743 which has enabled this work. See Gernot's blog <https://microkerneldude.wordpress.com/2021/08/04/sel4-integrity-enforcement…> for more details. The proof is available on GitHub <https://github.com/seL4/l4v/tree/master/proof/access-control>. June

1 0

Kansas State Joins the seL4 Foundation
by Announcements about seL4 -- low volume list 03 Aug '21

03 Aug '21

We are pleased to welcome Kansas State University as Associate Member of the se4 Foundation. KSU has for years been collaborating for years on seL4-based projects with a number of Foundation members under multiple DARPA projects and we are looking forward to their continued involvement. Welcome KSU! Gernot

1 0

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

29 Jul '21

On 29th 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. We obviously had a party then, and have since celebrated its anniversary, calling it, tongue-in-cheek, “International Proof Day”. On the fifth anniversary we open-sourced seL4, which was another major milestone, which we referred to as “seL4 Freedom Day”. Today marks the 12th anniversary of the proof, and the 7th anniversary of open-sourcing, and from now on we’ll refer to the date simply as "seL4 Day”. The seL4 community is now definitely global. Still we would normally have a physical party in Sydney, but won’t be able to due to the renewed Covid-19 restrictions – so we’ll all be remote ;-) Happy seL4 day everyone! A virtual toast to you all, and a big thank-you to all for your continued support! June -- June Andronick CEO of the seL4 Foundation https://sel4.systems/Foundation

1 0

TU Munich joins the seL4 Foundation
by Announcements about seL4 -- low volume list 20 Jul '21

20 Jul '21

The seL4 Foundation is pleased to welcome Technical University of Munich as an 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. Gernot

1 0

Second State joins the seL4 Foundation
by Announcements about seL4 -- low volume list 08 Jul '21

08 Jul '21

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 on 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. Gernot

1 0

seL4 Foundation Welcomes New Board Members
by Announcements about seL4 -- low volume list 07 Jul '21

07 Jul '21

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 representing Horizon Robotics Ian Xu representing Li Auto Dr Matthew P. Grosvenor representing Jump Trading Qiyan Wang represents NIO More at https://sel4.systems/news.pml.html For the complete seL4 Board see https://sel4.systems/Foundation/Board.html Welcome aboard, Feng, Ian, Matt and Qiyan! Gernot

1 0

The seL4 Foundation welcomes Jump Trading as a Premium member
by Announcements about seL4 -- low volume list 29 Jun '21

29 Jun '21

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. Welcome on board! Gernot

1 0

The seL4 Foundation welcomes Horizon Robotics as a Premium member
by Announcements about seL4 -- low volume list 25 Jun '21

25 Jun '21

About Horizon: 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.” Welcome on board! Gernot

1 0

seL4 jobs page
by Announcements about seL4 -- low volume list 24 Jun '21

24 Jun '21

The Foundation has created a "Jobs in the seL4 ecosystem" page where members can post offers for positions with seL4 expertise: https://sel4.systems/Foundation/Jobs.html. Our newly joined premium member NIO just posted some openings for seL4 experts. Gernot

1 0

The seL4 Foundation welcomes Li Auto as a Premium member
by Announcements about seL4 -- low volume list 23 Jun '21

23 Jun '21

Li Auto (NASDAQ:LI) 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. Welcome on board! Gernot

1 0