Events

During the webinar on the 16th of September 2021, Gernot Heiser, the chairman of the seL4 Foundation, and Yuning Liang, the CEO of Xcalibyte, shared the story of the seL4 microkernel and how it was engineered for cyberphysical systems. The focus of this broadcast was on next-generation automotive operating systems. The webinar was conducted in both English and Chinese.

Professor Gernot spoke about the seL4 microkernel design, implementation, and formal verification, which is used in self-driving cars, medical equipment and other IoT systems. The seL4 microkernel is the world’s first operating system (OS) kernel that inspects and certifies embedded systems for correctness and security. It is used on Arm and RISC-V processors. It is also open source, free-to-use, and is supported by the not-for-profit seL4 Foundation. Xcalibyte is actively cooperating with members of the seL4 Foundation. Their SAST technology is being used by members for the development of high quality and secure code which is a shared vision between the two organisations.

Some of the questions asked during the webinar included:

Q1. Conflicts between security and system performance is common. How do you address this problem? How does seL4 balance safety and performance?

Security and performance can sometimes conflict in terms of priority. The system engineering must rely on the business needs to determine priority. For example, a camera might require performance to take priority over security. I think that for all business needs, if you can construct a good design, you can achieve both security and performance requirements.

Q2. Is R&D for the seL4 being conducted by auto manufacturers in China?

If you look at the membership page of the seL4 Foundation, you will see that there are already many car companies that have been investing resources into R&D. The influx of members from the automotive industry has been rapid during the past 3 months, and we are expecting more cooperation with autonomous driving manufacturers. Any electronic vehicle company is welcome to join the Foundation.

Q3. What are the differences between seL4 and qnx microkernels?

The seL4 microkernel runs faster, has a more robust operating system for security, and its comprehensive certification on ARM and RISC-V processors is still unique. If you can do vertical design, you can achieve better results. The qnx microkernel is already a relatively commercial platform that provides SDK services. The seL4 microkernel is still being researched and designed and will provide SDK services soon.

Watch the full webinar recording, with all the questions and answers.

Download the full webinar deck.