A Type System for Expressive Security Policies

13 years 9 months ago

Download www.cs.cornell.edu

Certiﬁed 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 ﬂexibility of this scheme, so far, compilers that generate certiﬁed 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 welltyped programs with security checks and typing annotations. The resulting programs obey the policies speciﬁed by security automata and can be mechanically checked for safety. This work provides a foundation for the process of automatically generating certiﬁed code for expressive security policies.

David Walker

Real-time Traffic