Research activity

Cher Mathieu,

Ta disparition le 12 octobre nous a toutes et tous atterrés. Notre tristesse est immense. La direction du Laboratoire d’Informatique de Sorbonnne-Université, le LIP6, dont tu étais membre depuis 2001, l’équipe MoVe à laquelle tu appartenais depuis 2012, m’ont demandé de les représenter aujourd’hui. Je me fais aussi le porte-parole des nombreux collègues et amis qui ont partagé tes travaux de recherche et d’enseignement et de tes étudiants qui déplorent ta disparition.
J’adresse tout d’abord toutes nos condoléances à tes parents, à ta sœur et à tes neveux ainsi qu’à toutes celles et ceux qui sont comme nous dans la peine.

Je voudrais rappeler ici ton parcours scientifique depuis ton DEA IARFA à Paris 6 suivi de ta thèse, dirigée par René Lallement à l’École des Ponts, soutenue en septembre 1999. Tu as ensuite entrepris une carrière d’enseignant-chercheur sous l’auspice des méthodes formelles, c’est-à-dire de méthodes fondées sur les mathématiques et la logique. D’abord un poste d’ATER à l’Université d’Évry où tu as commencé une très longue collaboration, poursuivie jusqu’à présent, avec Catherine Dubois. Puis, tu as passé quelque temps à l’Université de Nanterre et à celle de Namur.

Contribution SPI

Tu as rejoint mon équipe SPI au LIP6 en septembre 2001 en tant que Maître de Conférences. Tu y as noué des relations solides, scientifiques et amicales, qui durent encore, avec Marc , Renaud , Vassiliki, etc., et les doctorants Sylvain,Nacera, Bruno, Virgile, Louis, Daniel, Julien, Philippe, Éric, Lionel ...
En tant que membre de l’équipe SPI, tu as été un des piliers de notre projet FOCALIZE. Avec ton légendaire appétit pour les méthodes formelles ultra-précises, tu t’es bien sûr consacré à la partie preuves assistées par ordinateur. Tu as beaucoup donné pour la réussite des ANR liées à FOCALIZE, intitulées Modulogic et SSURF, SSURF dont tu étais le responsable. Les participants à ces ANR appartenaient au CEDRIC (laboratoire d’informatique du CNAM) ou bien à INRIA Rocquencourt et Nancy ou aux sociétés BERTIN et SAFERIVER. Elles et ils se rappellent de nos séances de travail où se mêlaient sérieux, rigueur, mais aussi amitié qui dure encore et humour parfois décapant. Par exemple, on riait beaucoup quand, régulièrement, à « midi moins cinq » pile, tu demandais l’interruption de la séance, car tu affirmais que « l’estomac vide, tu ne pouvais plus réfléchir ». Nous avons toujours obéi à ton cri de famine. Je citerai juste 3 de tes publications de l’année 2003, pour illustrer la largeur de ton spectre de recherche 3 ans seulement après ta thèse « Réutilisation de preuves formelles : une étude pour le système Foc » (avec C. Dubois), « Making proofs in a hierarchy of mathematical structures » (avec V. Prevosto), « A full formalisation of Bell and La Padula Security model » (avec E. Gureghian et T. Hardin).
Ton investissement dans la cybersécurité, bien sûr à l’aide de méthodes formelles, date de ton tout premier encadrement (celui d’Emmanuel). Il portait sur la preuve mathématique des propriétés d’une politique de sécurité et vous avez ainsi découvert quelques bugs subtils dans cette politique pourtant déjà largement étudiée. Charles Morisset, le premier doctorant sur ce sujet que tu as pleinement encadré (thèse soutenue en 2007), m’a dit se souvenir avec beaucoup d’émotion de ton encadrement, qui reste toujours une référence pour lui. Il se rappelle de vos longues discussions autour d’un tableau blanc rempli de symboles mathématiques et du rituel du thé à la menthe de l’après-midi. Charles m’a demandé de rappeler aussi combien ta disponibilité, intellectuelle et humaine, a permis la poursuite de vos échanges scientifiques, mais surtout amicaux tout au long de ces vingt dernières années, jusqu’à ces derniers jours. Tu as soutenu ton habilitation à diriger les recherches, en novembre 2008. Elle était intitulée « Descriptions formelles : Comprendre, corriger, Implanter, réutiliser. Application au contrôle d’accès ». Tous tes sujets de prédilection en un seul titre. J’ai été très heureuse et très fière que ton activité de recherche soit ainsi reconnue.

