CAmkES RPC connector. 12, 13 Extending
the proof generator to support other
functional units, as in Figure 5. Using
this platform, systems architects can
design and build seL4-based systems
in terms of high-level components that
communicate with each other and with
hardware devices through connectors
like remote procedure calls (RPCs),
dataports, and events.

Figure 5. CAmkES workflow.

CAmkES

A
B

+

component
 code

 

Generated code. Internally, CAmkES implements these abstractions using seL4’s low-level kernel objects. Each component comprises (at least) one thread, a CSpace, and a VSpace. RPC connectors use endpoint objects, and CAmkES generates glue code to marshal and unmarshal messages and send them over IPC endpoints. Likewise, a dataport connector is implemented through shared memory, shared frame objects present in the address spaces of two components, and optionally restricting the direction of communication. Finally, an event connector is implemented using seL4’s notification mechanism.

capDL

AB

+ proof

Thread Object

CSpace CSpace

Thread

glue
code

Object CNode EP CNode

+ proof
CO
N
T
EX
T

Se
n
d
Rec
ei
v
e

T EX T CON .

..

..

.

VSpace

VSpace

initialized system + proof

Figure 6. RPC-generated code.

AB

CAmkES also generates, in the capDL language, 26 a low-level specification of the system’s initial configuration of kernel objects and capabilities. This capDL specification is the input for the generic seL4 initializer that runs as the first task after boot and performs the necessary seL4 operations to instantiate and initialize the system. 4

f() {
 //glue:
 //  marshalling
 //  seL4_Send(ep,...)
 //  seL4_Recv(ep,...)
 //  unmarshalling
}
 g_stub() {
 //glue:
 //  seL4_Recv(ep,...)
 //  unmarshalling
 //  g_invoke()
 //  marshalling
 //  seL4_Send(ep,...)
 }
 f();
 g() {
 ...

}handwritten generated

seL4

 

In summary, a component platform provides free code. The component architecture describes a set of boxes and arrows, and the implementation task is reduced to simply filling in the boxes; the platform generates the rest while enforcing the architecture.

tomate large parts of system construction without expanding the trusted computing base.

With a traditional component platform, the enforcement process would mean the generated code increases the trusted computing base of the system, as it has the ability to influence the functionality of the components. However, CAmkES also generates proofs.

lent to calling g. The lemma the system generates ensures the invocation of the generated RPC glue code f behaves as a direct invocation of g, as if it were co-located with the caller.

Automated proofs. While generat-
ing glue code, CAmkES produces for-
mal proofs in Isabelle/HOL, following
a translation-validation approach, 30
demonstrating that the generated glue
code obeys a high-level specification
and the generated capDL specification
is a correct refinement of the CAmkES
description. 12 We have also proved that
the generic seL4 initializer correctly
sets up the system in the desired ini-
tial configuration. In doing so, we au-
Developers rarely look at the output
of code generators, focusing instead on
the functionality and business logic of
their systems. In the same way, we in-
tend the glue code proofs to be artifacts
that do not need to be examined, mean-
ing developers can focus on proving the
correctness of their handwritten code.
Mirroring the way a header generated by
CAmkES gives the developer an API for
the generated code, the top-level gener-
ated lemma statements produce a proof
API. The lemmas describe the expected
behavior of the connectors. In the ex-
ample of RPC glue code outlined in Fig-
ure 6, the generated function f provides
a way to invoke a remote function g in
another component. To preserve the
abstraction, calling f must be equiva-
To be useful, the proofs the system
generates must be composable with
(almost) arbitrary user-provided proofs,
both of the function g and of the contexts
where g and f are used. To enable this
composability, the specification of the
connectors is parameterized through
user-provided specifications of remote
functions. In this way, proof engineers
can reason about their architecture,
providing specifications and proofs for
their components, and rely on specifica-
tions for the generated code.

To date, we have demonstrated this process end-to-end using a specific