Skip to main content


Compositional verification and refinement of concurrent value-dependent noninterference


Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah



University of Melbourne


Value-dependent noninterference allows the classification of program variables to depend on the contents of other variables, and therefore is able to express a range of data-dependent security policies. However, so far its static enforcement mechanisms for software have been limited either to progress- and termination-insensitive noninterference for sequential languages, or to concurrent message-passing programs without shared memory. Additionally, there exists no methodology for preserving value-dependent noninterference for shared memory programs under compositional refinement. This paper presents a flow-sensitive dependent type system for enforcing timing-sensitive value-dependent noninterference for shared memory concurrent programs, comprising a collection of sequential components, as well as a compositional refinement theory for preserving this property under componentwise refinement. Our results are mechanised in Isabelle/HOL.

BibTeX Entry

    author           = {Murray, Toby and Sison, Robert and Pierzchalski, Edward and Rizkallah, Christine},
    month            = jun,
    year             = {2016},
    keywords         = {dependent security type systems, secure refinement, isabelle/hol},
    title            = {Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference},
    booktitle        = {IEEE Computer Security Foundations Symposium},
    pages            = {417-431},
    address          = {Lisbon, Portugal}