Login | Register

A Security Verification Framework for SysML Activity Diagrams


A Security Verification Framework for SysML Activity Diagrams

Samir, Ouchani (2013) A Security Verification Framework for SysML Activity Diagrams. PhD thesis, Concordia University.

[thumbnail of Ouchani_Phd_F2013.pdf]
Text (application/pdf)
Ouchani_Phd_F2013.pdf - Accepted Version


UML and SysML play a central role in modern software and systems engineering. They are considered as the de facto standard for modeling software and systems. Today’s systems are created from a myriad of interacting parts that are combined to produce visible behavior. The main difficulty arises from the different ways in modeling each component and the way they interact with each other. Moreover, nowadays secure software has become an essential part in industrial development. One challenge in academia as well as in industry is to produce a secure product. Another challenge is to prove its correctness especially when the software environment is imprecise and uncertain.

The aim of this thesis is to provide a practical and formal framework that enables security risk assessment and security requirements verification on a system modeled as a composition of UML/SysML behavioral diagrams. Our main contribution is a novel approach to automatically verify security of systems on their design models based on security requirements, probabilistic adversarial interactions between potential attackers and the system’s models. These structures are shaped to provide an elegant way to define the combination between different kinds of diagrams. We rely on stochastic security templates to specify security properties and a standard catalogue of attack patterns to build a library of attacks design patterns. The result of the interaction between selected attack scenarios and the composed diagrams with the instantiated security properties are used to quantify security risk by applying probabilistic model-checker. To handle the verification process scalability, our approach allows the verification of large system efficiently by optimizing and avoiding the global model construction. To demonstrate the effectiveness of our approach, we apply our methodology on academia as well as industrial benchmarks.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Samir, Ouchani
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:5 September 2013
Thesis Supervisor(s):Mourad, Debbabi and Otmane, Ait Mohamed
Keywords:Probabilistic Verification, Temporal Logic, Probabilistic Automata, Security Properties, Attack Pattern, Vulnerability Detection, Risk Assessment, UML, SysML, Activity Diagrams.
ID Code:977746
Deposited On:13 Jan 2014 15:01
Last Modified:18 Jan 2018 17:45
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top