Dynamic intransitive noninterference revisited

DOI10.1007/S00165-017-0430-6MaRDI QIDQ1688559zbMATH OpenOpenAlexFDO

Authors Sebastian Eggert, Ron van der Meyden

Publication date 8 January 2018

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.05187

zbMATH Keywords

securityinformation flowaccess controlproof techniques

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science) (68P30)

Abstract: The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static intransitive noninterference policies. One of the interpretations focuses on information flows permitted by policy edges, the other focuses on prohibitions implied by absence of policy edges. In general, the two interpretations differ, but necessary and sufficient conditions are identified for the two interpretations to be equivalent. Sound and complete proof techniques are developed for both interpretations. Two applications of the theory are presented. The first is a general result showing that access control mechanisms are able to enforce a dynamic information flow policy. The second is a simple capability system motivated by the Flume operating system.

Recommendations

• Programming Languages and Systems
• A noninterference model for nondeterministic systems
• Symbolic algorithmic verification of intransitive generalized noninterference
• A Policy Model for Secure Information Flow
• Downgrading policies and relaxed noninterference

Cites work

• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• Noninterference for operating system kernels
• Noninterference with Local Policies
• Probabilistic models for the guarded command language
• Programming Languages and Systems
• Programming Languages and Systems
• The shadow knows: refinement and security in sequential programs

Cited in

(12)

• The enforcement of security policies for computation
• Tracking Information Flow in Dynamic Tree Structures
• Analysis of dynamic policies
• Symbolic algorithmic verification of intransitive generalized noninterference
• Characterizing intransitive noninterference for 3-domain security policies with observability
• Mediating secure information flow policies
• Programming Languages and Systems
• Downgrading policies and relaxed noninterference
• Architectural refinement and notions of intransitive noninterference
• A noninterference model for nondeterministic systems
• scientific article; zbMATH DE number 1930751 (Why is no real title available?)
• Just Forget It – The Semantics and Enforcement of Information Erasure

This page was built for publication: Dynamic intransitive noninterference revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688559)