Transcript Advantages of the approach

ERTOS – Research Projects
seL4 – Secure Embedded L4, L4.verified, Goanna
There are many challenges in building trustworthy
embedded systems. This poster presents projects
that are focused on the trustworthiness of the
microkernel itself.
seL4 Challenges
The seL4 project aims to answer two questions:
1.
seL4
The seL4 project is focused on developing the
kernel programming interface needed to enable
the construction of trustworthy embedded
systems.
L4.verified
This project aims to mathematically prove the
correctness of an implementation of the seL4
programming interface. This provides the
assurance needed to give trustworthy guarantees
about the foundations of the system.
Untrusted
2.
What is an appropriate high-performance
mechanism that can be used to control all
interaction between components in the
system?
What models and mechanisms are
appropriate to precisely control and
account for the consumption of memory in
the microkernel?
Untrusted
Trusted
Application 1
This project is in collaboration with the Formal
Methods program, more details can be found
there.
Application 2
seL4 Microkernel
Hardware
Goanna
This project is applying static analysis to the
source code of the microkernel to identify typical
programming errors in the context of operating
systems code. It is complimentary to L4.verified in
that it helps identify correctness issues in the
system, but using much less resources than
required for full formal verification.
This project is also in collaboration with the
Formal Methods program, more details can be
found there.
Approach
We’re developing an executable specification in
the functional programming language Haskell, and
have coupled the specification with a simulator of
an ARM embedded microprocessor.
Exercisable
Kernel API
ARM
Processor
Simulator
Trusted
Sensitive
Sensitive
Sensitive
App.
Sensitive
App.
App.
App.
Legacy
Legacy
Legacy
App.
Legacy
App.
App.
App.
Linux
Server
Device
Driver
Trusted
Trusted
Trusted
Service
Trusted
Service
Service
Service
Device
Device
Driver
Driver
Embedded OS
L4 Microkernel
Hardware
Advantages of the approach
• It provides a precise method for specifying the
behaviour of the kernel. The result forms part
of the reference manual.
• The specification provides an immediate
implementation for testing – we run the
manual!
• Together with the simulator, it supports the
running of real applications on the
specification itself.
• The specification in Haskell has proved to be
readily amenable to formalisation in
L4.verified, when compared to extracting a
formal model of an implementation in a lowlevel systems language.
• For kernel programmers and designers,
Haskell has proven to be a development
language more readily accessible than typical
formal specification tools.
• Haskell’s high-level nature (and hardware
independence) allows rapid prototyping of
ideas without getting bogged down in
complex, low-level hardware details and
associated debugging.
Expected Results and Benefits
We expect the following results from seL4:
• A high-performance microkernel programming
interface capable of controlling interaction
between all components in the system.
• A programming interface that provides control
of kernel memory allocation to the embedded
operating system running on seL4.
• The combination of the controlled interaction
and precise resource management enables the
microkernel to enforce strong partitioning
guarantees between trusted and untrusted
components.
• Experience in using functional programming as
a prototyping language for operating systems
where formal verification is also a target.
seL4 will provide the foundation for truly
trustworthy embedded systems.
Embedded systems you can trust!