This paper argues that Haigh and Young’s definition of noninterference for intransitive security policies admits information flows that are not in accordance with the intuitions it seeks to formalize. Several alternative definitions are discussed, which are shown to be equivalent to the classical definition of noninterference with respect to transitive policies. Rushby’s unwinding conditions for intransitive noninterference are shown to be sound and complete for one of these definitions, TA-security. Access control systems compatible with a policy are shown to be TA-secure, and it is also shown that TA-security implies that the system can be interpreted as an access control system.
A.Askarov and S.Chong, Learning is change in knowledge: knowledge-based security for dynamic policies, in: Proc. IEEE Computer Security Foundations Symposium, 2012, pp. 308–322.
2.
A.Askarov and A.Sabelfeld, Gradual release: unifying declassification, encryption and key release policies, in: Proc. IEEE Symposium Security and Privacy, 2007, pp. 207–221.
3.
M.Backes and B.Pfitzmann, Intransitive non-interference for cryptographic purposes, in: Proc. IEEE Symp. Security and Privacy, 2003, pp. 140–152.
4.
D.E.Bell and L.J.La Padula, Secure computer system: unified exposition and multics interpretation, Technical Report ESD-TR-75-306, Mitre Corporation, Bedford, MA, March 1976.
5.
W.R.Bevier and W.D.Young, A state-based approach to noninterference, in: Proc. IEEE Computer Security Foundations Workshop, 1994, pp. 11–21.
6.
A.Bossi, C.Piazza and S.Rossi, Modelling downgrading in information flow security, in: Proc. IEEE Computer Security Foundations Workshop, 2004, pp. 187–201.
7.
S.Chong and A.C.Myers, Security policies for downgrading, in: 11th ACM Conf. Computer and Communications Security (CCS), October 2004, 2004.
8.
S.Chong and R.van der Meyden, Deriving epistemic conclusions from agent architecture, in: Proc. Conf. Theoretical Aspects of Knowledge and Rationality, ACM Digital Library, 2009, pp. 61–70.
9.
S.Chong and R.van der Meyden, Using architecture to reason about information security, in: Proc. Layered Assurance Workshop, 2012, pp. 1–12, available at: http://www.acsac.org/2012/workshops/law/.
10.
D.Clark and S.Hunt, Non-interference for deterministic interactive programs, in: Proc. Workshop on Formal Aspects in Security and Trust, FAST’08, LNCS, Vol. 5491, Springer, 2009, pp. 50–66.
11.
S.Eggert, H.Schnoor and T.Wilke, Noninterference with local policies, in: MFCS, LNCS, Vol. 8087, Springer, 2013, pp. 337–348.
12.
S.Eggert, R.van der Meyden, H.Schnoor and T.Wilke, The complexity of intransitive noninterference, in: Proc. IEEE Symposium on Security and Privacy, 2011, pp. 196–211.
13.
R.Fagin, J.Y.Halpern, Y.Moses and M.Y.Vardi, Reasoning About Knowledge, MIT Press, 1995.
14.
R.Focardi and R.Gorrieri, Classification of security properties (Part I: information flow), in: Foundations of Security Analysis and Design, FOSAD 2000, Bertinoro, Italy, September 2000, R.Focardi and R.Gorrieri, eds, LNCS, Vol. 2171, Springer, 2001, pp. 331–396.
15.
J.A.Goguen and J.Meseguer, Security policies and security models, in: Proc. IEEE Symp. on Security and Privacy, Oakland, 1982, pp. 11–20.
16.
J.A.Goguen and J.Meseguer, Unwinding and inference control, in: IEEE Symp. on Security and Privacy, 1984, pp. 75–87.
17.
R.Gorrieri and M.Vernali, On intransitive non-interference in some models of concurrency, in: Foundations of Security Analysis and Design VI – FOSAD Tutorial Lectures, LNCS, Vol. 6858, Springer, 2011, pp. 125–151.
18.
D.Greve, M.Wilding and M.Vanfleet, A separation kernel formal security policy, in: Proc. Fourth International Workshop on the ACL2 Theorem Prover and Its Applications, 2003, Paper and associated proof scripts available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.
19.
J.T.Haigh and W.D.Young,
Extending the noninterference version of MLS for SAT, IEEE Trans. on Software EngineeringSE-13(2) (1987), 141–150.
20.
C.L.Heitmeyer, M.Archer, E.I.Leonard and J.D.McLean, Formal specification and verification of data separation in a separation kernel for an embedded system, in: Proc. ACM Conf. on Computer and Communications Security, 2006, pp. 346–355.
21.
D.M.Johnson and F.J.Thayer, Security and the composition of machines, in: Proc. IEEE Security Foundations Workshop, 1988, pp. 72–89.
22.
M.N.Krohn and E.Tromer, Noninterference for a practical DIFC-based operating system, in: IEEE Symp. on Security and Privacy, 2009, pp. 61–76.
23.
R.Leslie, Dynamic intransitive noninterference, in: Proc. IEEE Int. Symp. on Secure Software Engineering, 2006.
24.
H.Mantel, Possibilistic definitions of security – an assembly kit, in: Proc. IEEE Computer Security Foundations Workshop, 2000, pp. 185–199.
25.
H.Mantel, Information flow control and applications – bridging a gap, in: FME 2001: Formal Methods for Increasing Software Productivity, Proc. Int. Symp. of Formal Methods Europe, LNCS, Vol. 2021, Springer, 2001, pp. 153–172.
26.
H.Mantel and D.Sands, Controlled declassification based on intransitive noninterference, in: Proc. Asian Symp. on Programming Languages and Systems, LNCS, Vol. 3302, Springer-Verlag, 2004, pp. 129–145.
27.
W.B.Martin, P.White, A.Goldberg and F.S.Taylor, Formal construction of the mathematically analyzed separation kernel, in: Proc. 15th IEEE Int. Conf. on Automated Software Engineering, 2000, pp. 133–141.
28.
D.McCullough, Noninterference and the composability of security properties, in: Proc. IEEE Symp. on Security and Privacy, 1988, pp. 177–186.
29.
J.McLean, Reasoning about security models, in: Proc. IEEE Conf. on Security and Privacy, 1987, pp. 123–131.
M.C.Pease, R.E.Shostak and L.Lamport,
Reaching agreement in the presence of faults, J. ACM27(2) (1980), 228–234.
32.
C.Percival, Cache missing for fun and profit, available at: http://www.daemonology.net/papers/htt.pdf.
33.
A.W.Roscoe and M.H.Goldsmith, What is intransitive noninterference? in: IEEE Computer Security Foundations Workshop, 1999, pp. 228–238.
34.
J.Rushby,
Design and verification of secure systems, ACM Operating Systems Review15(1) (1981), 12–21.
35.
J.Rushby, Noninterference, transitivity, and channel-control security policies, Technical Report CSL-92-02, SRI International, December 1992.
36.
P.Y.Ryan, Mathematical models of computer security, in: Foundations of Security Analysis and Design, FOSAD 2000, Bertinoro, Italy, September 2000, R.Focardi and R.Gorrieri, eds, LNCS, Vol. 2171, Springer, 2001, pp. 1–62.
37.
P.Y.A.Ryan and S.A.Schneider,
Process algebra and non-interference, Journal of Computer Security9(1,2) (2001), 75–103.
38.
A.Sabelfeld and D.Sands, Dimensions and principles of declassification, in: Proceedings of the 18th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 2005, pp. 255–269.
39.
G.Schellhorn, W.Reif, A.Schairer, P.A.Karger, V.Austel and D.C.Toll,
Verified formal security models for multiapplicative smart cards, Journal of Computer Security10(4) (2002), 339–368.
40.
D.Sutherland, A model of information, in: Proc. 9th National Computer Security Conf., 1986, pp. 175–183.
41.
R.van der Meyden, A comparison of semantic models of intransitive noninterference, December 2007, Unpublished manuscript, available at: http://www.cse.unsw.edu.au/~meyden.
42.
R.van der Meyden and C.Zhang,
A comparison of semantic models for noninterference, Theoretical Computer Science411(47) (2010), 4123–4147.
43.
D.von Oheimb, Information flow control revisited: Noninfluence = Noninterference + Nonleakage, in: Computer Security – ESORICS 2004, LNCS, Vol. 3193, Springer, 2004, pp. 225–243.
44.
J.T.Wittbold and D.M.Johnson, Information flow in nondeterministic systems, in: Proc. IEEE Symp. on Security and Privacy, 1990, pp. 144–161.
45.
S.Zdancewic and A.C.Myers, Robust declassification, in: Proc. IEEE Computer Security Foundations Workshop, 2001.