Contribution de Valérie Triem Tong

C’est sur le domaine de la cybersécurité que porte depuis 2007 ta collaboration avec Valérie Triem Tong, Ludovic Mé et les membres de l’équipe CIDRE de INRIA/Centrale-Supelec Rennes. Valérie m’a demandé de souligner que vous avez pu, grâce à toi Mathieu, construire une fondation mathématique solide, qui a permis de formaliser des problèmes opérationnels de cybersécurité, jusque là empiriquement traités. Vous avez ainsi élaboré des outils sophistiqués, robustes, pour traquer des attaques de systèmes informatiques avancées et ces outils sont en cours de transfert vers l’industrie. Dans ce contexte, tu as coencadré la thèse de Laurent Georget, elle prouve une propriété de sécurité du noyau Linux (15 millions de lignes de code), une belle réussite récompensée par le prix du meilleur article à la Conférence SEFM 2017 (Software Engineering and formal Methods). De même, la thèse d’Aimad Berardy, que tu as co-dirigée, a été récompensée en 2023 par le prix Spécial du Jury décerné par la Gendarmerie nationale. Les doctorants que tu as encadrés à Paris ou à Rennes sont unanimes à louer ta curiosité, ta patience et ta gentillesse.
Voici les quelques mots que Valérie m’a demandé de prononcer en son nom. « D’un point de vue humain, moi, Valérie, j’avais avec Mathieu une complicité rare qui nous permettait de travailler en confiance et d’attaquer des sujets ambitieux et originaux qui ont tous été reconnus dans la communauté. Il était mon collègue, mais surtout mon ami et je garderai de lui sa gentillesse, son humour, ses modèles, ses flèches en Latex, des symboles inconnus de tous, ses feuilles de notes et le Bled de son enfance qu’il a transmis à mes enfants. J’ai eu beaucoup de chance de l’avoir côtoyé ces quinze dernières années. Il me manquera énormément ».

Contribution d’enseignants en informatique de l’UFR d’Ingénierie de Sorbonne-Université

Les enseignants d’informatique de Sorbonne-Université m’ont demandé d’être leur porte-parole et ont rédigé un texte que je vous lis.
Mathieu nous a quittés si jeune que certains de ses collègues enseignants ont eu la chance de le connaître en tant qu’étudiant, brillant et remarqué. Devenu lui-même enseignant-chercheur, Mathieu s’est toujours pleinement investi dans ses missions d’enseignement, avec enthousiasme et dévouement. Aussi exigeant avec lui-même qu’avec les étudiants, il fût à leur écoute, attentif aux difficultés qu’ils pouvaient rencontrer. Il laisse de nombreux supports de cours, toujours détaillés et pédagogiques, ainsi que deux ouvrages de logique et de mathématiques discrètes, écrits pour aider les étudiants des UE où il enseignait.
Travailler avec Mathieu était un plaisir. Il était sérieux, fiable et serviable; le collègue sur lequel on peut toujours compter, qui participe plus que sa part aux tâches collectives. Combien de fois nous a-t-il remplacé(e)s, plus ou moins au pied levé, lorsque nous étions absents?
Mathieu était dynamique, curieux, il n’hésitait pas à se renouveler, à adapter les enseignements pour améliorer la participation et la réussite des étudiants. Il a participé à la création de nouveaux enseignements, il ne voulait pas « s’encroûter » et se contenter de la routine. Il s’était beaucoup investi dans la préparation de l’Agrégation d’Informatique et ses leçons étaient fort appréciées des préparationnaires.
Mathieu était gentil, et très ouvert aux autres. Drôle et généreux, il n’hésitait pas à s’indigner face aux situations injustes. Nous sommes de nombreux collègues à nous être attachés à lui et à sa personnalité si particulière, et à ressentir le grand vide qu’il a laissé.

