Supervision : Béatrice BÉRARD

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

Information systems have become ubiquitous and are used to handle each day more and more data. This data is increasingly confidential: it may be strategic military or financial information, or private information. Any leakage of this data can be harmful in many different ways, such that human casualties, money loss, privacy breaching or identity theft. The use of formal methods and especially formal verification of such systems has become necessary to ensure both the safety of the behavior of the system and the security of the information it handles. These techniques are applied on models of the system where some parameters ? especially quantitative parameters ? may have been abstracted. These omitted parameters have sometimes been used in order to breach the security of supposedly secure systems. Nowadays, models tend to include more of this information, which is often relative to the (continuous) elapsing of time or to the probability distributions that rule the system's behavior. Models also include the architecture of the systems as several processes, who may have different, or even contradictory, goals: one may want to keep a secret while the other tries to discover it. When the behavior of all processes is partially or completely unknown, formal methods have to consider all possible cases, which is in general impossible (if there exist an infinite number of choice) or intractable (if there exist too many possibilities to consider them all). The contributions of this thesis are threefold. First, we study the problem of synthesis of a communication channel inside a system given as a transducer. Even though the model of transducers is syntactically limiting, we show that this synthesis problem is undecidable in general. However, when the system is functional, meaning that its behavior from an external point of view is always the same, the problem becomes decidable. We then generalize the concept of opacity to probabilistic systems, by giving measures separated in two groups. When the system is opaque, we evaluate the robustness of this opacity with respect to the bias induced by the probability distributions in the system. When the system is not opaque, we evaluate the size of the security hole opened by this non-opacity. Finally, we study the model of Interrupt Timed Automata (ITA) where information about time elapsing is organized along levels, which therefore resemble accreditation levels. We study properties of regularity and closure of the time languages accepted by these automata and give some model-checking algorithms for fragments of timed temporal logics. These results allow to verify formulas such as ?the system is (in state) ready before 7 time units have elapsed since the beginning of the system's execution?.

2009-2021 Publications

• 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”, thesis, phd defence 11/28/2011, supervision 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)