The Compositional Security Checker: a tool for the verification of information flow security properties
- 1 January 1997
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 23 (9) , 550-571
- https://doi.org/10.1109/32.629493
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 (Focardi and Gorrieri, 1994). They are derived from some classic notions, e.g., noninterference. The tool is based on the same architecture as the Concurrency Workbench, 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.Keywords
This publication has 16 references indexed in Scilit:
- Comparing two information flow security propertiesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A comparison of non-interference and non-deducibility using CSPPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Classification of Security Properties for Process Algebras1Journal of Computer Security, 1995
- The concurrency workbenchACM Transactions on Programming Languages and Systems, 1993
- On the identification of covert storage channels in secure systemsIEEE Transactions on Software Engineering, 1990
- Information flow in nondeterministic systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- A Theory of Communicating Sequential ProcessesJournal of the ACM, 1984
- Testing equivalences for processesTheoretical Computer Science, 1984
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978
- Word problems requiring exponential time(Preliminary Report)Published by Association for Computing Machinery (ACM) ,1973