Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Specification and Checking of Software Contracts for Conditional Information Flow
verfasst von : Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David Greve
Erschienen in: FM 2008: Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Information assurance applications providing
Multi-Level Secure
(MLS) solutions must often implement 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, used to develop such applications, are capable of capturing only unconditional information flows. Motivated by the need to better formally specify and certify MLS applications in industrial contexts, we present an enhancement of the SPARK system that enables specification, inference, and compositional checking of conditional information flow contracts. We report on the use of this framework for a collection of SPARK examples.