Type system for expressive security policies

Research output: Contribution to journalConference articlepeer-review

89 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)254-267
Number of pages14
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
StatePublished - 2000
Externally publishedYes
EventPOPL'00 - The 27th ACM SIGPLAN-SIGACT Symposium on Principles og Programming Languages - Boston, MA, USA
Duration: Jan 19 2000Jan 21 2000

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of 'Type system for expressive security policies'. Together they form a unique fingerprint.

Cite this