2020 | TransForm: Transactions Formelles

Axe : Scilex
Coordinateurs : Évelyne Contejean, LRI, équipe VALS
Stefania Dumbrava, ENSIIE & Samovar
Laboratoire gestionnaire : LRI
Autres laboratoires impliqués : SAMOVAR
Équipes concernées et liste des participants :

— Équipe Méthodes (Samovar) : Catherine Dubois, Stefania Dumbrava, Julien Forest
— Équipe Vals (LRI, LMF) : Thibaut Balabonski, Véronique Benzaken, Évelyne Contejean, Chantal Keller
— Nomadic Labs : Zaynah Dargaye, Germán Delbianco, Julien Tesson


Présentation :

Contexte, positionnement et objectifs scientifiques
Les applications centrées données se déploient maintenant à très grande échelle, par exemple pour le commerce électronique, pour la gestion de crises sanitaires, ou encore pour la sécurité du territoire. Ces applications impliquent des masses de données de plus en plus grandes, qui sont précieuses et dont la disponibilité, l’intégrité et la sûreté sont cruciales.
Les systèmes de bases de données, bien que très utilisés en pratique, n’offrent cependant pas encore les mêmes garanties de sûreté que d’autres systèmes critiques. Alors que dans le domaine de l’avionique par exemple, de gros efforts sont faits aujourd’hui pour spécifier les systèmes et leurs garanties et vérifier que ces systèmes répondent à leur spécification à l’aide de méthodes formelles, les garanties de sûreté des systèmes de bases de données reposent encore à ce jour sur des méthodes plus traditionnelles mais moins fortes. Ainsi, si les algèbres sous-jacentes aux bases de données forment une théorie élégante et bien comprise, la fidélité de leur mise en oeuvre par les systèmes de gestion de bases de données eux-mêmes reste imparfaite et délicate à évaluer. En outre, les aspects concurrents et distribués qui sont incontournables dans les applications actuelles
apportent leur lot supplémentaire de difficultés tant conceptuelles que pratiques.

Ce groupe de travail se place à la confluence des trois communautés bases de données, concurrence et méthodes formelles. Nous souhaitons y promouvoir l’utilisation des méthodes formelles pour les langages de
manipulations de données, pour apporter aux applications critiques manipulant des données les garanties de sûreté dont elles ont besoin.
Les premières formalisations [Gon03, MMSW10, CU11, BCD17, AHM+17, CWCS17, BCKM18, BC19] en ce domaine se sont essentiellement intéressées à l’interrogation des données. Dans ce groupe de travail, nous souhaitons plus particulièrement aborder la question de la mise à jour de données (ajout, suppression, modification). Cette question pose les nouveaux défis suivants, en particulier lorsque l’on veut tenir compte des aspects concurrents ou distribués :
— garantir l’intégrité des données, c’est-à-dire assurer que la mise à jour des données préserve un ensemble de propriétés des données et de la base ;
— garantir la sérialisabilité des transactions concurrentes, c’est-à-dire l’interaction cohérente des différentes opérations de mise à jour, fussent-elles simultanées ;
— identifier formellement les conditions permettant un usage des blockchains similaire à une base de données distribuée ;
— formaliser les garanties offertes par les différents systèmes quant à l’intégration de transactions valides ;
— formaliser des transformations pour les bases de données graphe préservant des invariants structurels ;
— certifier des mécanismes de transaction pour les modèles de données graphe ;
— étudier les liens entre les modèles de données semi-structurées et les blockchains.

