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.

Sécurité numérique
Eurecom Ref:
© 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.
See also: