Verified enforcement of stateful information release policies

TitleVerified enforcement of stateful information release policies
Publication TypeJournal Articles
Year of Publication2009
AuthorsSwamy N, Hicks MW
JournalSIGPLAN Not.
Pagination21 - 31
Date Published2009/02//
ISBN Number0362-1340
Keywordsaffine types, certified evaluation, declassification, dependent types, singleton types, state modifying 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 lAIR, a core formalism for a functional programming language. lAIR 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 lAIR meet the requirements of the original AIR policy specification.