Architecture

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 base (TCB).

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.

SecCode

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 certificate checker.

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 possible.

As a concrete representation of SecCode, we use a typed variant of ANF (Administrative Normal Form).⁴ ANF has a clean semantics and is well suited to the flow-oriented analysis⁵ 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).⁶ 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.