The overall architecture of the Sec prototype is sketched in the
accompanying figure. Certifying compilers generate a certified
architecture-neutral low-level code, which we term the SecCode. The
execution platform for SecCode comprises the four components in the
dashed box of the figure, all of which is part of the trusted computing
- Certificate Checker
The certificate checker uses a SecCode certificate
to prove that the associated code cannot violate the currently
configured security policy. Where the certificate does not make all
the required guarantees, the certificate checker generates proof
obligations that need to be discharged by use of a reference monitor.
- IRM Rewriter
Proof obligations generated by the certificate checker
may be resolved by an inlined reference monitor (IRM) that is
transparently included into a code component by the IRM rewriter.
- ORM Manager
Alternatively, proof obligations may be resolved by
imposing constraints onto the executing component by out-of-line
reference monitors (such as the underlying operating system). These
constraints are controlled by the ORM manager.
- Code Specialiser
If the certificate checker approves a component for
execution, SecCode is specialised to concrete machine code of the
target architecture by the code specialiser, which is realised as a
load-time or runtime compiler.
The security policy for an instance of the Sec execution platform can be
configured by the user.
Software components executed by the Sec platform come in two flavours:
- Raw components
These are architecture-dependent binaries without
a certificate; i.e., components that for whatever reasons have
not been generated by a certifying compiler. These components may
either be trusted or untrusted. Trusted code, such as a system
library, is treated as a vanilla shared library. In contrast,
untrusted code needs to be completely sandboxed by the ORM manager.
- SecCode components
These are architecture-neutral objects
including a certificate. The trust placed into these components
depends on the associate certificate and is determined by the
SecCode achieves architecture independence by abstracting over the
concrete instruction and register set. Nevertheless, it is a low-level
code at the abstraction level of concrete machine codes to minimise the
semantic gap that specialisation needs to bridge. The goal is to make
specialisation a cheap process that complicates the TCB as little as
As a concrete representation of SecCode, we use a typed variant of ANF
(Administrative Normal Form).4 ANF has a clean semantics and
is well suited to the flow-oriented analysis5 needed to perform register
allocation and the like. We express certificates as type annotations,
for which we will initially investigate the feasibility of LTT (Logical
Type Theory).6 LTT can be considered
a meta type-theory that can be instantiated to different type theories
depending on the properties that need to be asserted and depending on
the required level of expressiveness. This gives us the flexibility to
experiment with different types systems without the need to redo the
complete infrastructure of certificates and certificate checking.
Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen.
The essence of compiling with continuations.
In Proceedings ACM SIGPLAN 1993 Conf. on Programming
Language Design and Implementation, PLDI'93, volume 28(6), pages
ACM Press, 1993.
Manuel M. T. Chakravarty, Gabriele Keller, and Patryk Zadarnowski.
A functional perspective on SSA optimisation algorithms.
In Jens Knoop and Wolf Zimmermann, editors, 2nd International
Workshop on Compiler Optimization Meets Compiler Verification (COCV
2003), volume 82 of ENTCS. Elsevier Science, 2003.
Karl Crary and Joseph C. Vanderwaart.
An expressive, scalable type theory for certified code.
In Proceedings of the 7th ACM SIGPLAN International
Conference on Functional Programming (ICFP '02), number 7. ACM
SIGPLAN, October 2002.
Last modified: Thu May 15 15:17:00 EST 2003