CVS is a widely known version management system, which can be used for the distributed development of software as well as its distribution from a central database. In this paper, we provide an outline of a formal security analysis of a CVS-Server architecture performed in [1]. The analysis is based on an abstract architecture (enforcing a role-based access control on the repository), which is rened to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as framework to formulate access control and condentiality properties. Both the abstract as well as the concrete architecture are specied in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machinechecked proofs for consistency properties of the specication, for the correctness of the renement, and for some security properties. Thus, we present a case study for the security analysis of realistic models over an o-the-shelf system by formal machine-checked proofs.
['Achim D. Brucker', 'Burkhart Wolff']
A Case Study of a Formalized Security Architecture