Noninterference for a Practical DIFC-Based Operating System
- 1 May 2009
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 4 (10816011) , 61-76
- https://doi.org/10.1109/sp.2009.23
Abstract
The Flume system is an implementation of decentralized information flow control (DIFC) at the operating system level. Prior work has shown Flume can be implemented as a practical extension to the Linux operating system, allowing real Web applications to achieve useful security guarantees. However, the question remains if the Flume system is actually secure. This paper compares Flume with other recent DIFC systems like Asbestos, arguing that the latter is inherently susceptible to certain wide-bandwidth covert channels, and proving their absence in Flume by means of a noninterference proof in the communicating sequential processes formalism.Keywords
This publication has 18 references indexed in Scilit:
- Quantitative information flow as network flow capacityPublished by Association for Computing Machinery (ACM) ,2008
- What is intransitive noninterference?Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Some new attacks upon security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- LOMAC: Low Water-Mark integrity protection for COTS environmentsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Process algebra and non-interferencePublished by Institute of Electrical and Electronics Engineers (IEEE) ,1999
- A framework for model-checking timed CSPPublished by Institution of Engineering and Technology (IET) ,1999
- Trust in the λ-calculusPublished by Springer Nature ,1995
- Multilevel security in the UNIX traditionSoftware: Practice and Experience, 1992
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982
- A lattice model of secure information flowCommunications of the ACM, 1976