Ces questions seront étudiées dans un sens très large pour les modèles de données les plus utilisés aujourd’hui : les bases de données relationnelles, les bases de données orientées graphe et les blockchains.
Systèmes de gestion de bases de données relationnelles Les systèmes de bases de données relationnelles sont toujours très utilisés et sont théoriquement fondés sur le modèle relationnel [AHV95]. Ce modèle permet de représenter l’information (au moyen de relations) et d’affiner cette information au moyen de contraintes d’intégrité. Une contrainte d’intégrité est un invariant (une formule de la logique du premier ordre) que les données doivent satisfaire au cours de la vie de l’application modélisée. La littérature identifie plusieurs grandes classes de contraintes : les dépendences fonctionnelles et clés, les dépendences d’inclusion, et enfin les dépendences de jointure et/ou multivaluées.
Les données résidentes dans de tels systèmes sont principalement gérées au moyen du langage de requêtes standard SQL. Ce langage offre de nombreux mécanismes pour définir des contraintes d’intégrités vérifiées statiquement ou dynamiquement.
— typage : contraignant les valeurs admissibles pour un attribut ;
— clés primaires et clés étrangères : indiquant que certaines valeurs sont définies de manières uniques (clé) ou font référence à des valeurs existant dans d’autres parties de la base (dépendences d’inclusion) ;
— triggers : permettant d’exprimer des contraintes générales.
Pour certaines, la vérification se fait statiquement mais généralement, la vérification est dynamique. C’est le mécanisme des triggers qui permet une telle vérification. Ces «triggers» peuvent déclencher dynamiquement
une action en cas de requête violant une propriété donnée : la requête peut être rejetée, ou d’autres requêtes peuvent être exécutées pour rétablir l’intégrité.
Deux niveaux d’erreurs peuvent survenir dans la mise en place d’une politique d’intégrité sur une base relationnelle. D’une part, le langage ne fournit aucun moyen de s’assurer que les contraintes mises en place, qui peuvent être particulièrement complexes dans le cas de l’utilisation de triggers, assurent bien la mise en oeuvre de cette politique d’intégrité. D’autre part, l’implantation du langage SQL choisie peut contenir des
erreurs dans la vérification des contraintes, voire dans la mise à jour des données elle-même.
Notre premier objectif est d’étudier ces deux niveaux. Nous voulons donc fournir un langage de haut niveau pour décrire une politique d’intégrité, et le relier formellement aux mécanismes de contraintes offerts par SQL. Par ailleurs, nous voulons fournir une implantation, certifiée au moyen de l’assistant Coq, de ce types de requêtes et contraintes de SQL.
Pour la mise en oeuvre de cet objectif, la sémantique formelle de SQL établie dans l’assistant de preuves Coq par [BC19] pour des requêtes d’interrogation (select) peut servir de premier socle pour fonder un
langage de spécification d’invariants sur le résultat de ces requêtes. Nous souhaitons :
— développer un tel langage, et l’étendre à la spécification d’invariants sur les données et les bases de données elles-mêmes ;
— donner une sémantique formelle pour les requêtes de mise à jour de SQL (insert, delete et update), ainsi que les outils utilisés pour définir les contraintes d’intégrité, comme les triggers.
Notre objectif à plus long terme est que ces outils soient utilisables par des non experts de Coq, voire des méthodes formelles en général. Un point crucial sera donc de fournir un outil de haut niveau et le plus automatisé possible pour raffiner une politique d’intégrité en une implantation concrète, avec une garantie formelle de cette implantation.

