Formal verification of language-based concurrent noninterference

Article

Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formal verification of language-based concurrent noninterference. Journal of Formalized Reasoning. 6 (1), pp. 1-30. https://doi.org/10.6092/issn.1972-5787/3690
TypeArticle
TitleFormal verification of language-based concurrent noninterference
AuthorsPopescu, A., Hölzl, J. and Nipkow, T.
Abstract

We 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 noninterference 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.

Research GroupFoundations of Computing group
JournalJournal of Formalized Reasoning
ISSN1972-5787
Publication dates
Print27 Aug 2013
Publication process dates
Deposited27 Apr 2015
Output statusPublished
Publisher's version
Copyright Statement

Full text: Copyright (c) 2013 Andrei Popescu, Johannes Hölzl, Tobias Nipkow.
Creative Commons License: This work is licensed under a Creative Commons Attribution 3.0 International License - http://creativecommons.org/licenses/by/3.0/

Digital Object Identifier (DOI)https://doi.org/10.6092/issn.1972-5787/3690
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/85207

Log in to edit

Download files

Publisher's version
3690-10209-1-PB.pdf

Restricted files

File

  • 19
    total views
  • 7
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as