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

Formal specification of security guidelines for program certification

Zhioua, Zeineb; Roudier, Yves; Ameur-Boulifa, Rabea

TASE 2017, 11th International Symposium on Theoretical Aspects of Software Engineering, September 13-15, 2017, Nice, France

Secure software can be obtained out of two distinct processes: security by design, and security by certification. The former approach has been quite extensively formalized as it builds upon models, which are verified to ensure security properties are attained and from which software is then derived manually or automatically. In contrast, the latter approach has always been quite informal in both specifying security best practices and verifying that the code produced conforms to them. In this paper, we focus on the latter approach and describe how security guidelines might be captured by security experts and verified formally by developers. Our technique relies on abstracting actions in a program based on modularity, and on combining model checking together with information flow analysis. Our goal is to formalize the existing body of knowledge in security best practices using formulas in the MCL language and to conduct formal verifications of the conformance of programs with such security guidelines. We also discuss our first results in creating a methodology for the formalization of security guidelines.

Document Bibtex

Titre:Formal specification of security guidelines for program certification
Mots Clés:Security Guidelines, Security Best Practices, Program Certification, Information Flow Analysis, Model Checking, Labelled Transition Systems
Type:Conférence
Langue:English
Ville:Nice
Pays:FRANCE
Date:
Département:Sécurité numérique
Eurecom ref:5293
Copyright: © Université de Nice. Personal use of this material is permitted. The definitive version of this paper was published in TASE 2017, 11th International Symposium on Theoretical Aspects of Software Engineering, September 13-15, 2017, Nice, France and is available at :
Bibtex: @inproceedings{EURECOM+5293, year = {2017}, title = {{F}ormal specification of security guidelines for program certification}, author = {{Z}hioua, {Z}eineb and {R}oudier, {Y}ves and {A}meur-{B}oulifa, {R}abea}, booktitle = {{TASE} 2017, 11th {I}nternational {S}ymposium on {T}heoretical {A}spects of {S}oftware {E}ngineering, {S}eptember 13-15, 2017, {N}ice, {F}rance}, address = {{N}ice, {FRANCE}}, month = {09}, url = {http://www.eurecom.fr/publication/5293} }
Voir aussi: