The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties
Issue No.09 - September (1997 vol.23)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.629493
<p><b>Abstract</b>—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 [<ref rid="bibe05508" type="bib">8</ref>]. They derive from some classic notions, e.g., Noninterference [<ref rid="bibe055011" type="bib">11</ref>]. The tool is based on the same architecture as the Concurrency Workbench [<ref rid="bibe05505" type="bib">5</ref>], 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.</p>
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, September 1997, doi:10.1109/32.629493