Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Research highlights
Research results
Research highlight : A VERIFICATION APPROACH FOR APPLIED SYSTEM SECURITY
A VERIFICATION APPROACH FOR APPLIED SYSTEM SECURITY
8 July 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 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.



Keyword
  [none]

Group
  [none]

Contact
  [none]
Research highlights
MODEL TRANSFORMATION AS CONSERVATIVE THEORY-TRANSFORMATION
30 October 2020
We present a new technique to construct tool support for domain-specific languages (DSLs) inside the

BEST STUDENT PAPER AWARD (ML) AT ECML 2019
20 September 2019
Guillaume Doquet (A&O) received the Best Student Paper Award (category Machine Learning) at ECML 201

BEST PAPER AWARD - HPCS 2019 - ON SERVER-SIDE FILE ACCESS PATTERN MATCHING
17 July 2019
Francieli Zanon Boito¹ , Ramon Nou², Laércio Lima Pilla³, Jean Luca Bez⁴, Jean-François Méhaut¹, T

BEST FULL PAPER AWARD EDM 2019 - EDUCATIONAL DATA MINING
5 July 2019
DAS3H: Modeling Student Learning and Forgetting for Optimally Scheduling Distributed Practice of Ski

BEST PAPER AWARD - CODIT2019 - STOCHASTIC DUAL DYNAMIC INTEGER PROGRAMMING FOR A MULTI-ECHELON LOT-SIZING PROBLEM WITH REMANUFACTURING AND LOST SALES
14 May 2019
Franco Quezada, Céline Gicquel and Safia Kedad-Sidhoum