Gruppo di ricerca : SPI - Semantics, Proofs and Implementations
Axe : .Responsabile del gruppo di ricerca :
Thérèse Hardin
Presentazione breve
The SPI team build formal tools for critical software. The language, called Focal, for specifications and programs, allows to mix declarations, definitions, properties and proofs in a compilation unit. Focal has strong object features (inheritance, late binding), high level generic parametrization, and an encapsulation mechanism. Proofs are currently done within Coq or by an automatic prover called Zenon which issues Coq proofs when it success. The compiler produces OCaml sources, Coq sources and automatic documentation (XML files). The distribution comes with an important library of algebraic structures. The development of Focal is done in collaboration with the team CPR of CEDRIC lab. CNAM and of researchers at INRIA.
The SPI team also works on the construction of a general model of security policies, which allow two compare specifications and implementations of access control policies. This model is to be described within Focal, which as already been successfully used to specify several security policies and their implementations (annex 17-Doc 2320 of Civil aviation - CPR team, SQL reference monitor).
formal specifications, proofs and automatic deduction, correctness of implementations, critical systems, deduction modulo
Selected publications
- M. Jaume, V. Viet Triem Tong, G. Hiet : “Spécification et mécanisme de détection de flots d'information illégaux”Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, vol. 31 (6), pp. 713-742, (Lavoisier)[Jaume 2012c]
- D. Doligez, M. Jaume, R. 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, Beijing, China, (ACM)[Doligez 2012]
- M. Jaume : “Semantic comparison of security policies: from access control policies to flow properties”Workshop on Semantic Computing and Security, WSCS'2012, IEEE CS Security and Privacy Workshops, San Francisco, United States, pp. 60-67, (IEEE)[Jaume 2012a]
- M. Jaume, V. Viet Triem Tong, L. Mé : “Flow based interpretation of access control: Detection of illegal information flows”7th International Conference on Information Systems Security (ICISS), vol. 7093, Lecture Notes in Computer Science, Kolkata, India, pp. 72-86, (Springer)[Jaume 2011]
- T. Bourdier, H. Cirstea, M. Jaume, H. Kirchner : “Formal Specification and Validation of Security Policies”FPS - 4th Canada-France MITACS Workshop on Foundations and Practice of Security - 2011, vol. 6888, Lecture Notes in Computer Science, Paris, France, pp. 148-163, (Springer, Heidelberg)[Bourdier 2012]
- M. Jaume : “Security rules versus Security properties”Sixth International Conference on Information Systems Security (ICISS 2010), vol. 6503, Lecture Notes in Computer Science, Gandhinagar, India, pp. 231-245[Jaume 2010a]
- L. Habib, M. Jaume, Ch. Morisset : “Formal definition and comparison of access control models”Journal of information assurance and security (JIAS), vol. 4 (4), pp. 372-381[Habib 2009]
- Ph. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, Th. Hardin, M. Jaume, Ch. Morisset, F. Pessaux, R. Rioboo, P. Weis : “Trusted Software within Focal”Trusting Trusted Computing ?, Rennes, France, pp. 162-179[Ayrault 2008]
- Ph. Ayrault, Th. Hardin, F. Pessaux : “Development life cycle of critical software under FoCal”Electronic Notes in Theoretical Computer Science, vol. 243, pp. 15-31, (Elsevier)[Ayrault 2009a]
- É. Jaeger, Th. Hardin : “A Few Remarks About Formal Development of Secure Systems”High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11th IEEE, Nanjing, China, pp. 165-174, (IEEE)[Jaeger 2008]
gennaio 2004 → dicembre 2011