학술논문
Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment : a case study within the FoCaLiZe environment
Document Type
Conference
Author
Source
Proceedings of the 7th Workshop on Programming Languages and Analysis for Security. :1-12
Subject
Language
English
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 secured systems, while proving that the implementation meets its specification or design requirements. We thus obtain a modular implementation of a generic framework for the definition of security policies together with certified enforcement mechanism for these policies.