Publications

- Daniel J. Dougherty, Claude Kirchner, Hélène Kirchner and Anderson Santana de Oliveira, Modular Access Control via Strategic Rewriting. 12th European Symposium On Research In Computer Security, ESORICS'07, 2007.
- Julien Blond and Charles Morisset, Un moniteur de référence sûr d'une base de données, TSI (Technique et Scoence Informatiques), 2007.
- Charles Morisset and Anderson Santana de Oliveira, Automated Detection of Information Leakage in Access Control, Security and Rewriting Techniques, SecReT 2007.
- Mathieu Jaume and Charles Morisset, Contrôler le contrôle d'accès : Approches formelles., Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'07), Namur (Belgium), June 2007.
- Anderson Santana de Oliveira, Eric Ke Wang, Claude Kirchner, Hélène Kirchner, Weaving Rewrite-Based Access Control Policies, 5th ACM Workshop on Formal Methods in security Engineering : From Specification to Code, FMSE'07.
- Charles Morisset, Sémantique des systèmes de contrôle d'accès, PhD thesis, UPMC, Sept 2007.
- Andréa-Diane Kadja et Florian Brecht, Implantation d'une politique de contrôle d'accès discrétionnaire avec FOCAL., Rapport de stage, 1ère année de Master, UPMC, Sept 2007.
- Lionel Habib, Formalisation, comparaison et implantation d'un modèle de contrôle d'accès à base de rôles., Rapport de stage, 2ème année de Master, UPMC, Sept 2007.
- F. blanqui, T. Hardin and P. Weis, On the implementation of construction functions for non-free concrete data types., ESOP07 (European Symposium on Programming), LNCS 4421, 2007.
- Eric Jaeger and Catherine Dubois, Why Would You Trust B?., Conference on Logic Programming Artificial Intelligence and Reasoning, LPAR 2007, LNCS.
- Anderson Santana de Oliveira, Réécriture et Modularité pour les Politiques de Sécurité, Thèse de Doctorat, Mars 2008, Nancy.
- M. Carlier and C. Dubois, Functional Testing in the Focal environment, In Test And Proof, 9-11 Avril 2008, B. Berckert, R. Hahnle, Eds., LNCS 4966, pp. 84--98, 2008.
- Horatiu Cirstea, Pierre-Etienne Moreau and Anderson Santana de Oliveira, Rewrite Based Specification of Access Control Policies, Security and Rewriting Techniques, SecReT 2008, Pittsburgh, USA.
- Claude Kirchner, Hélène Kirchner and Anderson Santana de Oliveira, Analysis of Rewrite-Based Access Control Policies., Security and Rewriting Techniques, SecReT 2008, Pittsburgh, USA.
- Horatiu Cirstea, Pierre-Etienne Moreau and Anderson Santana de Oliveira, Information Leakage Detection in Access Control Policies, Third Franco-Japanese Computer Security Workshop, Nancy, France, 2008.
- Horatiu Cirstea, Pierre-Etienne Moreau and Anderson Santana de Oliveira, Détection automatisée des flux d'informations (Poster), 3SGS'08 Workshop Surveillance, Sûreté et Sécurité des Grands Systèmes, Troyes, Juin 2008.
- L. Habib, M. Jaume and C. Morisset, A formal comparison of the Bell & LaPadula and RBAC models, Fourth International Conference on Information Assurance and Security, IAS'2008. Naples, Italy, September 2008. IEEE CS Press.
- M. Jaume and C. Morisset, Un cadre sémantique pour le contrôle d'accès, Technique et Science Informatique, TSI 27(8):951-976, 2008.
- P. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, T. Hardin, M. Jaume, C. Morisset, F. Pessaux, R. Rioboo, P. Weis, Trusted Software within FoCaL, C&ESAR 2008 - Trusting Trusted Computing ?, Rennes, Décembre 2008.
- M. Jaume. Descriptions formelles : Comprendre, corriger, implanter, réutiliser. Applicationau contrôle d'accès. Habilitation à Diriger des Recherches, UPMC, Novembre 2008.
- P. Ayrault, T. Hardin and F. Pessaux. Development life cycle of critical software under FoCaL, 2nd International Workshop on Harnessing Theories for Tool Support in Software, TTSS'08, Istambul, 2008.
- E. Jaeger and T. Hardin, A few remarks about formal development of secure systems, 11th IEEE High Assurance Systems Engineering Symposium, HASE'08 - Chine, 2008.
- M. Jaume, Un cadre formel pour le contrôle d'accès., Journées nationales du GDR GPL (Génie de la Programmation et du Logiciel), Toulouse, Janvier 2009.
- M. Carlier, C. Dubois, L. Habib and M. Jaume, Politique de contrôle d'accès multi-niveaux : test de conformité vis à vis des flots avec l'outil FoCaL., Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'09, Toulouse, Janvier 2009.
T.Bourdier, H. Cirstea, P.E. Moreau and A. Santana de Oliveira, Analysis of Lattice-Based Access Control Policies using Rewriting Systems and Tom., First Luxembourg Day on Security and Reliability, Luxembourg, Février 2009.
- P.Ayrault, T.Hardin and F.Pessaux, Development of a generic voter under Focal, Third International Conference on Tests and Proofs (TAP09), Zurich, July 2009.
- I. Noyer and R. Rioboo, Reusing proofs in a mathematical library, Calculemus 2009, 16th Symposium on the integration of symbolic computation and mechanised reasoning, July 2009, Ontario, Canada.
- L. Habib, M. Jaume and C. Morisset, Formal definition and comparison of access control models, Special Issue on Access Control and protocols of the Journal of Information Assurance and Security (JIAS), 2009.
- M. Carlier, Test automatique de propriétés dans un atelier de développement de logiciels sûrs, Thèse de doctorat, Octobre 2009.
- N. Bertaux and David Delahaye. Developping structured libraries using the FOCAL environment. 1st Workshop on Modules and Libraries for Proof Assistants (MLPA'09).
- C. Faure (SafeRiver), Computer Aided Extrinsic Robustness Verification, Workshop SAFA 2009 (Sophia-Antipolis Formal Analysis group).
- Tony Bourdier, Automatic analysis of firewalls using tree automata, 2010 Grande Region Security and Reliability Day, Saarbruken, Germany, 2010.
- Tony Bourdier, Horatiu Cirstea, Mathieu Jaume and Hélène Kirchner, On Formal Specification and Analysis of Security Policies, 2010 Grande Region Security and Reliability Day, Saarbruken, Germany, 2010. (full paper available on HAL)
- Eric Jaeger, Study of the benefits of using deductive formal methods for secure developments, PHD Thesis, UPMC, 2010.
- Mathieu Jaume, Valérie Viêt Triêm Tông and Ludovic Mé, Contrôle d'accès versus Contrôle de flots, Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL2010, Poitiers, Juin 2010. pdf
- Tony Bourdier, Horatiu Cirstea, Mathieu Jaume and Hélène Kirchner, Rule-based Specification and Analysis of Security Policies, 5th International Workshop on Security and Rewriting Techniques, Valencia, Spain, 2010.
- Renaud Rioboo, Invariants for the FOCAL language, Annal of Mathematics and Artificial Intelligence, 56(3):273-296, Springer, 2010.
- M. Carlier, C. Dubois and A. Gotlieb. Constraint reasonning in FocalTest, 5rd International Conference on Software and Data Technologies (ICSOFT'10), July 2010.
- D. Delahaye, C. Dubois et P.N. Tollite. Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize, 21ème Journées Francophones des Langages Applicatifs (JFLA), 2010.
- T. Bourdier, H. Cirstea, M. Jaume, and H. Kirchner. Operational specification and verification of security policies, Annual Meeting of the IFIP Working Group 1.6. on Term Rewriting (associated to RTA 2010), Edinburgh, UK, July 2010.