A Case Study of a Formalized Security Architecture

by Achim D. Brucker and Burkhart Wolff

Cover for brucker.ea:case:2003.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~citebrucker.ea:cvs-server:2002. The analysis is based on an abstract architecture (enforcing a role-based access control on the repository), which is refined 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 confidentiality properties. Both the abstract as well as the concrete architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for some security properties. Thus, we present a case study for the security analysis of realistic models over an off-the-shelf system by formal machine-checked proofs.

Keywords: security, access control, POSIX, Unix, CVS, Z
Categories: , ,
Documents: (full text as PDF file) (slides) (handout)

QR Code for brucker.ea:case:2003.Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff. A Case Study of a Formalized Security Architecture. In Electronic Notes in Theoretical Computer Science, 80, pages 24-40, 2003. Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03)
Keywords: security, access control, POSIX, Unix, CVS, Z
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1016/S1571-0661(04)80807-7) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@Article{ brucker.ea:case:2003,
abstract = {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~\cite{brucker.ea:cvs-server:2002}. The analysis is based on an abstract architecture (enforcing a role-based access control on the repository), which is refined 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 confidentiality properties. Both the abstract as well as the concrete architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for some security properties. Thus, we present a case study for the security analysis of realistic models over an off-the-shelf system by formal machine-checked proofs.},
address = {Amsterdam},
author = {Achim D. Brucker and Burkhart Wolff},
doi = {10.1016/S1571-0661(04)80807-7},
editor = {Thomas Arts and Wan Fokkink},
journal = {Electronic Notes in Theoretical Computer Science},
keywords = {security, access control, POSIX, Unix, CVS, Z},
language = {USenglish},
location = {R{\o}ros, Norway},
note = {Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03)},
pages = {24--40},
pdf = {https://www.brucker.ch/bibliography/download/2003/brucker.ea-case-2003.pdf},
publisher = {Elsevier Science Publishers},
talk = {talk:brucker.ea:case:2003},
title = {A Case Study of a Formalized Security Architecture},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-case-2003},
volume = {80},
year = {2003},
}