Blog

It was a great honor to participate 2022 seL4 Summit in Germany. During the Summit, we shared some progress about making seL4 iso 26262 compliant.

As seL4 moves onto automotive applications, having industry standards will be a big step forward for mass adoption. Iso 26262 ASIL-D is well known and established standard for the automotive software supply chain. And MISRA C standard is well suited to making C-language-written software compliant with Iso 26262 ASIL-D standard.

A few critical criteria have to be satisfied for a piece of software system before becoming ASIL-D certified. Two of those are the MISRA coding standard and Code Coverage.

First, MISRA is a critical coding standard for the automotive industry. Making seL4 source code MISRA compliant is a key point to boost the adoption of seL4 in the automotive industry. In this talk, we’ll present a joint work from our partners and us on how to make seL4 code MISRA compliant, who has chosen seL4 as the fundamental kernel for their OS product. We’ll discuss typical implementation issues which don’t follow MISRA guidance, the fixes, and the impacts on proofs.

Second, Code Coverage has been an important metric to measure code quality in the automotive industry. Although seL4 is formally proven, Code Coverage is essential for two reasons. Code Coverage can work orthogonally with formal proof to assure the code quality. The other is Code Coverage rate is the key metric in many certifications. We’d like to share our work regarding measuring seL4 kernel code coverage. We will present the measuring results and ways we have tried to improve the code coverage rate.

During the summit Q&A session, one audience asked why the industry is still stuck with the half-century-old software safety by coding rules inspection instead of using much more sophisticated formal verification but a much more reliable methodology. The main reason is that the automotive industry has a complex and well-established long supply chain. And it’s challenging to abolish the existing altogether and adopt something completely new while the industry is still in fast pace mass production. Therefore, a retrofit approach is much more practical, like making seL4 ISO 26262 compliant as the first cornerstone in industrial adoption.

Lastly, we hope our work can help seL4 make it into the most complex automotive industry and look forward to more adaptation in another field.

Click here to download the presentation.