A Verification Approach for Applied System Security
by Achim D. Brucker and Burkhart Wolff
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.
Keywords: verification, security, access control, refinement, POSIX, CVS, Z
Categories: , ,
Documents: (full text as PDF file)
Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff.
A Verification Approach for Applied System Security.
In International Journal on Software Tools for Technology (STTT), 7 (3), pages 233-247, 2005.
Keywords: verification, security, access control, refinement, POSIX, CVS, Z
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s10009-004-0176-3) (
| 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}, | |
| = | {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}, |