Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference

Select |




Print


Murray, Toby; Sison, Robert; Pierzchalski, Edward; Rizkallah, Christine

Murray, Toby; Sison, Robert; Pierzchalski, Edward; Rizkallah, Christine


2016-06-28


Conference Material


IEEE Computer Security Foundations Symposium


Lisbon, Portugal


417-431


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.


Dependent security type systems, secure refinement, Isabelle/HOL


http://csf2016.tecnico.ulisboa.pt/


nicta:9213


Murray, Toby; Sison, Robert; Pierzchalski, Edward; Rizkallah, Christine. Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. In: IEEE Computer Security Foundations Symposium; Lisbon, Portugal. 2016-06-28. 417-431.



Loading citation data...

Citation counts
(Requires subscription to view)