Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Résultat majeur
Production scientifique
Résultat majeur : A VERIFICATION APPROACH FOR APPLIED SYSTEM SECURITY
A VERIFICATION APPROACH FOR APPLIED SYSTEM SECURITY
24 janvier 2005

Achim D. Brucker and Burkhart Wolff. A Verification Approach for Applied System Security. In International Journal on Software Tools for Technology Transfer (STTT), 7 (3), pages 233-247, 2005.
We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises several concurrently executing systems that authenticate users and generate and store digital signatures by passing security relevant data through a tightly controlled interface. The architecture is interesting from a formal-methods perspective as it involves complex operations on data as well as process coordination and hence is a candidate for both data-oriented and process-oriented formal methods.
We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.
The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.
Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.

Achim D. Brucker and Burkhart Wolff. Springer, DOI 10.1007/s10009-004-0176-3.

Activités de recherche
  [aucun]

Equipe
  [aucun]

Contact
  ° WOLFF Burkhart
Résultats majeurs
COMPUTER‐AIDED BIOCHEMICAL PROGRAMMING OF SYNTHETIC MICROREACTORS AS DIAGNOSTIC DEVICES
27 avril 2018
Alexis Courbet, Patrick Amar, Francois Fages, Eric Renard, Franck Molina Mol Syst Biol. (2018) 14:

BEST PAPER AWARD: SELF-STABILIZING DISTRIBUTED STABLE MARRIAGE
05 novembre 2017
SSS 2017, M. Laveau, G. Manoussakis, J. Beauquier, T. Bernard, J. Burman, J. Cohen, and L. Pilard

BEST PAPER AWARD INTELLI 2017: A MODEL OF PULSATION FOR EVOLUTIVE FORMALIZING INCOMPLETE INTELLIGENT SYSTEMS
27 juillet 2017
authors: Marta Franova, Yves Kodratoff

INFORMATION-GEOMETRIC OPTIMIZATION ALGORITHMS: A UNIFYING PICTURE VIA INVARIANCE PRINCIPLES
02 mai 2017
Yann Ollivier, Ludovic Arnold, Anne Auger, Nikolaus Hansen - JMLR 18(18):1−65, 2017.

FORMAL MUTATION TESTING FOR CIRCUS
21 avril 2016
Alex Donizeti Betez Alberto, Ana Cavalcanti, Marie-Claude Gaudel, Adenilso Simao Journal of Infor