Sec >Sec architecture<

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


4 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 237-247. ACM Press, 1993.
5 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.
6 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.


< Contact: chak@cse.unsw.edu.au Last modified: Thu May 15 15:17:00 EST 2003 >