Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Model-Checking Secure Information Flow for Multi-threaded Programs
verfasst von : Marieke Huisman, Henri-Charles Blondeel
Erschienen in: Theory of Security and Applications
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
This paper shows how secure information flow properties of multi-threaded programs can be verified by model checking in a precise and efficient way, by using the idea of self-composition.
It discusses two properties that aim to capture secure information flow for multi-threaded programs, and it shows how these properties can be characterised in modal
μ
-calculus. For this characterisation, a self-composed model of the program is constructed. More precisely, this is a model that contains two copies of the labelled transition system induced by the program, so that the program is executed in parallel with itself. The self-composed model allows to compare two program executions in a single temporal formula that characterises a secure information flow property.
Both the formula and model are translated into the input language for the Concurrency Workbench model checker. We discuss this encoding, and use it for some practical experiments on several simple examples.