Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference

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.