Blockchains
Une blockchain est un registre numérique, décentralisé et immuable qui archive les transactions entre les participants du réseau. Les transactions concernent principalement un type de données purement numérique appelé token, pouvant être une crypto-monnaie, mais elles peuvent également porter des informations, inscrites elles aussi dans le registre. Plus précisément, une transaction blockchain est un transfert de propriété d’une quantité de token d’un compte à un autre sous condition de validité d’une garde. Cette garde est constituée d’une partie implicite propre au respect de certains invariants présidant au fonctionnement de la blockchain, comme l’absence de double dépense, et d’une partie explicite qui doit être évaluée sur chaque noeud par la machine abstraite de la blockchain. Cette garde explicite, appelée smart contract, est spécifique aux comptes impliqués dans la transaction, à la quantité de tokens et aux données étiquetant la transaction. Les applications envisagées pour la blockchain tendent à l’utiliser comme une base de données distribuée dont les points forts sont l’immuabilité et l’infalsifiabilité des enregistrements ainsi que l’absence de tiers de confiance. Or, mise à part Hyperledger Fabric [ABB+] qui ne gère pas de crypto-monnaie et qui fonctionne en réseau fermé avec permission, les blockchains diffèrent des bases de données distribuées par l’absence d’un serveur central comme tiers de confiance, le fait que le réseau soit ouvert et, dans la majorité des cas des blockchains déployées, la cohérence à terme avec convergence probabiliste de la structure de donnée distribuée.
L’inscription d’une transaction au registre met en jeu différents noeuds et se déroule sur plusieurs étapes : la transaction est diffusée sur un réseau pair-à-pair, et son intégration est soumise à la stratégie de fabrication
d’un bloc, qui peut être propre à chaque fabriquant. Un bloc fabriqué est lui-même diffusé en tant que candidat comme nouvelle tête de la chaîne, et les transactions qu’il contient sont considérées comme inscrites au registre
lorsqu’un consensus sur l’inclusion du bloc est atteint dans le réseau. Dans le cas d’un algorithme de consensus classique tolérant aux fautes Byzantines [LSP82] (noté BFT), la blockchain a une cohérence forte et si on
prend en compte les latences due au réseau, on peut aussi parler de convergence à terme [Vog09, Bur14].
Dans ces cas-là, la publication d’une transaction dépend de la validité de sa garde, de la stratégie de sélection du fabriquant de bloc et du vote du quorum dans le consensus. Tendermint [BKM18] ou Red Belly [CGLR17]
implémentent un tel consensus. Dans la majorité des blockchains déployées, l’algorithme de consensus n’est pas un consensus classique mais un consensus organique ou à la Satoshi [Nak09]. Ce type de consensus est organique car il mêle des aspects stratégiques liés aux intérêts des pairs, qui peuvent être vus comme des acteurs, à des aspects algorithmiques
définissant la popularité d’une chaîne. Plus une chaîne est populaire, plus il est probable qu’elle soit la copie locale courante de chaque pair : en générale, les consensus organiques sont des consensus au mieux à cohérence à terme avec convergence probabiliste, a contrario d’une base de données distribuée dont la cohérence est terminale, voire causale [Lam78, SM94], mais déterministe. Une transaction n’est alors pas du tout atomique,
elle peut être publiée sur un noeud et pas sur un autre.
La criticité des usages des blockchains pousse à une formalisation mécanisée de ces structures de données décentralisées. Bien que l’usage des blockchains est envisagé comme celle d’une base de données distribuée, les
consensus organiques ne permettent pas aux blockchains d’avoir les mêmes propriétés. Aussi, une formalisation mécanisée des blockchains basées sur la formalisation des bases de données permettrait de formaliser la distance entre ces deux types objets. Il s’agirait alors de pousser les outils formels exposés plus haut dans un cadre ouvert, décentralisé, à cohérence à terme avec convergence probabiliste. De tels travaux permettraient de poser les bases sémantiques nécessaire au développement d’applications décentralisées ou d’oracles sûrs afin d’avoir des garanties formelles à la hauteur de la criticité des applications envisagées.
Bases de données orientées graphe Les bases de données orientées graphe sont des systèmes nonrelationnels adaptés à la manipulation des données fortement interconnectées. Celles-ci sont représentées et stockées directement comme des graphes, dans lesquels les noeuds dénotent des entités abstraites et les arêtes les reliant dénotent des relations. Les bases de données graphe peuvent représenter aussi d’autres modèles NoSQL, comme le modèle clé-valeur, colonne, ou document, car elles s’appuient sur un formalisme plus riche qui permet d’associer des propriétés aux noeuds et aux relations. Ce modèle de multi-graphe orienté et attribué est aussi appelé le modèle de graphe de propriétés (PGM) et fournit les bases de la plupart des implantations commerciales comme Oracle PGX, Neo4j ou Giraph.
L’avantage principal de ce paradigme est qu’il permet d’exprimer et de traiter de manière efficace des requêtes graphe, comme par exemple celles qui calculent l’atteignabilité à travers des chemins étiquetés. Alors que dans le contexte relationnel ces types de requêtes seraient exprimées avec une itération coûteuse d’opérateurs de jointure, dans le cadre des bases de données graphe il est possible de directement naviguer dans le graphe par des pointeurs physiques. De plus, les bases de données graphe peuvent exprimer un schéma flexible spécifiant les types des noeuds et des arêtes avec leurs propriétés. Cela permet de définir des index qui offrent un accès rapide aux noeuds, soit de manière structurelle, selon des motifs de sous-graphe, soit selon des valeurs spécifiques de leurs propriétés.

