Automatic compositional verification of some security properties

Abstract

The Compositional Security Checker (CSC for short) is a semantic tool for the automatic verification of some compositional information flow properties. The specifications given as inputs to CSC are terms of the Security Process Algebra, a language suited for the specification of systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by CSC are some of those classified in [4]. They are derivations of some classic notions, e.g. Non Interference [6]. The tool is based on the same architecture of the Concurrency Workbench [2], from which some modules have been integrally imported. The usefulness of the tool is tested with the significative case-study of an access-monitor.