Verified enforcement of stateful information release policies

11 years 5 months ago
Verified enforcement of stateful information release policies
Many organizations specify information release policies to describe the terms under which sensitive information may be released to other organizations. This paper presents a new approach for ensuring that security-critical software correctly enforces its information release policy. Our approach has two parts. First, an information release policy is specified as a security automaton written in a new language called AIR. Second, we enforce an AIR policy by translating it into an API for programs written in AIR, a core formalism for a functional programming language. AIR uses a novel combination of dependent, affine, and singleton types to ensure that the API is used correctly. As a consequence we can certify that programs written in AIR meet the requirements of the original AIR policy specification.
Nikhil Swamy, Michael Hicks
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Authors Nikhil Swamy, Michael Hicks
Comments (0)