CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Compositional Information-flow Security for Interactive Systems

Willard Rafnsson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Andrei Sabelfeld (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
27th IEEE Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July 2014 (1063-6900). p. 277-292. (2014)
[Konferensbidrag, refereegranskat]

To achieve end-to-end security in a system built from parts, it is important to ensure that the composition of secure components is itself secure. This work investigates the compositionality of two popular conditions of possibilistic noninterference. The first condition, progress-insensitive noninterference (PINI), is the security condition enforced by practical tools like JSFlow, Paragon, sequential LIO, Jif, Flow Caml, and SPARK Examiner. We show that this condition is not preserved under fair parallel composition: composing a PINI system fairly with another PINI system can yield an insecure system. We explore constraints that allow recovering compositionality for PINI. Further, we develop a theory of compositional reasoning. In contrast to PINI, we show what PSNI behaves well under composition, with and without fairness assumptions. Our work is performed within a general framework for nondeterministic interactive systems.


Article number 6957117
Pdf also available at: http://www.cse.chalmers.se/~andrei/csf14.pdf



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-12-01. Senast ändrad 2016-05-23.
CPL Pubid: 206960

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)