Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment. A case study within the FoCaLiZe environment

Abstract : FoCaLiZe is an object-oriented programming environment that combines specifications, programs and proofs in the same language. This paper describes how its features can be used to formally express specifications and to develop by stepwise refinement the design and implementation of se- cured systems, while proving that the implementation meets its specification or design requirements. We thus obtain a modular implementation of a generic framework for the def- inition of security policies together with certified enforce- ment mechanism for these policies.
Type de document :
Communication dans un congrès
PLAS - Seventh Workshop on Programming Languages and Analysis for Security, Jun 2012, Beijing, China. ACM, 2012, <10.1145/2336717.2336726>
Liste complète des métadonnées


https://hal.inria.fr/hal-00773654
Contributeur : Damien Doligez <>
Soumis le : lundi 14 janvier 2013 - 14:33:07
Dernière modification le : lundi 19 septembre 2016 - 17:16:52
Document(s) archivé(s) le : samedi 1 avril 2017 - 04:28:19

Fichier

DJR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Damien Doligez, Mathieu Jaume, Renaud Rioboo. Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment. A case study within the FoCaLiZe environment. PLAS - Seventh Workshop on Programming Languages and Analysis for Security, Jun 2012, Beijing, China. ACM, 2012, <10.1145/2336717.2336726>. <hal-00773654>

Partager

Métriques

Consultations de
la notice

158

Téléchargements du document

128