The Open UniversitySkip to content

Run-time security traceability for evolving systems

Bauer, Andreas; Jürjens, Jan and Yu, Yijun (2011). Run-time security traceability for evolving systems. The Computer Journal, 54(1) pp. 58–87.

Full text available as:
PDF (Accepted Manuscript) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (667kB)
DOI (Digital Object Identifier) Link:
Google Scholar: Look up in Google Scholar


Security-critical systems are challenging to design and implement correctly and securely. A lot of vulnerabilities have been found in current software systems both at the specification and the implementation levels. This paper presents a comprehensive approach for model-based security assurance. Initially, it allows one to formally verify the design models against high-level security requirements such as secrecy and authentication on the specification level, and helps to ensure that their implementation adheres to these properties, if they express a system's run-time behaviour. As such, it provides a traceability link from the design model to its implementation by which the actual system can then be verified against the model while it executes. This part of our approach relies on a technique also known as run-time verification. The extra effort for it is small as most of the computation is automated; however, additional resources at run-time may be required. If during run-time verification a security weakness is uncovered, it can be removed using aspect-oriented security hardening transformations. Therefore, this approach also supports the evolution of software since the traceability mapping is updated when refactoring operations are regressively performed using our tool-supported refactoring technique. The proposed method has been applied to the Java-based implementation JESSIE of the Internet security protocol SSL, in which a security weakness was detected and fixed using our approach. We also explain how the traceability link can be transformed to the official implementation of the Java secure sockets extension that was recently made open source by Sun.

Item Type: Journal Item
Copyright Holders: 2010 The Authors
ISSN: 0010-4620
Extra Information: A preliminary version of this paper was presented at the BCS08 Visions of Computer Science Conference, held on 22-24 September 2008.
Keywords: run-time verification; monitoring; IT security; cryptographic protocols; formal verification; security analysis; software evolution; requirements traceability
Academic Unit/School: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Faculty of Science, Technology, Engineering and Mathematics (STEM)
Research Group: Centre for Research in Computing (CRC)
Item ID: 21678
Depositing User: Yijun Yu
Date Deposited: 10 Jun 2010 10:32
Last Modified: 20 May 2019 17:47
Share this page:


Altmetrics from Altmetric

Citations from Dimensions

Download history for this item

These details should be considered as only a guide to the number of downloads performed manually. Algorithmic methods have been applied in an attempt to remove automated downloads from the displayed statistics but no guarantee can be made as to the accuracy of the figures.

Actions (login may be required)

Policies | Disclaimer

© The Open University   contact the OU