Expires soon Edf

Thèse - Apports des systèmes de gestion de registres distribués pour la surveillance automatique - H/F

  • CDI
  • Chatou (Yvelines)
  • IT development

Job description

Sujet de thèse : Vérification formelle de smart contract pour la certification distribuée d'opérations industrielles.

 

Le contexte

La surveillance des opérations de fabrication et de maintenance des équipements des centrales nucléaires est une activité fastidieuse et onéreuse qui requiert le concours de nombreuses opérations humaines ne garantissant in fine qu'une surveillance partielle (le suivi est soumis à la disponibilité des agents de surveillance). Dans une dynamique d'amélioration continue de la sûreté et de la performance de ses outils de production, EDF envisage de simplifier et de rendre plus pertinents les moyens de surveillance de ces processus de fabrication et de maintenance. L'objectif technique est de développer un outil pour automatiser l'enregistrement de certificats de conformité de la réalisation d'une opération industrielle dans un registre distribué sécurisé et accessible à tous les acteurs concernés de la filière nucléaire. Les cas d'usages concrets sont très nombreux et on peut citer parmi eux : l'identification de contrefaçons de composants électroniques qualifiés, le contrôle systématique de la qualité des soudures (à l'aide d'un casque de soudeur connecté), l'amélioration de la qualité des essais de contrôle non destructifs sur les équipements sous pression, la vérification du respect des protocoles d'essais réalisés en laboratoires...

Les nouveaux protocoles de gestion de registres distribués tels que les Blockchain, Tangle et Hashgraph, de par leurs bonnes propriétés (distribués, sécurisés, auditables), apportent des solutions technologiques favorisant a priori l'atteinte de cet objectif. Toutefois, pour que ceux-ci soient effectivement adoptés, il est nécessaire de bien spécifier la portée et le comportement attendu d'un tel dispositif. En effet, de nombreuses questions de conception se posent :

? Quel est le protocole de consensus le plus adapté ?

Cette question nous amènera à analyser la « chaine de confiance » qui lie les différents acteurs impliqués dans les processus de fabrication et de maintenance et à dimensionner les flux de communication entre chacun. La discussion permettra en particulier de s'assurer de l'adéquation des nouveaux protocoles avec le contexte du nucléaire et de les confronter aux protocoles traditionnels centralisés.

? Comment spécifier l'interface entre l'outil de surveillance et les objets suivis ?

La surveillance est une opération requérant une connaissance actualisée des objets suivis. Quels que soient les moyens choisis pour fournir à l'outil de surveillance cette connaissance source (dans la terminologie de la blockchain, on parle d'oracle), il est nécessaire de garantir leur qualité et leur sécurité.

? Comment intégrer ce nouveau dispositif numérique dans le système d'information d'EDF et l'interfacer avec ceux des autres partenaires de la filière nucléaire ?

Les éléments de réponse à cette problématique se formuleront en termes d'architectures logicielles, de télécommunication, de cybersécurité, et plus généralement d'ingénierie système.

? Comment maîtriser les risques de dysfonctionnement de l'outil de surveillance ?

La mise en place d'un tel dispositif implique notamment la vérification formelle de la correction de l'implémentation des programmes assurant cette automatisation (smart contracts, protocole... ainsi qu'une analyse de la fiabilité du matériel nécessaire à l'exécution de ces programmes.

Toutes ces problématiques peuvent être formalisées et discutées à travers de nombreux champs des sciences de l'ingénieur. La R&D d'EDF a déjà contribué sur plusieurs de ces sujets d'étude, en particulier sur le dernier [2,3,4], et souhaite à présent recruter un doctorant pour approfondir ces travaux.

Le sujet

Dans le contexte du nucléaire, pour toute numérisation des procédures ou procédés importants pour la sûreté, les autorités de sûreté sont susceptibles d'exiger des garanties formelles sur le bon fonctionnement des nouveaux dispositifs numériques. Cette position règlementaire est d'autant plus probable dans le cas de la technologie blockchain, étant donnés le changement important de paradigme qu'elle représente par rapport aux solutions centralisées qui sont bien maîtrisées et le caractère inaltérable - et donc impossible à corriger - des smart contracts (programme dont le code et les résultats d'exécutions sont enregistrés dans la blockchain). De telles exigences doivent être anticipées au plus tôt.