Contribution de V. Viguié Donzeau-Gouge et moi-même

Toujours dans le domaine de l’enseignement, Véronique Viguié et moi, souhaitons, Mathieu, évoquer ta participation au DESS Logiciels Sûrs, habilité UPMC et CNAM puis au parcours de master 2 du même nom. Les étudiants, futurs ingénieurs dans le domaine de la sûreté et la sécurité, trouvaient difficiles tes cours sur l’interprétation abstraite et sur les assistants à la preuve, mais ils réalisaient très vite que ces contenus étaient une formation décisive dans leur parcours. Tu exigeais d’eux, rigueur, respect des échéances afin de les initier à leurs futures obligations professionnelles. Mais cette exigence était enrobée de beaucoup d’attention, de gentillesse et d’empathie et les anciens étudiants de LS avec qui j’ai échangé ces derniers jours m’ont dit leur grande tristesse.
Nous avons ensemble, toi, Véronique Viguié, François Pessaux et moi, écrit un ouvrage « Concepts et sémantiques des langages de programmation » publié en 2021. Ta minutie dans la rédaction a réussi à nous surprendre plus d’une fois et elle a été l’occasion de quelques plaisanteries. Nous gardons tous les trois le souvenir chaleureux de nos nombreuses discussions sur les contenus, de tes déclarations, parfois un peu énervées, sur nos outils latex et git trop capricieux à ton goût, de toutes tes remarques pleines d’humour que tu faisais en étant très pince-sans-rire. Notre amitié est sortie renforcée de ce travail commun et nous déplorons ta disparition.

Contribution personnelle

Mathieu, je voudrais, pour terminer, te dire quelques mots plus personnels. Nous collaborions depuis 2001 sans aucun accroc, nous comprenant souvent à demi-mot. Nous avions une grande connivence scientifique, aimant tous les deux « les choses au carré » et nous prenions grand plaisir à « pousser ensemble du symbole » pour arriver à nous convaincre mutuellement du bien-fondé d’un énoncé de théorème. Notre collaboration, c’était aussi notre chaleureuse amitié, le plaisir de nos longs échanges à propos de nos familles. Nous comparions les évolutions de tes neveux et de mes petits-enfants qui sont du même âge, nous bavardions beaucoup, sur ta vie au LIP6, sur nos lieux de vie, sur nos questions de santé, sur nos vacances, je te plaisantais sur ton peu d’appétence pour la campagne, mais tu me répondais sur la beauté des plages et le plaisir de se dorer au soleil sans rien faire. Merci pour tous ces moments, Mathieu. Ce sont de précieux souvenirs. Ta disparition me laisse un grand vide et une très grande tristesse.

Texte lu par Thérèse Hardin au cours des obsèques de Mathieu le 28 octobre 2023.

Two past PhD students (2007 - 2011) at Sorbonne University

2000-2022 Publications

• 2022
  • A. BERADY, M. Jaume, V. Viet Triem Tong, G. Guette : “PWNJUTSU: A Dataset and a Semantics-Driven Approach to Retrace Attack Campaigns”, IEEE Transactions on Network and Service Management, vol. 19 (4), Special Issue on Recent Advances in Network Security Management, pp. 5252-5264, (IEEE) (2022)
