Préservation de l'opacité par raffinement de systèmes spécifiés par des chaînes de Markov discrètes à intervalles

Les méthodes formelles permettent de modéliser et concevoir des systèmes informatiques critiques, notamment dans les domaines à fort risque humain que sont les transports de personne ou les centrales énergétiques, par exemple. L'une des méthodes de conception est celle dite de raffinements successifs, étapes lors desquelles les spécifications du système sont ajustées afin que le produit final soit le plus conforme possible aux exigences initiales. Le principe du raffinement est tel qu'il ne doit pas être destructif : le modèle raffiné doit vérifier au moins les mêmes requis déjà validés par le modèle précédent - par exemple, l'absence de blocage, ou la terminaison du programme dans un état acceptant. Parmi ces requis, le système doit parfois valider des requis non-fonctionnels, tels que des propriétés de sécurité. Notamment, on se penche davantage sur la propriété d'opacité libérale. Pour modéliser les systèmes informatiques ainsi que de tels requis non-fonctionnels, on a besoin de méthodes quantitatives. Ainsi, nous choisissons comme cadre théorique le modèle de la IDTMC. Ce modèle a pour intérêt d'avoir un aspect non-déterministe. En réalité, c'est une extension du modèle de PTS : en ce sens, on considère qu'une IDTMC représente une spécification, que l'on peut implémenter par un PTS. Les PTS eux-mêmes sont des modèles probabilistes, qui permettent la mesure de propriétés quantitatives. Le second avantage de ce type de modèle est l'existence de trois types de raffinement : fort, faible et complet. La problématique principale liée au raffinement de systèmes sécurisés est la suivante : le fait qu'une spécification vérifie une propriété de sécurité donnée n'est pas une condition nécessaire au fait que son raffinement la vérifie également. Le but est donc de trouver, dans notre cadre théorique, une notion de raffinement qui préserve la propriété de sécurité que l'on étudie. L'opacité est une propriété de sécurité introduite avec le modèle du LTS, puis étendue aux PTS : elle traduit la capacité d'un observateur extérieur à déduire l'état d'un prédicat secret en observant uniquement la partie publique des exécutions du programme. Sa première définition est une définition binaire ; en étendant la notion aux PTS, on introduit un aspect probabiliste en définissant l'opacité libérale, qui mesure la non-opacité du système, et l'opacité restrictive, qui mesure son opacité effective. Il est alors possible d'étendre à nouveau ces notions aux IDTMC : il suffit de calculer l'opacité dans le pire des cas pour l'ensemble des implémentations des IDTMC. Ainsi, nous prouvons les résultats suivants. Tout d'abord, on prouve que l'opacité libérale dans une IDTMC non-modale, c'est-à-dire complètement définie, se calcule en un temps fini, doublement exponentiel. Nous proposons un algorithme de calcul. De plus, on prouve qu'il est possible d'approcher l'opacité libérale dans une IDTMC dans le cas général, en un temps doublement exponentiel également. Nous proposons comme contribution originale une extension de l'algorithme de calcul du cas non-modal, et nous prouvons sa correction. Enfin, on prouve que l'opacité libérale dans une spécification est préservée après raffinement faible, ce qui généralise un résultat similaire mais qui ne considérait que le raffinement fort. En définitive, nous réalisons une preuve de concept destinée à être reproduite pour d'autres modèles et propriétés de sécurité similaires, telles que les Propriétés Rationnelles de Flux d'Information (RIFP) dont est issue l'opacité.

Abstract

Formal methods can help to design any computer system - softwares, protocols, architectures, etc. Indeed, developping a system usually consists in refining it. The refined system is then a more precise one, with some more features. Thus, all these stages lead to a final product which is a working implementation of the initial specification. The key issue is as follows: each refined system must at least verify all the properties verified by the previous one. This must be the case for behaviour properties (like the absence of any deadlock) and for security properties. This issue is relatively easily resolved when it is about usual behaviour properties, but security is trickier to model. Therefore, one cannot ensure the fact that a refined system verifies the same security properties as the previous system. This essay aims to highlight a particular security property, opacity, for which we prove that it is preserved when a system is refined. Opacity is linked to the probability for a passive external observer to know the content of a secret, only by observing the public outputs of the system. The framework is as follows. In order to modelize our specifications, we define the Interval Discrete-Time Markov Chain (IDTMC), which is a generalisation of the Probabilistic Transition System (PTS). The probabilistic aspect is a way to introduce quantitative measurement on our models. Since IDTMC are non-deterministic, they carry a higher layer of abstraction than the PTS model. On this framework, one can define three types of refinement: strong, weak and thorough. Since opacity is already defined on PTSs, we define its extension to IDTMC. Particularly, one can differentiate liberal opacity (the measure of non-opacity) from restrictive opacity (the measure of effective opacity). The extension is directly defined by stating the fact that the opacity of a secret in a IDTMC is the worst case among all the PTSs that implement this specification. Then we prove the following theorems. First, if we consider a non-modal IDTMC, i.e. a specification for which each transition has a non-zero probability, then the liberal opacity of any secret is computable in 2EXP-time. We provide an algorithm to compute this value. Then, for the general case, we prove that the liberal opacity can be approximate in 2EXP-time. This original contribution comes with an extension of the previous algorithm, for which we prove its correctness. Finally, we solve the main issue of this essay: liberal opacity in a specification is preserved when the system is weakly refined. This contribution expands a similar result, which only considered strong refinement. These results lead to a proof of concept for the fact that secured systems can be refined and keep their security properties, for a certain type of properties. This can be especially generalised to all Rational Information Flow Properties (RIFP).