Skip to main content

Tools for traceable security verification


Andreas Bauer, Jan Juerjens and Yijun Yu


The Open University


Dependable systems evolution has been identified by the UK Computing Research Committee (UKCRC) as one of the current grand challenges for computer science. We present work towards addressing this challenge which focusses on one facet of dependability, namely data security: We give an overview on an approach for modelbased security verification which provides a traceability link to the implementation. The approach uses a design model in the UML security extension UMLsec which can be formally verified against high-level security requirements such as secrecy and authenticity. An implementation of the specification can then be verified against the model by making use of run-time verification through the traceability link. The approach supports software evolution in so far as the traceability mapping is updated when refactoring operations are regressively performed using our tool-supported refactoring technique. The proposed method has been applied to an implementation of the Internet security protocol SSL.

BibTeX Entry

    author           = {Bauer, Andreas and Juerjens, Jan and Yu, Yijun},
    editor           = {{E. Gelenbe and S. Abramsky and V. Sassone}},
    month            = sep,
    year             = {2008},
    title            = {Tools for Traceable Security Verification},
    address          = {Swindon, UK},
    pages            = {367--378},
    booktitle        = {BCS International Academic Conference 2008---Visions of Computer Science}


Served by Apache on Linux on seL4.