Formal Verification of Language-Based Concurrent Noninterference
AbstractWe perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of non-interference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.
How to Cite
Popescu, A., Hölzl, J., & Nipkow, T. (2013). Formal Verification of Language-Based Concurrent Noninterference. Journal of Formalized Reasoning, 6(1), 1–30. https://doi.org/10.6092/issn.1972-5787/3690
Copyright (c) 2013 Andrei Popescu, Johannes Hölzl, Tobias Nipkow
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy