Vérification de propriété de cybersécurité temporisés grâce aux méthodes formelles.

école doctorale

équipe

MOSEL-VERIDIS

contexte

The pervasiveness of cyber-physical systems is highly increasing, raising many safety and security concerns. For instance, the observation of an user's interac- tions with a system should not give secret information to an attacker. Take the example of an attacker trying to guess a password by writing down a random input. If the system follows a naive algorithm to check the correctness of the password (i.e. checking if every letter is correct one by one and returning f alse as soon as a wrong letter is detected), the attacker can guess how many of the first letters of their input are correct. In order to deal with this kind of issue, we request systems to be opaque, meaning that secret behaviours of the system (the correct password) give the same observations to an attacker as some public behaviours of the system. These observations may include timing delays, energy consumption,. . . Formal methods aim at tackling problems such as opacity through the verifi- cation of formal properties on a model abstracting the real system. A well-known formal model to reason about timed systems is timed automata, an extension of finite-state automata with continuous clocks measuring time. Timed automata have been extensively used to verify safety properties, but not so much security properties, with some exceptions.

spécialité

Informatique

laboratoire

LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications