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.