Discretionary Information Flow Control for Interaction-Oriented Specifications

In this talk we present an approach to specify and check discretionary information flow properties of concurrent systems. The approach is inspired by the success of the interaction-oriented paradigm to concurrent systems (cf. choreographies, behavioural types, protocols,...) in providing behavioural guarantees of global properties such as deadlock-absence. We show how some information flow properties are easier to formalise and check on a global interaction-oriented description of a concurrent system rather than on a local process-oriented description of the components of the system. We use a simple choreography description language adapted from the literature. We provide a generic method to instrument the semantics with information flow annotations. Information flow policies are used to specify the admissible flows of information. We present a sound type system for statically checking if a system specification ensures an information flow policy.