L'état de l'art sur les méthodes formelles appliquées aux programmes basés sur le paradigme blockchain est foisonnant. Les contributions consistent à proposer des outils et méthodes pour offrir des garanties, a priori (développement de programmes corrects par conception) ou a posteriori (vérification formelle de programme), sur les propriétés attendues du (des) protocole(s) sous-jacent(s) à la blockchain (cohérence, vivacité, équité...) [5,6] ou de smart contracts (absence de défauts intrinsèques, conformité à une spécification formelle) [7,8]. Afin d'accompagner les choix de conception du projet industriel susmentionné vers des options favorables à l'obtention de garanties formelles, le candidat devra bien maîtriser cet état de l'art, éprouver les méthodologies les plus prometteuses sur le cas considéré et si besoin, les étendre pour les adapter au mieux aux solutions choisies. En outre, la blockchain est une brique intégrée dans un eco-système logiciel diversifié donc l'ingénierie de preuve risque d'être complexe et devra vraisemblablement intégrer plusieurs techniques également diversifiées de méthodes formelles. C'est dans l'intégration de plusieurs approches distinctes au sein d'une méthodologie outillée que réside l'originalité scientifique de ce travail (dans le sillon de l'approche présentée dans [9]).

Références :

[1] Omar Dib, Kei-Leo Brousmiche, Antoine Durand, Eric Thea and Elyes Ben Hamida. Consortium Blockchains: Overview, Applications and Challenges. International Journal on Advances in Telecommunications, vol 11, n° 1 & 2, pp. 51 - 64, IARIA, 2018.

[2] Tesnim Abdellatif and Kei-Léo Brousmiche. Formal verification of smart contracts based on users and blockchain behaviors models. In IFIP NTMS International Workshop on Blockchains and Smart Contracts (BSC), Paris, France, February 2018.

[3] Zeinab Nehai, Pierre-Yves Piriou and Frédéric Daumas. Model checking of smart contracts. In IEEE International Conference on Blockchain, Halifax, Canada, August 2018.

[4] Pierre-Yves Piriou, Jean-François Dumas. Simulation of stochastic blockchain models. In Proceeding on 14th European Dependable Computing Conference (EDCC'18), Workshop on Dependable Blockchain, IEEE, Iasi, Romania, September 2018.

[5] George Pîrlea. Mechanising Blockchain Consensus, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 78-90, January 2018, Los Angeles (CA - USA).

[6] E. Anceaume, A. D. Pozzo, R. Ludinard, M. Potop-Butucaru, and S. Tucci Piergiovanni. Blockchain Abstract Data Type. CoRR, abs/1802.09877, 2018.

[7] C. B. Bozman, M. Iguerblala, M. Laporte, F. Le Fessant, and A. M. Mesbout. Liquidity : Ocaml pour la blockchain. In Journées Francophones des Langages Applicatifs JFLA'18, 2018, Banyuls-sur-Mer (France).

[8] I. Sergey, A. Kumar, and A. Hobor. Scilla: a smart contract intermediate level language. In CoRR, abs/1801.00687, 2018.

[9] M. Charpentier and K. M. Chandy. 1999. Towards a Compositional Approach to the Design and Verification of Distributed Systems. In Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I - Volume I (FM '99), Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.), Vol. I. Springer-Verlag, London, UK, UK, 570-589.



Ideal candidate profile

Etudiant diplômé d'un Master 2 de recherche en informatique théorique.

Une spécialisation dans les méthodes formelles serait apprécié.