Safety-Critical Systems

Safety-Critical Systems is one activity of the Trustworthy Systems project inside the Software System Research Group (SSRG).

• Aim: Apply the verified seL4 kernel in safety-critical systems.

  The isolation guarantees provided by seL4 are useful in the context of safety critical systems as well as secure systems. The key aim of this activity is to explore the benefit that verified isolation properties can bring to the design, development, and analysis of safety-critical systems.

  As a first step we are developing an seL4-based version of the AUTOSAR componentised automotive software platform that will provide strong isolation between application and system components. We aim to apply existing safety analysis methods, and investigate component-based safety analysis methods to understand how the verified kernel can contribute to provide stronger safety guarantees.

• Latest news: An initial feasibility study of seL4 AUTOSAR has been started in collaboration with Fraunhofer IESE.

• Context: This is the first practical experience with a formally verified kernel in a safety-critical application, and the first step in applying our research to the Reliability aspect of Trustworthy Systems. Developing a real-world seL4-based AUTOSAR system will depend on many of the results of the the Real Time research activity, including low and deterministic interrupt latencies, and real-time scheduling.

• Technical research challenges:

  • Applying seL4 in a real-time environment.
  • Safety analysis with formally verified code, how are traditional safety analyses affected by verified code, can the assurance be expressed or integrated in existing safety frameworks?
  • Dealing with hardware failure modes.
  • Co-development of component-based safety cases and component-based system architectures using seL4's isolation guarantees.

• Contact: Ihor Kuz, ihor.kuz<at>nicta.com.au

People