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

Please cite this work as follows:
A. D. Brucker and B. Wolff, “A verification approach for applied system security,” International Journal on Software Tools for Technology (STTT), vol. 7, no. 3, pp. 233–247, 2005, doi: 10.1007/s10009-004-0176-3. Author copy: http://logicalhacking.com/publications/brucker.ea-verification-2005/

BibTeX
@Article{ brucker.ea:verification:2005,
  author    = {Achim D. Brucker and Burkhart Wolff},
  title     = {A Verification Approach for Applied System Security},
  journal   = {International Journal on Software Tools for Technology (STTT)
               },
  year      = {2005},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  language  = {USenglish},
  keywords  = {Verification, Security, Access Control, Refinement, POSIX,
               CVS, Z},
  areas     = {security, formal methods, software},
  issn      = {1433-2779},
  doi       = {10.1007/s10009-004-0176-3},
  volume    = {7},
  number    = {3},
  pages     = {233--247},
  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.},
  note      = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-verification-2005/}},
}