Noninterference for a Practical DIFC-Based Operating System

Author

Krohn, Maxwell ; Tromer, Eran

Author_Institution

CyLab, Carnegie Mellon Univ., Pittsbrugh, PA, USA

fYear

2009

fDate

17-20 May 2009

Firstpage

61

Lastpage

76

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

Internet; Linux; operating systems (computers); security of data; Asbestos; Flume system; Linux operating system; Web applications; communicating sequential processes; decentralized information flow control; noninterference proof; practical DIFC-based operating system; Artificial intelligence; Communication system security; Control systems; Data security; Dynamic programming; Information security; Kernel; Linux; Operating systems; Privacy; Communicating Sequential Processes; Information flow control; covert channels; noninterference;

fLanguage

English

Publisher

ieee

Conference_Titel

Security and Privacy, 2009 30th IEEE Symposium on

Conference_Location

Berkeley, CA

ISSN

1081-6011

Print_ISBN

978-0-7695-3633-0

Type

conf

DOI

10.1109/SP.2009.23

Filename

5207637