OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Modeling and Formal Approach for the Precise Specification of Security Patterns

Hamid, Brahim and Percebois, Christian A Modeling and Formal Approach for the Precise Specification of Security Patterns. (2014) In: International Symposium on Engineering Secure Software and Systems - ESSoS 2014, 26 February 2014 - 28 February 2014 (Munich, Germany).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
546kB

Official URL: http://dx.doi.org/10.1007/978-3-319-04897-0_7

Abstract

Non-functional requirements such as Security and Dependability (S &D) become more important as well as more difficult to achieve. In fact, the integration of security features requires the availability of both application domain specific knowledge and security expertise at the same time. Hence, capturing and providing this expertise by the way of security patterns can support the integration of S&D features by design to foster reuse during the process of software system development. The solution envisaged here is based on combining metamodeling techniques and formal methods to represent security pattern at two levels of abstraction fostering reuse during the process of pattern development and during the process of pattern-based development. The contribution of this work is twofold: (1) An improvement of our previous pattern modeling language for representing security pattern in the form of a subsystem providing appropriate interfaces and targeting security properties, (2) Formal specification and validation of pattern properties, using the interactive Isabelle/HOL proof assistant. The resulting validation artifacts may mainly complete the definitions, and provide semantics for the interfaces and the properties in the context of S&D. As a result, validated patterns will be used as bricks to build applications through a Model-Driven engineering approach.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. The definitive version is available at http://link.springer.com/chapter/10.1007/978-3-319-04897-0_7
HAL Id:hal-01141439
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:13 Apr 2015 07:18

Repository Staff Only: item control page