Visible to the public Nontransitive Security Types for Coarse-grained Information Flow Control

TitleNontransitive Security Types for Coarse-grained Information Flow Control
Publication TypeConference Paper
Year of Publication2020
AuthorsLu, Y., Zhang, C.
Conference Name2020 IEEE 33rd Computer Security Foundations Symposium (CSF)
Date PublishedJune 2020
PublisherIEEE
ISBN Number 978-1-7281-6572-1
KeywordsComputer languages, computer security, History, Information Flow Control, Labeling, language-based security, Lattices, noninterference, policy-based governance, pubcrawl, security policies, security types, Software, type systems
Abstract

Language-based information flow control (IFC) aims to provide guarantees about information propagation in computer systems having multiple security levels. Existing IFC systems extend the lattice model of Denning's, enforcing transitive security policies by tracking information flows along with a partially ordered set of security levels. They yield a transitive noninterference property of either confidentiality or integrity. In this paper, we explore IFC for security policies that are not necessarily transitive. Such nontransitive security policies avoid unwanted or unexpected information flows implied by transitive policies and naturally accommodate high-level coarse-grained security requirements in modern component-based software. We present a novel security type system for enforcing nontransitive security policies. Unlike traditional security type systems that verify information propagation by subtyping security levels of a transitive policy, our type system relaxes strong transitivity by inferring information flow history through security levels and ensuring that they respect the nontransitive policy in effect. Such a type system yields a new nontransitive noninterference property that offers more flexible information flow relations induced by security policies that do not have to be transitive, therefore generalizing the conventional transitive noninterference. This enables us to directly reason about the extent of information flows in the program and restrict interactions between security-sensitive and untrusted components.

URLhttps://ieeexplore.ieee.org/document/9155179
DOI10.1109/CSF49147.2020.00022
Citation Keylu_nontransitive_2020