Analyse de données
Grâce au fait qu’elles peuvent exprimer des relations complexes de manière
compacte, les bases de données graphe ont trouvé des applications dans l’analyse des données dans une variété de domaines, comme les réseaux sociaux, la bio-informatique, la logistique etc. Une des techniques de
base dans l’analyse exploratoire des données est le clustering, qui permet d’identifier des composants qui ont des propriétés similaires. En général, chaque cluster comprend des noeuds qui sont fortement connectés entre
eux et faiblement connectés au reste du graphe. Pour comprendre la structure générale d’un graphe, il est important non seulement de calculer ces clusters, mais aussi de distinguer entre les rôles de chaque entité.
En particulier, ont peut identifier des noeuds qui connectent des clusters différents comme étant des entités très influentes (des hubs) et les noeuds qui ne sont ni des clusters, ni des hubs, comme étant du bruit (des
outliers). En vue de la topologie du blockchain et de la complexité des rôles et des comportement des différents acteurs qui y participent, une piste de recherche serait d’analyser ces composantes avec des techniques de
clustering, utilisées pour l’analyse des données graphe. Par exemple, ces transformations de graphe pourraient être formellement définies et la préservation des propriétés structurelles, comme l’atteignabilité, pourrait être formellement prouvée. Une telle analyse serait importante pour prendre en compte la sécurité et la scalabilité des blockchains, car elle pourrait permettre d’identifier des potentielles transactions frauduleuses, ainsi que des noeuds qui ne sont plus actifs et qui peuvent être supprimés. Ceci peut servir de base pour visualiser la topologie de l’infrastructure des transactions, pour interroger et en extraire des motifs structurels, ainsi que
pour étudier la provenance des données. Cette analyse nécessiterait la prise en compte des niveaux verticaux d’une blockchain (réseau de communication, la structure de donnée elle-même et le niveau applicatif) et
permettrait d’abstraire cette verticalité dans les formalisations mécanisées. De même, une telle abstraction aiderait à aborder la formalisation mécanisée des interactions entre plusieurs blockchains, le cross-chain, ainsi
qu’à raisonner sur des flots de transactions au travers de blockchains différentes [NK18].

Transactions
Afin d’assurer des garanties fortes, des travaux ont été menés sur l’application des méthodes formelles aux blockchains, notamment sur la modélisation formelle des smart contrats. Cependant, la formalisation des transactions reste à être traitée. Un axe de recherche envisagé est la spécification formelle d’un langage pour les transactions, avec une sémantique formelle et une traduction certifiée vers les transactions
Bitcoin ou Etherium. Il est aussi souhaitable d’établir un lien formel avec les modèles transactionnels implémentés dans les données graphe distribuées, dans lesquelles des critères de sérialisabilité sont imposés pour assurer la consistance éventuelle des données. Outre que les transactions ACID, dans le contexte des bases de donnees graphe, de nombreux systemes implémentent aussi un mécanisme transactionel de type OLTP (Online Transaction Processing) qui permet d’effectuer des requêtes analytiques sur l’ensemble du graphe et qui possent aussi des problèmes de disponibilité opérationnelle. Le traitement formel des transactions dans le cadre semi-structuré d’un modèle à base de graphes peut avoir comme bases des travaux de certifications concernant les graphes dynamiques [BDA18]. En exploitant ainsi le modèle riche de graphes de propriétés et en suivant des travaux récentes [DHES16], on peut ajouter des informations temporelles, c’est-à-dire des estampilles de temps, aux noeuds correspondants à chaque
transaction. Une façon de permettre transactions ACID strictement sérialises, ainsi que les transactions OLTP serait d’implémenter et vérifier un oracle qui permet de raffiner ces estampilles témporelles selon une
chronologie donnée.

