We revisit the classical notion of noninterference for state-based systems, as presented by Rushby in 1992. We strengthen his results in several ways, in particular clarifying the impact of transitive vs. intransitive policies on unwinding. Inspired partially by Mantels observations on unwinding for event systems, we remove the restriction on the unwinding relation to be an equivalence and obtain new insights in the connection between unwinding relations and observational preorders.
Moreover, we make two major extensions. Firstly, we introduce the new notion of nonleakage, which complements noninterference by focusing not on the observability of actions but the information flow during system runs, and then combine it with noninterference, calling the result noninfluence. Secondly, we generalize all the results to (possibilistic) nondeterminism, introducing the notions of uniform step consistency and uniform local respect. Finally, we share our experience using nonleakage to analyze the confidentiality properties of the Infineon SLE66 chip.
Like Rushbys, our theory has been developed and checked using a theorem prover, so there is maximal confidence in its rigor and correctness.
| David von Oheimb |
| Siemens AG, Munich |
| Date: | Wed Oct 6 2004 |
| Time: | 10.30am - 12:00pm |
| Location: | Room 1010, Level 10, Applied Science Building, UNSW Kensington campus |
Last updated by tbourke at Fri Oct 8 09:56:53 2004 GMT+1000