RIF: Reactive information flow labels

Article type: Research Article

Authors: Kozyri, Elisavet^a | Schneider, Fred B.^{b; *}

Affiliations: [a] School of Engineering and Applied Sciences, Harvard University, MA, USA. E-mail: [email protected] | [b] Department of Computer Science, Cornell University, NY, USA. E-mail: [email protected]

Correspondence: [*] Corresponding author. E-mail: [email protected].

Abstract: Restrictions that a reactive information flow (RIF) label imposes on a value are determined by the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as a fitting security policy, because noninterference is not suitable. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: RIF automata are general-purpose and based on finite-state automata; κ-labels concern confidentiality in programs that use cryptographic operations.

Keywords: Reclassification, piesewise noninterference, type system, RIF automaton, κ-label

DOI: 10.3233/JCS-191316

Journal: Journal of Computer Security, vol. 28, no. 2, pp. 191-228, 2020