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