Travaux connexes
Dans le domaine des bases de données relationnelles, un effort conséquent a été porté sur l’interrogation des données. Les travaux les plus récents portent sur la décision de l’équivalence de requêtes [CWCS17], la sémantique du langage SQL [BC19], ou encore la compilation [AHM+17] ou l’exécution [BCKM18] de requêtes. Quelques travaux préliminaires portent sur la définition d’un sous-ensemble des contraintes d’intégrité, comme les dépendances fonctionnelles [BCD14]. Concernant les blockchains et leur consensus, des efforts de formalisations mécanisées ont été menés.
Différents algorithmes de consensus classiques ont été formalisés mécaniquement, e.g. Velisarios [RVVEV18], Asphalion [VRV19], Raft [WWA+16]. Dans [GKL15], les auteurs formalisent les différentes qualités de cohérence que l’on peut attendre de BitCoin selon des hypothèses sur la proportion de noeuds byzantins présents dans le réseau. Ils démontrent ainsi que dans le cas général, BitCoin a une cohérence à terme avec convergence probabiliste. Dans [ADPL+19], les auteurs proposent un formalisme générique permettant de déterminer et de classifier les blockchains par rapport à leur cohérence. Comme attendu, celles à cohérence forte implémentent de véritables consensus distribués. Dans [PS18], les auteurs s’intéressent à la formalisation généralisée mécanisée
qui, paramétrée par la fonction de sélection d’une tête de chaîne et la fonction de validation d’un bloc ou d’une transaction, établit qu’elle a une cohérence à terme lorsque le réseau est en clique sans nouvelle tête
en attente. Cependant, les hypothèses de ces travaux ne prennent pas en compte la réalité et ne reflètent pas les véritables propriétés des blockchains à consensus organiques. Des travaux plus récents essaient de
mécaniser les formalisations du protocol Backbone de Bitcoin [GKL15] dans [GS20]. Une thèse est en cours sur la formalisation mécanisée de la blockchain Concordium [DYSTT19].
Dans le domaine de bases de données graphe, des travaux ont été menés sur le développement d’un standard pour les requêtes graphe [AAB+18], ainsi que sur la formalisation Coq d’un moteur certifié pour l’évaluation d’un sous-langage de requêtes navigationnelles linéarisables sur des graphes de propriétés dynamiques [BDA18]. Concernant les modèles de données graphes, une formalisation Coq de GraphQL à été fourni dans [DOT20] ; la sérialisation des graphes de propriétés a été étudié dans [TAS+19] et l’interopérabilité entre ce modèle et le modèle RDF à été étudié dans [ATT19].
L’ensemble des travaux du groupe de travail vont nécessiter la formalisation de modélisation de contraintes en toute généralité. Dans ce cadre, de nombreux travaux ont concerné la traduction de diagrammes UML vers un formalisme logique pour ensuite vérifier formellement certaines propriétés. En particulier Laleau et Mammar ont développé un ensemble de travaux assez complet qui vise les bases de données [ML06] : un diagramme UML est traduit en une spécification B qui peut être non seulement utilisée pour vérifier des contraintes d’intégrité mais aussi dériver des implantations de confiance (JAVA/SQL) obtenues en utilisant
le raffinement de B.

Retombées, organisation et consortium
L’objectif de ce groupe de travail est d’opérer un rapprochement fructueux entre les diverses communautés présentées ci-dessus. Cela permettra une meilleure compréhension des enjeux autour des transactions dans les
bases de données au sens large, à travers leur formalisation. Un intérêt particulier sera porté à la formalisation d’un socle commun pour les divers objectifs visés. Le groupe de travail s’organisera autour d’exposés scientifiques (ouverts à un public large) d’orateurs du groupe de travail et externes, avec une fréquence de 4 séminaires par an. Les orateurs extérieurs envisagés sont les suivants :
— Louis Mandel, Avraham Shinnar (IBM, États-Unis) et Jérôme Siméon (Clause.io, États-Unis), pour leurs travaux autour de la formalisation d’une chaîne de compilation optimisante pour les bases de données, ainsi que la formalisation de smart contracts dans le cas de Jérôme Siméon ;
— Pierre Courtieu (CNAM), pour ses travaux autour de la formalisation en Coq d’algorithmes distribués ;
— Ilya Sergey (Yale-NUS College, actuellement à l’université de Singapour), pour ses travaux de formalisations mécanisées de la blockchain, et son implication dans le projet CertiChain ;
— Bas Spitters (Aarhus University), pour ses travaux de formalisations mécanisées autour des smart contracts et des blockchains et son implication dans le projet Concordium.
Le groupe de travail servira de support à des financements de doctorants et de post-doctorants communs à deux, voire trois des thématiques proposées.
Le consortium reflète la diversité des communautés présentées. Véronique Benzaken, Évelyne Contejean, Stefania Dumbrava et Chantal Keller sont des expertes en formalisation autour des bases de données relationnelles.
Stefania Dumbrava est également une experte en bases de données orientées graphe. Zaynah Dargaye, Germán Delbianco et Julien Tesson sont des experts en formalisation autour des blockchains en particulier en
formalisation mécanisée des théories des langages, langages concurrents et structures de données distribuées. Catherine Dubois et Julien Forest ont une forte expertise en formalisation et en automatisation. Thibaut Balabonski est expert en théorie de la concurrence et sa formalisation.
Bien qu’extérieure à DigiCosme, l’entreprise Nomadic Labs apporte une expertise en formalisation des blockchains centrale au groupe de travail.