The seL4 Foundation is pleased to welcome the Technology Innovation
Institute.
Technology Innovation Institute’s (TII) Secure Systems Research Centre (SSRC) has obtained seL4 Foundation membership that will enable the Centre to participate in and contribute to driving the open source for a robust hypervisor technology. The critical technology will help build a secure software stack for many edge devices, such as secure communicators and drones. Through the membership, TII will research, contribute to and advance next-generation high-end edge device environments that focus on resilience, isolation, trust, and security.
In July, we announced that the assurance story for seL4 on RISC-V keeps building, with the completion of the proof that seL4 enforces integrity, following the earlier proofs of functional correctness and binary correctness for seL4 on RISC-V.
The next step in the assurance stack is now also completed for RISC-V with the proof that seL4 enforces confidentiality, i.e. that seL4 provably enforces information flow control, when it is correctly configured to do so.
"This completes the 3 big CIA security properties for seL4 on RISC-V: confidentiality, integrity and availability. While integrity ensures there is no unauthorised interference with private data, confidentiality ensures there is no unauthorised access to private data”, says Gernot Heiser, chair of the seL4 Foundation.
We thank Ryan Barry of the Trustworthy Systems group at UNSW, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work. The proof is available on GitHub.
The seL4 Foundation has awarded Interim
Endorsement to Proofcraft as a
Trusted Service Provider for commercial support, verification projects,
training and consulting on formal verification of seL4 and seL4-based
systems. More on our services and products
page.
Following CSIRO’s abandoning of Trustworthy Systems (TS) and the
seL4 technology TS developed, the seL4 community and the seL4
Foundation have grown a lot. This has led to concerns that the
broader participation might have the potential to undermine the
integrity of seL4. In his latest
blog, Gernot
explains why there is no reason for such concern. seL4's open
governance and technical leadership is based on technical merit
and established trust, not money.
The seL4 Foundation is pleased to welcome Proofcraft.
Founded by the seL4 verification leaders, Proofcraft 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!
Xcalibyte, a member of the seL4 Foundation, is hosting a webinar on Sep 16,
2021, given by Gernot Heiser, seL4 Foundation Chairman & Scientia Professor,
UNSW Sydney, and Yuning Liang, CEO & co-founder, Xcalibyte. The topic will be
‘The seL4 Microkernel: Proved Security for Cyberphysical Systems’.
To register: http://xcalscan.mikecrm.com/Uw4y9HU.
The seL4 Foundation thanks Ghost for its
generous contribution. Ghost's commitment strengthens the seL4
Foundation's mission to continue advancing the ecosystem, the code
base, and the verification efforts of seL4, the world's most
advanced and highly assured operating-system kernel.
As a founding member of the Foundation, Ghost is developing self-driving cars using seL4, aiming to make the first formally proven safety-critical system on the road into a reality for millions of drivers.
We warmly thank Ghost for its continued support!
The seL4 Foundation has awarded interim endorsement to the
seL4-based TRENTOS
secure operating system from Foundation member HENSOLDT
Cyber. This is the first time a product is endorsed, and marks a
new milestone for the Foundation and the growth of the seL4
ecosystem.
HENSOLDT Cyber's training module for TRENTOS has also received interim endorsement, which constitutes another milestone as the first endorsed training provided from outside the Trustworthy Systems group.
Details on interim-endorsed services and products are on our services and products page.
The seL4 Foundation
welcomes Lotus Cars.
Lotus is a leader in the Global Premium Sport Car market. We stand out as a brand dedicated to pure driving experience. Committed to advancing technology with precision and passion, Lotus continues to spearhead research into areas such as autonomous driving, connectivity, intelligence, electrification. Emira, Evija, Evora are representative models that in recent years drive Lotus’ world-wide reputation. Going forward, Lotus’ approach will be based on the principle of “EAS-IP” (Electrify, Amplify, Simplify, Intensify and Personify), a globally R&D strategy, and excellent autonomous driving solutions to create a novel, technology-based driving experience for future global users.
In joining the seL4 Foundation, Lotus is committed to the development and deployment of the seL4 microkernel in the field of autonomous driving, advance Lotus' automotive operating system to meet the overall functional safety goals of the system, and realize the launch of safe and reliable autonomous driving products.
On 6 August DARPA brought the
“SMACCMcopter”
to DEF CON
and invited the assembled hacker elite to attack it. The
SMACCMcopter was the research vehicle of the Air Team at
DARPA's HACMS
program. The Trustworthy Systems
team worked
with project partners to deploy seL4 and leverage formal
methods to protect the drone from cyber attacks.
The result? Predictably, sel4's verified security enforcement defeated the hackers comprehensively. As DARPA said: “Formal methods FTW!”
The seL4 Foundation is pleased to
welcome Kansas State
University as Associate Member. 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.
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!
The assurance story for seL4
on RISC-V keeps building. We first
formally proved functional
correctness: that
the seL4 C code on RISC-V platforms behaves exactly as its
specification says. 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. 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 of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work.
See Gernot's blog for more details. The proof is available on GitHub.
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:
- seL4 v12.1.0: release, change log
- CAmkES v3.10.0: release, change log
- CapDL v0.2.1: release, change log
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.
-
donations and crowdfunding, in particular towards the
“continuity project”.
https://sel4.systems/Foundation/Support/
seL4 crowdfunding page
The crowd-funding platform works for large and small financial contributions, and contributions can be dedicated to specific topics. Fans are always welcome to contribute and show the continued support to seL4 :), but if you know of companies that would like to show financial support without a longer-term commitment, this is a quick and easy mechanism to do so.
We have set up a dedicated “continuity project” to raise funds specifically targeted to the transition of the infrastructure (testing, boards etc) and the immediate support needs (maintenance of all configurations, libraries, releases etc) to the Foundation. All donors of $1,000 and above will be listed on the page above. -
get more members signed up to the Foundation.
https://sel4.systems/Foundation/Join/
A push to get more organisations joining in the coming weeks will be a clear message of the strong support to seL4 and will provide the necessary funds funds to transition more support to the Foundation. Longer term, membership helps deliver on the Foundation’s vision to increase usability, exposure, support, education, participation, and verification of seL4. Join or help spreading the word to join to your partners and customers. -
in-kind offer of expertise.
The number of seL4 experts is growing. Active participation and especially support for new users and beginners on Discourse (https://sel4.discourse.group) and the mailing list will help keep the community active. Likewise contributions to reviews and discussion on GitHub on pull requests and issues will help to keep things moving. The focus has shifted away from just D61 contributions in the past year already, now is the time to keep the momentum up. The TS team and people in the technical steering committee are working on moving testing and verification infrastructure to UNSW. This will include opening up the infrastructure such that members can contribute hardware tests. We will send more information about this in the next few weeks. Please contact Gerwin as the TSC chair if you are interested in this or have additional ideas how to help.
We were gearing up for the next seL4 release. This might be slightly delayed by the infrastructure move, but if everything comes together as planned the release will go ahead. -
jobs in the seL4 ecosystem.
https://sel4.systems/Foundation/Jobs/
While some expertise is needed to be kept within the Foundation, it is also important to keep it within the community. We have just set up a page for members to post jobs related to seL4. This will help match seL4 experts to organisations willing to build upon, develop or support seL4. Contact foundation@sel4.systems to post on that page.
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 extended Interim Endorsement as Trusted
Service Provider to HENSOLDT
Cyber, for consulting and development services for seL4-based
systems. More on:
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.