Intransitive noninterference in nondeterministic systems

Intransitive noninterference in nondeterministic systems

Kai Engelhardt, Ron van der Meyden

16 October 2012

This paper addresses the question of how TA-security, a semantics for intransitive information-flow policies in deterministic systems, can be generalized to nondeterministic systems. Various definitions are proposed, including definitions that state that the system enforces as much of the policy as possible in the context of attacks in which groups of agents collude by sharing information through channels that lie outside the system. Relationships between the various definitions proposed are characterized, and an unwinding-based proof technique is developed. Finally, it is shown that on a specific class of systems, access control systems with local non-determinism, the strongest definition can be verified by checking a simple static property.


Venue : N/A

External Link: http://www.informatik.uni-trier.de/~ley/db/conf/ccs/ccs2012.html#EngelhardtMZ12