• 2021
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts and Semantics of Programming Languages 2: Modular and Object‐oriented Constructs with OCaml, Python, C++, Ada and Java”, (ISTE Wiley), (ISBN: Print ISBN:9781786306029 |Online ISBN:9781119851196) (2021)
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts and Semantics of Programming Languages 1: A Semantical Approach with OCaml and Python”, (ISTE Wiley), (ISBN: Print ISBN:9781786305305 |Online ISBN:9781119824121) (2021)
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts et sémantique des langages de programmation 1 : constructions fonctionnelles et impératives avec OCaml, Python, C et C++”, (ISTE Editions), (ISBN: 9781784057015) (2021)
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts et sémantique des langages de programmation 2 : constructions modulaires et objet avec OCaml, Python, C++, Ada et Java”, (ISTE Editions), (ISBN: 9781784057022) (2021)
  • A. BERADY, M. Jaume, V. Viet Triem Tong, G. Guette : “From TTP to IoC: Advanced Persistent Graphs for Threat Hunting”, IEEE Transactions on Network and Service Management, vol. 18 (2), Special Issue on Latest Developments for Security Management of Networks and Services, pp. 1321-1333, (IEEE) (2021)
• 2020
  • M. Jaume, M. Journault, M.‑J. Lesot, P. Manoury, I. Mounier : “Logique pour l’informatique”, (Ellipses), (ISBN: 9782340042612) (2020)
• 2017
  • L. Georget, M. Jaume, G. Piolle, F. Tronel, V. Viet Triem Tong : “Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory”, Proceedings of the 15^th International Conference on Software Engineering and Formal Methods (SEFM 2017), LNCS, Trento, Italy, pp. 1-16, (Springer International Publishing) (2017)
  • L. Georget, M. Jaume, G. Piolle, F. Tronel, V. Viet Triem Tong : “Suivi de flux d’information correct sous Linux”, Actes des 16^es journées AFADL (Approches formelles dans l'assistance au développement de logiciels), Montpellier, France, pp. 19-26 (2017)
  • L. Georget, M. Jaume, G. Piolle, F. Tronel, V. Viet Triem Tong : “Verifying the Reliability of Operating System-Level Information Flow Control Systems in Linux”, 5^th International FME Workshop on Formal Methods in Software Engineering, Buenos Aires, Argentina, pp. 10-16, (IEEE Press) (2017)
• 2016
  • M. Jaume : “Eléments de mathématiques discrètes - Cours, exercices résolus, implémentations avec les langages Python et OCaml”, (Ellipses), (ISBN: 978-2340014800) (2016)
• 2015
  • L. Georget, G. Piolle, F. Tronel, V. Viet Triem Tong, M. Jaume : “Towards a Formal Semantics for System Calls in terms of Information Flow”, Tenth International Conference on Systems (ICONS 2015), Barcelone, Spain, pp. 1-4, (IARIA) (2015)
• 2014
  • M. Jaume, Th. Laurent : “Teaching formal methods and discrete mathematics”, Proceedings of the 1^st Workshop on Formal Integrated Development Environment (F-IDE 2014), vol. 149, Electronic Proceedings in Theoretical Computer Science, Grenoble, France, pp. 30-43 (2014)
• 2013
  • M. Jaume, R. Andriatsimandefitra, V. Viet Triem Tong, L. Mé : “Secure states versus Secure executions: From access control to flow control”, ICISS 2013 - 9^th International Conference on Information Systems Security, vol. 8303, Lecture Notes in Computer Science, Calcutta, India, pp. 148-162, (Springer) (2013)
• 2012
  • 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) (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) (2012)
  • M. Jaume, R. Rioboo : “Développement de systèmes sécurisés avec l’atelier FoCaLiZe”, JFLA - Journées Francophones des Langages Applicatifs - 2012, Carnac, France, pp. 104-118 (2012)
  • T. Bourdier, H. Cirstea, M. Jaume, H. Kirchner : “Formal Specification and Validation of Security Policies”, FPS - 4^th 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) (2012)
  • 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) (2012)
• 2011
  • M. Jaume, V. Viet Triem Tong, L. Mé : “Flow based interpretation of access control: Detection of illegal information flows”, 7^th International Conference on Information Systems Security (ICISS), vol. 7093, Lecture Notes in Computer Science, Kolkata, India, pp. 72-86, (Springer) (2011)
• 2010
  • 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 (2010)
  • T. Bourdier, H. Cirstea, M. Jaume, H. Kirchner : “Rule-based Specification and Analysis of Security Policies”, 5^th International Workshop on Security and Rewriting Techniques - SecReT 2010, Valencia, Spain (2010)
  • M. Jaume, V. Viet Triem Tong, L. Mé : “Contrôle d’accès versus Contrôle de flots”, 10^emes Journées Francophones sur les Approches Formelles dans l'Assistance au développement des logiciels, AFADL 2010, Poitiers, France, pp. 27-41 (2010)
  • T. Bourdier, H. Cirstea, M. Jaume, H. Kirchner : “On Formal Specification and Analysis of Security Policies”, 2010 Grande Region Security and Reliability Day, Saarbrücken, Germany (2010)
• 2009
  • M. Carlier, C. Dubois, L. Habib, M. Jaume : “Politique de contrôle d’accès multi-niveaux : test de conformité vis à vis des flots avec l’outil FoCaL”, AFADL'09 - Approches formelles dans l'assistance au développement des Logiciels, Toulouse, France, pp. 145-160 (2009)
  • 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 (2009)
• 2008
  • M. Jaume : “Descriptions formelles : Comprendre, Corriger, Implanter, Résutiliser. Application au contrôle d’accès”, habilitation, phd defence 11/06/2008 (2008)
  • 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 (2008)
  • L. Habib, M. Jaume, Ch. Morisset : “A formal comparison of the Bell & LaPadula and RBAC models”, Fourth International Conference on Information Assurance and Security, IAS'2008, Naples, Italy, pp. 3-8, (IEEE) (2008)
  • M. Jaume, Ch. Morisset : “Un cadre sémantique pour le contrôle d’accès”, Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, vol. 27 (8), pp. 951-976, (Lavoisier) (2008)
• 2007
  • M. Jaume, Ch. 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, pp. 227-244 (2007)
• 2006
  • M. Jaume, Ch. Morisset : “Towards a formal specification of access control”, Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), Seattle, Washington, United States (2006)
  • Th. Hardin, M. Jaume, Ch. Morisset : “Access control and Rewrite Systems”, 1^st International Workshop on Security and Rewriting Techniques, SecReT'06, Venice, Italy, pp. 2-17 (2006)
  • M. Jaume, Ch. Morisset : “A formal approach to implement access control”, Journal of Information Assurance and Security, vol. 1 (2), pp. 137-148, (Dynamic Publishers Inc., USA) (2006)
• 2005
  • M. Jaume, Ch. Morisset : “Formalisation and Implementation of Access control models”, ITCC 2005 - International Conference on Information Technology: Coding and Computing, Las Vegas, United States, pp. 703-708, (IEEE) (2005)
  • D. Delahaye, M. Jaume, V. Prevosto : “Coq : un outil pour l’enseignement”, Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, vol. 24 (9), pp. 1139-1160, (Lavoisier) (2005)
• 2003
  • E. Gureghian, Th. Hardin, M. Jaume : “A full formalisation of the Bell and La Padula security model”, (2003)
  • V. Prevosto, M. Jaume : “Making proofs in a hierarchy of mathematical structures”, Calculemus 2003 - 11^th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Rome, Italy, pp. 89-100, (Aracne) (2003)
  • C. Dubois, J. Grandguillot, M. Jaume : “Réutilisation de preuves formelles : une étude pour le système Foc”, Journées Francophones des Langages Applicatifs, JFLA'03, Chamrousse, France, pp. 63-76 (2003)
• 2002
  • M. Jaume : “On greatest fixpoint semantics of logic programming”, Journal of Logic and Computation, vol. 12 (2), pp. 321-342, (Oxford University Press (OUP)) (2002)
• 2000
  • M. Jaume : “Logic programming and Co-inductive definitions”, International Workshop, Computer Science Logic, CSL'2000, vol. 1862, Lecture Notes in Computer Science, Fischbachau, Germany, pp. 343-355, (Springer) (2000)