Verification and Trade-Off Analysis of Security Properties in UML System Models

G Georg, K Anastasakis, Behzad Bordbar, SH Houmb, I Ray, M Toahchoodee

Research output: Contribution to journalArticle

25 Citations (Scopus)


Designing secure systems is a nontrivial task. Incomplete or faulty designs can cause security mechanisms to be incorrectly incorporated in a system, allowing them to be bypassed and resulting in a security breach. We advocate the use of the Aspect-Oriented Risk-Driven Development (AORDD) methodology for developing secure systems. This methodology begins with designers defining system assets, identifying potential attacks against them, and evaluating system risks. When a risk is unacceptable, designers must mitigate the associated threat by incorporating security mechanisms methodically into the system design. Designers next formally evaluate the resulting design to ensure that the threat has been mitigated, while still allowing development to meet other project constraints. In this paper, we focus on the AORDD analysis, which consists of: 1) a formal security evaluation and 2) a trade-off analysis that enables system designers to position alternative security solutions against each other. The formal security evaluation uses the Alloy Analyzer to provide assurance that an incorporated security mechanism performs as expected and makes the system resilient to previously identified attacks. The trade-off analysis uses a Bayesian Belief Network topology to allow equally effective security mechanisms to be compared against system security requirements and other factors such as time-to-market and budget constraints.
Original languageEnglish
Pages (from-to)338-356
Number of pages19
JournalIEEE Transactions on Software Engineering
Issue number3
Publication statusPublished - 1 May 2010


  • Bayesian belief network (BBN)
  • Monotonicity
  • security analysis
  • Aspect-oriented modeling (AOM)
  • Correlated equilibrium distribution
  • Implementation
  • trade-off analysis


Dive into the research topics of 'Verification and Trade-Off Analysis of Security Properties in UML System Models'. Together they form a unique fingerprint.

Cite this