A Verification Approach for Applied System Security

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: , ,

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
(PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/s10009-004-0176-3) ( )