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.

• Type: Journal
• Year: 2008
• Where: SIGPLAN
• Authors: Nikhil Swamy, Michael Hicks
• Keywords: AIR Policy, Information Release, Information Release Policy, SIGPLAN 2008, System Software