Direction de recherche : Béatrice BÉRARD

Noninterférence et canaux cachés dans les systèmes temporisés

Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles : il peut s'agir d'informations stratégiques militaires ou financières, ou bien d'informations personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les méthodes formelles de vérification sont nécessaires pour garantir la sûreté et la sécurité du système. Ces techniques s'appliquent sur des modèles du système où certains paramètres ? en particulier des paramètres quantitatifs ? peuvent avoir été abstraits. Ces paramètres ont pu être utilisés dans des attaques de systèmes réputés sûrs. Les modèles actuels intègrent donc ces informations, qui se rapportent le plus souvent à l'écoulement (continu) du temps ou aux lois de probabilités qui régissent le fonctionnement du système. Les modèles intègrent d'autre part le découpage de l'application en divers processus, mûs par des buts différents, voire contraires : l'un peut chercher à dissimuler de l'information tandis que l'autre cherche à la découvrir. Lorsque le fonctionnement de tous les processus est partiellement ou totalement inconnu, les méthodes formelles doivent considérer tous les cas possibles, ce qui est en général impossible en théorie ? s'il existe un nombre infini de possibilités ? ou en pratique ? s'il existe trop de possibilités pour que l'on puisse les envisager exhaustivement. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un canal de communication dans un système décrit par un transducteur. Malgré les limites imposées par ce modèle, nous montrons que le problème de synthèse est indécidable en général. Cependant, lorsque le système est fonctionnel, c'est-à-dire que son fonctionnement externe est toujours le même, le problème devient décidable. Nous généralisons ensuite le concept d'opacité aux systèmes probabilistes, en donnant des mesures groupées en deux familles. Lorsque le système est opaque, nous évaluons la robustesse de cette opacité vis-à-vis des informations données par les lois de probabilités du système. Lorsque le système n'est pas opaque, nous évaluons la taille de la faille de sécurité induite par cette non opacité. Enfin, nous étudions le modèle des automates temporisés à interruptions (ITA) où les informations sur l'écoulement du temps sont organisées en niveaux comparables à des niveaux d'accréditation. Nous étudions les propriétés de régularité et de clôture des langages temporisés générés par ces automates et proposons des algorithmes de model-checking pour des fragments de logiques temporelles temporisées. Ces résultats permettent la vérification de propriétés telles que « le système est (dans un état) prêt avant les 7 premières unités de temps de fonctionnement du système ».

Publications 2009-2021

• 2021
  • B. Bérard, S. Haddad, C. Picaronny, M. Safey El Din, M. Sassolas : “Polynomial interrupt timed automata: Verification and expressiveness”, Information and Computation, vol. 277, pp. 104580, (Elsevier) (2021)
• 2018
  • B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas : “Opacity for linear constraint Markov chains”, Discrete Event Dynamic Systems, vol. 28 (1), pp. 83-108, (Springer Verlag) (2018)
• 2016
  • B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas : “Opacity for Linear Constraint Markov Chains”, (2016)
  • B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas : “Preserving opacity on Interval Markov Chains under simulation”, Proceedings of 13^th International Workshop on Discrete Event Systems (WODES) 2016, IEEE, Xi'an, China, pp. 319-324 (2016)
• 2015
  • B. Bérard, J. Mullins, M. Sassolas : “Quantifying Opacity”, Mathematical Structures in Computer Science, vol. 25 (Special issue 2), pp. 361-403, (Cambridge University Press (CUP)) (2015)
  • B. Bérard, S. Haddad, C. Picaronny, M. Safey El Din, M. Sassolas : “Polynomial Interrupt Timed Automata”, The 9^th Workshop on Reachability Problems (RP'15), vol. 9328, Lecture Notes in Computer Science, Warsaw, Poland, pp. 20-32, (Springer) (2015)
  • B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas : “Probabilistic Opacity in Refinement-Based Modeling”, (2015)
• 2012
  • B. Bérard, S. Haddad, M. Sassolas : “Interrupt Timed Automata: verification and expressiveness”, Formal Methods in System Design, vol. 40 (1), pp. 41-87, (Springer Verlag) (2012)
  • B. Bérard, S. Haddad, M. Sassolas, N. Sznajder : “Concurrent Games on VASS with Inhibition”, 23^rd International Conference on Concurrency Theory (CONCUR'12), vol. 7454, Lecture Notes in Computer Science, Newcastle upon Tyne, United Kingdom, pp. 39-52, (Springer) (2012)
  • G. Benattar, B. Bérard, D. Lime, J. Mullins, O. Roux, M. Sassolas : “Channel Synthesis for Finite Transducers”, International Journal of Foundations of Computer Science, vol. 23 (6), pp. 1241-1260, (World Scientific Publishing) (2012)
• 2011
  • M. Sassolas : “Noninterférence et canaux cachés dans les systèmes temporisés”, thèse, soutenance 28/11/2011, direction de recherche Bérard, Béatrice (2011)
  • B. Bérard, J. Mullins, M. Sassolas : “Quantifying Opacity”, (2011)
  • M. Sassolas, M. Chechik, S. Uchitel : “Exploring Inconsistencies between Modal Transition Systems”, Software and Systems Modeling, vol. 10 (1), pp. 117-142, (Springer Verlag) (2011)
  • G. Benattar, B. Bérard, D. Lime, J. Mullins, O. Roux, M. Sassolas : “Channel Synthesis for Finite Transducers”, AFL 2011 - 13^th International Conference on Automata and Formal Languages, Debrecen, Hungary, pp. 79-92 (2011)
• 2010
  • G. Benattar, B. Bérard, D. Lime, J. Mullins, O. Roux, M. Sassolas : “Covert Channel Synthesis for Transducers”, (2010)
  • B. Bérard, J. Mullins, M. Sassolas : “Quantifying Opacity”, 7^th International Conference on Quantitative Evaluation of Systems (QEST 2010), Williamsburg, Virginia, United States, pp. 263-272, (IEEE Computer Society) (2010)
  • B. Bérard, S. Haddad, M. Sassolas : “Real Time Properties for Interrupt Timed Automata”, 17^th International Symposium on Temporal Representation (TIME 2010), Paris, France, pp. 69-76, (IEEE Computer Society Press) (2010)
  • B. Bérard, S. Haddad, M. Sassolas, M. Zeitoun : “Distributed Synthesis with Incomparable Information”, (2010)
• 2009
  • G. Benattar, B. Bérard, D. Lime, J. Mullins, O. Roux, M. Sassolas : “Covert Channels with Transducers”, Proceedings of the LICS Workshop on Foundations of Computer Security (FCS'09), Los Angeles, California, United States (2009)