Sciweavers

Share
FM
2008
Springer

Specification and Checking of Software Contracts for Conditional Information Flow

9 years 8 months ago
Specification and Checking of Software Contracts for Conditional Information Flow
Abstract. Information assurance applications built according to the MILS (Multiple Independent Levels of Security) architecture often contain information flow policies that are conditional in the sense that data is allowed to flow between system components only when the system satisfies certain state predicates. However, existing specification and verification environments, such as SPARK Ada, used to develop MILS applications can only capture unconditional information flows. Motivated by the need to better formally specify and certify MILS applications in industrial contexts, we present an enhancement of the SPARK information flow annotation language that enables specification, inferring, and compositional checking of conditional information flow contracts. We report on the use of this framework for a collection of SPARK examples.
Torben Amtoft, John Hatcliff, Edwin Rodrígu
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FM
Authors Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David Greve
Comments (0)
books