Name
Abstract | ||
|---|---|---|
This paper presents 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 of choreographies and session types. We provide a generic method to instrument the semantics with information flow annotations. Policies are used to specify the admissible flows of information. The main contribution of the paper is a sound type system for statically checking if a system specification ensures an information flow policy. The approach is illustrated with two archetypal examples of distributed and parallel computing systems: a protocol for an identity-secured data providing service and a parallel MapReduce computation. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-23165-5_20 | Lecture Notes in Computer Science |
Keywords | DocType | Volume |
Information flow control,Discretionary access control,Choreographies,Communication protocols,Interaction-oriented computing,Parallel computing,Service-oriented computing,High-performance computing | Conference | 9200 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.36 |
References | Authors | |
14 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alberto Lluch-Lafuente | 1 | 119 | 9.41 |
| flemming nielson | 2 | 1769 | 172.05 |
| Hanne Riis Nielson | 3 | 1719 | 153.77 |