The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties

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 protoco