Making Linux Fly: Towards Certified Linux Kernel


Speaker: Wentao Zhang, PhD student at University of Illinois Urbana-Champaign and Steven H. VanderLeest, Technical Fellow at The Boeing Company

Although the Linux operating system has been used widely in many industries, adoption in aerospace has been slow due to the rigorous assurance evidence required as part of flight certification. The guidance for commercial flight software in most of the world is RTCA DO-178C, which identifies five progressively more rigorous levels of assurance. Providing the software life cycle data outlined by DO-178C is a daunting task for software as large and complex as Linux. In this project we focus on three objectives from DO-178C related to code coverage — the fraction of the source code that is exercised by testing. The three types of code coverage in DO-178C are statement coverage, decision coverage, and Modified Condition/Decision Coverage (MC/DC). The last of these, MC/DC, is only required for Software Level A, the highest level of assurance. For operating system kernels like Linux, measuring code coverage is challenging because of the unique execution environment compared to user space. Measuring MC/DC is even harder given the intricacy of the metric and limitations of tools. We share our experience in measuring Linux kernel’s code coverage, with an emphasis on MC/DC. We describe how we have enabled measuring Linux kernel’s MC/DC for the first time, by enhancing both the toolchain and the kernel itself. We also discuss the generalizability of our approach across different kernel versions and opportunities for improving coverage with kernel testing suites like KUnit and kselftest.