Formally Verifying Flow Integrity Properties in Industrial Systems

Abstract : In contrast to other IT systems, industrial systems often do not only require classical properties like data confidentiality or authentication of the communication, but have special needs due to their interaction with physical world. For example, the reordering or deletion of some commands sent to a machine can cause the system to enter an unsafe state with potentially catastrophic effects. To prevent such attacks, the integrity of the message flow is necessary. We provide a formal definition of Flow Integrity. We apply our framework to two well-known industrial protocols: OPC-UA and MODBUS. Using TAMARIN, a cryptographic protocol verification tool, we confirm that most of the secure modes of these protocols ensure Flow Integrity given a resilient network. However, we also identify a weakness in a supposedly secure version of MODBUS.
Type de document :
Communication dans un congrès
SECRYPT 2017 - 14th International Conference on Security and Cryptography, Jul 2017, Madrid, Spain. pp.12
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

http://hal.univ-grenoble-alpes.fr/hal-01527913
Contributeur : Maxime Puys <>
Soumis le : vendredi 26 mai 2017 - 10:39:14
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43
Document(s) archivé(s) le : lundi 28 août 2017 - 16:22:03

Fichier

secrypt17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01527913, version 1

Citation

Jannik Dreier, Maxime Puys, Marie-Laure Potet, Pascal Lafourcade, Jean-Louis Roch. Formally Verifying Flow Integrity Properties in Industrial Systems. SECRYPT 2017 - 14th International Conference on Security and Cryptography, Jul 2017, Madrid, Spain. pp.12. 〈hal-01527913〉

Partager

Métriques

Consultations de la notice

198

Téléchargements de fichiers

103