A Type System for Expressive Security Policies
Abstract
Certified code is a general mechanism for enforcing security
properties. In this paradigm, untrusted mobile 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 type safety properties rather than more general
security properties.
Security automata can specify an expressive collection of
security policies including access control and resource bounds. In
this paper, we describe how to instrument well-typed programs with
security checks and typing annotations. The resulting programs obey
the policies specified by security automata and can be mechanically
checked for safety. This work provides a foundation for the process
of automatically generating certified code for expressive security
policies.
(pdf)