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 Doi 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
Département:Sécurité numérique
Eurecom ref:5293
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+5293, doi = {}, 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 = {} }
Voir aussi: