A UML-based static verification framework for security |
| |
Authors: | Igor Siveroni Andrea Zisman George Spanoudakis |
| |
Affiliation: | (1) Department of Computing, City University London Northampton Square, London, EC1V, UK |
| |
Abstract: | Secure software engineering is a new research area that has been proposed to address security issues during the development
of software systems. This new area of research advocates that security characteristics should be considered from the early
stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after
the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and
verification of secure software systems in early stages of the software development life-cycle taking into consideration security
and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and
state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property
specification language designed to reason about temporal and general properties of UML state machines using the semantic domains
of the former, and implement the model checking process by translating models and properties into Promela, the input language
of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing
the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|