The CVS-Server Case Study: A Formalized Security Architecture
by Achim D. Brucker, Frank Rittinger, and Burkhart Wolff
CVS is a widely known version management system. Configured in server mode, it can be used for the distributed development of software as well as its distribution from a central database called the repository. In this setting, a number of security mechanisms have to be integrated into the CVS-server architecture. We present an abstract formal model of the access control aspects of a CVS-server architecture enforcing a role-based access control on the data in the repository. This abstract architecture is refined to an implementation architecture, which represents (an abstraction of) a concrete CVS-server configuration running in a POSIX/UNIX environment. Both the abstract as well as the concrete architecture are specified in the language Z. The specification is compiled to HOL-Z, such that refinement proofs for this case study can be done in Isabelle/HOL.
Keywords:
Categories: , ,
Documents: (full text as PDF file)
Please cite this article as follows:
Achim D. Brucker, Frank Rittinger, and Burkhart Wolff.
The CVS-Server Case Study: A Formalized Security Architecture.
In FM-TOOLS 2002, pages 47-52, 2002. Available as Technical Report, University Augsburg, number 2002-11.
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (
| abstract | = | {CVS is a widely known version management system. Configured in server mode, it can be used for the distributed development of software as well as its distribution from a central database called the \emph{repository}. In this setting, a number of security mechanisms have to be integrated into the CVS-server architecture. We present an abstract formal model of the access control aspects of a CVS-server architecture enforcing a role-based access control on the data in the repository. This abstract architecture is refined to an implementation architecture, which represents (an abstraction of) a concrete CVS-server configuration running in a POSIX/UNIX environment. Both the abstract as well as the concrete architecture are specified in the language Z. The specification is compiled to HOL-Z, such that refinement proofs for this case study can be done in Isabelle/HOL.}, | |
| address | = | {Augsburg}, | |
| author | = | {Achim D. Brucker and Frank Rittinger and Burkhart Wolff}, | |
| booktitle | = | {FM-TOOLS 2002}, | |
| editor | = | {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif}, | |
| language | = | {USenglish}, | |
| month | = | {jul}, | |
| note | = | {Available as Technical Report, University Augsburg, number 2002--11.}, | |
| organization | = | {University Augsburg}, | |
| pages | = | {47--52}, | |
| = | {https://www.brucker.ch/bibliography/download/2002/brucker.ea-cvs-server-2002.pdf}, | ||
| project | = | {FSA}, | |
| title | = | {The {CVS}-Server Case Study: {A} Formalized Security Architecture}, | |
| url | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002}, | |
| year | = | {2002}, |