Safety Certification with the Open Source Microkernel-Based Operating System L4Re

Safety Certification with the Open Source Microkernel-Based Operating System L4Re

연구 분야: Verification

학회: International Conference on Computer Safety, Reliability, and Security

We report on recent efforts to certify the open-source operating system framework L4Re [2] and its commercial variant EB corbos Hypervisor [1]. Certification is carried out in adherence to ISO 26262 and targets an Automotive Safety Integrity Level B (ASIL-B). Unlike existing work on OS verification [3], the presented work discusses how a complete software system can be taken to certification. The paper identifies challenges arising from the re-use of open-source legacy software in a safety context and provides strategies for its certification without re-implementing major parts of the system. To achieve this, the paper introduces a new safety architecture based on the L4 style of “system-call forwarding”, hierarchical memory management and configuration-based setup of inter-process communication relations. Collectively, the proposed innovations isolate safety applications from hidden errors in components not developed in adherence to the ISO 26262, in this case the feature-rich software stack implementing the L4Re userland.