This Article 
 Bibliographic References 
 Add to: 
The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties
September 1997 (vol. 23 no. 9)
pp. 550-571

Abstract—The Compositional Security Checker (CoSeC for short) is a semantic-based tool for the automatic verification of some compositional information flow properties. The specifications given as inputs to CoSeC are terms of the Security Process Algebra, a language suited for the specification of concurrent systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by CoSeC are some of those classified in [8]. They derive from some classic notions, e.g., Noninterference [11]. The tool is based on the same architecture as the Concurrency Workbench [5], from which some modules have been imported unchanged. The usefulness of the tool is tested with the significant case-study of an access-monitor, presented in several versions in order to illustrate the relative merits of the various information flow properties that CoSeC can check. Finally, we present an application in the area of network security: we show that the theory (and the tool) can be reasonably applied also for singling out security flaws in a simple, yet paradigmatic, communication protocol.

[1] P.G. Allen, "A Comparison of NonInterference and NonDeducibility using CSP," Proc. Fourth IEEE Computer Security Foundations Workshop, pp. 43-54,Franconia, New Hampshire, June 1991.
[2] D.E. Bell and L.J. La Padula, "Secure Computer Systems: Unified Exposition and Multics Interpretation," ESD-TR-75-306, MITRE MTR-2997, Mar. 1976.
[3] J.A. Bergstra and J.W. Klop, "Algebra of Communicating Processes with Abstraction," Theoretical Computer Science, vol. 37, pp. 77-121, 1985.
[4] S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe, "A Theory of Communicating Sequential Processes," J. ACM, vol. 31, no. 3, pp. 560-599, July 1984.
[5] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 36-72.
[6] R. Focardi, "Comparing Two Information Flow Security Properties," Proc. Ninth IEEE Computer Security Foundation Workshop, (CSFW'96), M. Merritt, ed., pp. 116-122. IEEE CSPress, June 1996.
[7] R. Focardi, A. Ghelli, and R. Gorrieri, "Using NonInterference for the Analysis of Security Protocols," to appear.
[8] R. Focardi and R. Gorrieri, "A Classification of Security Properties for Process Algebras," J. Computer Security, vol. 3, no. 1, pp. 5-33, 1994/1995.
[9] R. Focardi and R. Gorrieri, "Non Interference: Past, Present and Future," Proc. Foundations for Secure Mobile Code Workshop, pp. 33-36, DARPA, Mar. 1997.
[10] R. Focardi, R. Gorrieri, and R. Segala, "A Concrete Criterion for Information Flow Security," to appear.
[11] J.A. Goguen and J. Meseguer, "Security Policy and Security Models," Proc. Symp. Security and Privacy, pp. 11-20. IEEE CS Press, Apr. 1982.
[12] M. Hennessy and H. Lin, "Symbolic Bisimulations," Technical Report CSR1/92, Univ. of Sussex, 1992.
[13] Y. Hirshfeld, "Bisimulation Trees and the Decidability of Weak Bisimulations," Technical Report, Tel Aviv Univ, 1996.
[14] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[15] J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages and Computation, pp. 22-24. Addison-Wesley, 1979.
[16] P.C. Kanellakis and S.A. Smolka, "CCS Expressions, Finite State Processes, and Three Problems of Equivalence," Information and Computation, pp. 43-68, vol. 86, 1990.
[17] R.M. Keller,“Formal verification of parallel programs,” Comm. ACM, vol. 19, no. 7, July 1976.
[18] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[19] R. Milner, J. Parrow, and D. Walker, “A Calculus of Mobile Processes,” Information and Computation, vol. 100, pp. 1-77, 1992.
[20] R.M. Needham and M.D. Schroeder, "Using Encryption for Authentication in Large Networks of Computers," Comm. ACM, vol. 21, no. 12, pp. 993-999, Dec. 1978
[21] R. De Nicola and M. Hennessy, "Testing Equivalences for Processes," Theoretical Computer Science, vol. 34, pp. 83-133, 1984.
[22] Department of Defense, "Integrity in Automated Information Systems," Technical Report C 79-91, National Computer Security Center, Sept. 1991.
[23] G. Plotkin, "A Structural Approach to Operational Semantics," Technical Report DAIMI-FN-19, Aarhus Univ., 1981.
[24] A.W. Roscoe, "Model Checking CSP," A.W. Roscoe, ed., A Classical Mind. Prentice Hall, 1994.
[25] A.W. Roscoe, J.C.P. Woodcock, and L. Wulf, "Noninterference through Determinism," Proc. European Symp. Research in Computer Security 1994 (ESORICS'94), pp. 33-53, Lecture Notes in Computer Science 875. Springer-Verlag, 1994.
[26] P.Y.A. Ryan, "A CSP Formulation of NonInterference," Proc. Computer Security Foundation Workshop III,Franconia. IEEE CS Press, 1990.
[27] L.J. Stockmeyer and A.R. Meyer, "Word Problems Requiring Exponential Time," Proc. Fifth ACM Symp. Theory of Computing, pp. 1-9, 1973.
[28] C.R. Tsai, V.D. Gligor, and C.S. Chandersekaran, "On the Identification of Covert Storage Channels in Secure Systems," IEEE Trans. Software Eng., pp. 569-580, June 1990.
[29] J.T. Wittbold and D. Johnson, "Information flow in nondeterministic systems," Proc. 1990 IEEE Symp. Research in Security and Privacy. IEEE Press, 1990.

Index Terms:
Tools and techniques, program verification, access controls, information flow controls, network protocol verification.
Riccardo Focardi, Roberto Gorrieri, "The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties," IEEE Transactions on Software Engineering, vol. 23, no. 9, pp. 550-571, Sept. 1997, doi:10.1109/32.629493
Usage of this product signifies your acceptance of the Terms of Use.