A Verification Approach for Applied System Security

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:verification:2005.We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.

The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the posix environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.

Both the abstract and the implementation 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 security properties.

Schlüsselwörter: verification, security, access control, refinement, POSIX, CVS, Z
Kategorien: , ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:verification:2005.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff. A Verification Approach for Applied System Security. In International Journal on Software Tools for Technology (STTT), 7 (3), pages 233-247, 2005.
Schlüsselwörter: verification, security, access control, refinement, POSIX, CVS, Z
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s10009-004-0176-3) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@Article{ brucker.ea:verification:2005,
abstract = {We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.\\\\The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the \posix{} environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.\\\\Both the abstract and the implementation 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 security properties.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
doi = {10.1007/s10009-004-0176-3},
issn = {1433-2779},
journal = {International Journal on Software Tools for Technology (STTT)},
keywords = {verification, security, access control, refinement, POSIX, CVS, Z},
language = {USenglish},
number = {3},
pages = {233--247},
pdf = {https://www.brucker.ch/bibliography/download/2005/brucker.ea-verification-2005.pdf},
publisher = {Springer-Verlag},
title = {A Verification Approach for Applied System Security},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-verification-2005},
volume = {7},
year = {2005},
}