A Type System for Expressive Security Policies
Abstract
Certified code is a general mechanism for enforcing security properties. In this
paradigm, untrusted agent code carries annotations that allow a host to verify its
trustworthiness. Before running the agent, the host checks the annotations and proves that
they imply the host's security policy. Despite the flexibility of this scheme, so far,
compilers that generate certified code have focused on simple memory and control-flow
safety rather than more general security properties.
Security automata can enforce an expressive collection of security policies including
access control policies and resource bounds policies. In this paper, we show how to take
specifications in the form of security automata and automatically transform them into
signatures for a typed lambda calculus that will enforce the corresponding safety
property. Moreover, we describe how to instrument typed source language programs with
security checks and typing annotations so that the resulting programs are provably secure
and can be mechanically checked. This work provides a foundation for the process of
automatically generating certified code for expressive security policies in a
type-theoretic framework.
(pdf, ps.gz)