Trustworthy Systems

Compositional verification and refinement of concurrent value-dependent noninterference

Authors

Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

NICTA\ UNSW\ University of Melbourne

Abstract

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

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

Download