Ecole d'ingénieur et centre de recherche en Sciences du numérique

Formal specification and verification of security guidelines

Zhioua, Zeineb; Roudier, Yves; Ameur-Boulifa, Rabéa

PRDC 2017, IEEE Pacific Rim International Symposium on Dependable Computing, January 22-25, 2017, Christchurch, New Zealand

Ensuring the compliance of developed software with general and application-specific security requirements is a challenging task due to the lack of automatic and formal means to lead this verification. In this paper, we present our approach that aims at integrating the formal specification and verification of security guidelines in early stages of the development lifecycle by combining the model checking together with information flow analysis. We present our framework that is based on an extension of LTS (Labeled Transition Systems) by data dependence information to cover the end-to-end specification and verification of security guidelines.

Doi Bibtex

Titre:Formal specification and verification of security guidelines
Mots Clés:Security Guidelines, Formal specification, Model Checking, Information Flow Analysis, Program Dependence Graph
Département:Sécurité numérique
Eurecom ref:5100
Copyright: © 2017 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
Bibtex: @inproceedings{EURECOM+5100, doi = {}, year = {2017}, title = {{F}ormal specification and verification of security guidelines}, author = {{Z}hioua, {Z}eineb and {R}oudier, {Y}ves and {A}meur-{B}oulifa, {R}ab{\'e}a}, booktitle = {{PRDC} 2017, {IEEE} {P}acific {R}im {I}nternational {S}ymposium on {D}ependable {C}omputing, {J}anuary 22-25, 2017, {C}hristchurch, {N}ew {Z}ealand}, address = {{C}hristchurch, {NOUVELLE}-{Z}{\'{E}}{LANDE}}, month = {01}, url = {} }
Voir aussi: