Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/7394
 Title: A Type System for Expressive Security Policies Authors: Walker, David Keywords: computer sciencetechnical report Issue Date: Apr-1999 Publisher: Cornell University Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1740 Abstract: {\em 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 proof-carrying code have focused on simple memory and control-flow safety rather than more general security properties. {\em 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 secure certified code in a type-theoretic framework. URI: http://hdl.handle.net/1813/7394 Appears in Collections: Computer Science Technical Reports

Files in This Item:

File Description SizeFormat