Fulltext

A verification approach to applied system security

Brucker, Achim D. ; Wolff, Burkhart

In: International Journal on Software Tools for Technology Transfer, 2005, vol. 7, no. 3, p. 233-247

Ajouter à la liste personnelle
    Titre
    • A verification approach to applied system security
    Auteur
    • Brucker, Achim D.. Information Security, ETH Zürich, ETH-Zentrum, 8092, Zürich, Switzerland
    • Wolff, Burkhart. Universität Freiburg, George-Köhler-Allee 52, 79110, Freiburg, Germany
    Type de document
    • Postprint
    Langue
    • Anglais
    Publié dans
    • International Journal on Software Tools for Technology Transfer, 2005, vol. 7, no. 3, p. 233-247. Springer Berlin Heidelberg; www.springer.de
    Autre version électronique
    Identifiant OAI-PMH
    • oai:doc.rero.ch:318938
    Summary
    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