A CVS-Server Security Architecture — Concepts and Formal Analysis

By Achim D. Brucker, Frank Rittinger, and Burkhart Wolff.

We present a secure architecture of a CVS-server, its implementation (i.e. mainly its configuration) and its formal analysis. Our CVS-server is uses cvsauth, that provides protection of passwords and protection of some internal data of the CVS repository. In contrast to other (security oriented) CVS-architectures, our approach allows the CVS-server run on an open filesystem, i.e. a filesystem where users can have direct access both by CVS-commands and by standard UNIX/POSIX commands such as mv. For our secure architecture of the CVS-server, we provide a formal specification and security analysis. The latter is based on a refinement mapping high-level security requirements on the architecture on low-level security mechanisms on the UNIX/POSIX filesystem level. The purpose of the formal analysis of the secure CVS-server architecture is twofold: First, it is the bases for the specification of mutual security properties such as non-repudiation, authentication and access control for this architecture. Second, the mapping of the architecture on standard security implementation technology is described. Thus, our approach can be seen as a method to give a formal underpinning for the usually tricky business of system administrators.

Keywords:
Security Architecture, Concurrent Versions System (CVS), Z, Formal Methods, Refinement, Access Control

Please cite this work as follows:
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/

BibTeX
@TechReport{ brucker.ea:cvs-server:2002-b,
  author      = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  language    = {USenglish},
  number      = {182},
  areas       = {security, formal methods, software},
  title       = {A {CVS-Server} Security Architecture --- Concepts and Formal
                 Analysis},
  abstract    = {We present a secure architecture of a CVS-server, its
                 implementation (i.e. mainly its configuration) and its formal
                 analysis. Our CVS-server is uses cvsauth, that provides
                 protection of passwords and protection of some internal data
                 of the CVS repository. In contrast to other (security
                 oriented) CVS-architectures, our approach allows the
                 CVS-server run on an open filesystem, i.e. a filesystem where
                 users can have direct access both by CVS-commands and by
                 standard UNIX/POSIX commands such as \texttt{mv}. For our
                 secure architecture of the CVS-server, we provide a formal
                 specification and security analysis. The latter is based on a
                 refinement mapping high-level security requirements on the
                 architecture on low-level security mechanisms on the
                 UNIX/POSIX filesystem level. The purpose of the formal
                 analysis of the secure CVS-server architecture is twofold:
                 First, it is the bases for the specification of mutual
                 security properties such as non-repudiation, authentication
                 and access control for this architecture. Second, the mapping
                 of the architecture on standard security implementation
                 technology is described. Thus, our approach can be seen as a
                 method to give a formal underpinning for the usually tricky
                 business of system administrators.},
  keywords    = {Security Architecture, Concurrent Versions System (CVS), Z,
                 Formal Methods, Refinement, Access Control},
  year        = {2002},
  num_pages   = {100},
  note        = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-cvs-server-2002-b/}},
  pdf         = {https://logicalhacking.com/publications/brucker.ea-cvs-server-2002-b/brucker.ea-cvs-server-2002-b.pdf},
}