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.

Obsoleted by:
This publication has been obsoleted by the following publication:
A. D. Brucker and B. Wolff, “A case study of a formalized security architecture,” Electronic Notes in Theoretical Computer Science, vol. 80, pp. 24–40, 2003, doi: 10.1016/S1571-0661(04)80807-7. Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS’03). Author copy: https://logicalhacking.com/publications/brucker.ea-case-2003/

Extended by:
An extended version is available as:
A. D. Brucker, F. Rittinger, and B. Wolff, “A CVS-Server security architecture — concepts and formal analysis,” Albert-Ludwigs-Universität Freiburg, 182, 2002. Author copy: https://logicalhacking.com/publications/brucker.ea-cvs-server-2002-b/

Please cite this work as follows:
A. D. Brucker, F. Rittinger, and B. Wolff, “The CVS-server case study: A formalized security architecture,” in FM-TOOLS 2002, D. Haneberg, G. Schellhorn, and W. Reif, Eds. Augsburg: University Augsburg, 2002, pp. 47–52. Available as Technical Report, University Augsburg, number 2002–11.. Author copy: https://logicalhacking.com/publications/brucker.ea-cvs-server-2002/

BibTeX
@InCollection{ brucker.ea:cvs-server:2002,
  author       = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  areas        = {security, formal methods, software},
  title        = {The {CVS}-Server Case Study: {A} Formalized Security
                  Architecture},
  editor       = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif},
  booktitle    = {FM-TOOLS 2002},
  year         = {2002},
  pages        = {47--52},
  month        = {jul},
  organization = {University Augsburg},
  address      = {Augsburg},
  language     = {USenglish},
  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.},
  note         = {Available as Technical Report, University Augsburg, number
                  2002--11.. 
                  Author copy: \url{https://logicalhacking.com/publications/brucker.ea-cvs-server-2002/}},
  extendedby   = {brucker.ea:cvs-server:2002-b},
  obsoletedby  = {brucker.ea:case:2003},
  pdf          = {https://logicalhacking.com/publications/brucker.ea-cvs-server-2002/brucker.ea-cvs-server-2002.pdf},
}