Abstract:

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.