benefit of transforming a component
into native code is a reduced footprint
and better performance, removing the
guest operating system and removing
the execution and communication
overhead of the VMM.
Using a native component also increases the potential for applying formal verification and other techniques
for improving the assurance and
trustworthiness of the component. Examples range from full functional verification of handwritten code to cogen-eration of code and proofs, application
of model checking, using type-safe programming languages, and static analysis or traditional thorough testing of a
Due to the isolation provided by
seL4 and the componentized architecture, it becomes possible for components of mixed assurance levels to
coexist in the system without decreasing the overall assurance to that of the
lowest-assurance component or increasing the verification burden of the
lowest-assurance components to that
of the highest-assurance ones.
In our example, we target the VM for
mission manager and ground-station
link, implementing the communications, cryptography, and mission-manager functionality as native components. We leave the camera and WiFi
to run in a VM as an untrusted legacy
component (see Figure 9). This split
was a trade-off between the effort to
reimplement the subsystems and the
benefit gained by making them native
from both a performance and an assurance perspective.
Step 4. Overall assurance. With all
parts in place, the final step is to analyze
the assurance of the overall system based
on the assurance provided by the architecture and by individual components.
In HACMS, the communication,
cryptography, and mission manager
functionality were implemented in a
provably type-safe, domain-specific
language called Ivory, 11 with fixed
heap-memory allocation. Without further verification, Ivory does not give us
high assurance of functional correctness but does give us assurance about
robustness and crash-safety. Given
component isolation, we reason that
these assurances are preserved in the
presence of untrusted components
(such as the camera VM).
code of only part of the original system.
Each VM/VMM combination runs in
a separate CAmkES component that
introduces isolation between the different subsystems, keeping mutually
distrusting ones from affecting each
other, and, later, allowing different assurance levels to coexist.
In general, the partitions follow
the existing software architecture, although a redesign may be necessary
where the software architecture is inadequate for effective isolation.
The partitions will in general need
to communicate with each other, so in
this step we also add appropriate communication channels between them.
For security, it is critically important
that these interfaces are narrow, limiting the communication between
partitions to only what is absolutely
necessary to maximize the benefits of
isolation. Moreover, interface protocols should be efficient, keeping the required number of messages or amount
of data copying minimal. Critically,
seL4’s ability to enable controlled and
limited sharing of memory between
partitions allows a developer to minimize the amount of data copying.
Besides the VMs that represent subsystems of the original system, we also
extract and implement components
for any shared resources (such as the
We can iterate the entire step 2 until
we have achieved the desired granularity of partitions. The right granularity
is a trade-off between the strength of
isolation on the one hand and the increased overhead and cost of communication between partitions, as well as
re-engineering cost, on the other.
In our example we end up with three
partitions: a VM that implements the
ground-station communication functionality running on Linux; another
VM that implements camera-based
navigation functionality (also running
on Linux); and a native component that
provides shared access to the network,
as in Figure 8.
Step 3. Native components. Once
the system has been decomposed into
separate VM partitions, some or all
of the individual partitions can be reimplemented as native components
rather than as VMs. The aim is to significantly reduce the attack surface for
the same functionality. An additional
the glue code proofs
to be artifacts
that do not need
to be examined,
focus on proving
of their handwritten