dim. Jan 2nd, 2022
    Free TON

    En avril, la sous-gouvernance des méthodes formelles (Formal Methods SubGovernance) a été créée pour rendre Free TON plus sûr et plus fiable. Pour plus de détails — qu’est-ce que la vérification formelle et comment elle est appliquée dans Free TON – nous nous sommes tournés vers l’un des initiateurs de la création de la sous-gouvernance — Sergey Egorov (qui est également cofondateur et l’un des dirigeants de Pruvendo).

    • Veuillez nous parler de votre parcours et comment tout a commencé.

    J’ai travaillé pendant assez longtemps en tant que responsable des services de test dans des entreprises comme Oracle, et je connais bien le domaine du contrôle qualité. Puis je me suis lassé de tout, et j’ai commencé à faire des affaires avec mon partenaire Andrey Lyashin (l’un des auteurs du concept du système binaire NOT a TON — ndlr.). Nous avons commencé avec des conseils de haute technologie et nous avons souvent changé de direction, mais à la fin nous sommes retournés à notre “port d’attache”. Je suis devenu Chief Software Officer d’une société d’externalisation traditionnelle, mais je voulais quelque chose de différent.

    Et il y a huit ans, Andrey a appris la vérification formelle. Il y avait un sentiment qu’il y avait un avenir derrière cela, une entreprise, quelque chose de grand et d’intéressant, mais nous ne comprenions pas quoi exactement. Nous avons essayé différentes options, venues de différents côtés et, par conséquent, l’idée est venue que cela pourrait être intéressant pour un contrat intelligent. En effet, à un moment donné, nous avons été présentés aux gars de Free TON, qui partagent le même avis.

    • Depuis combien de temps avez-vous eu l’idée de créer un système de sous-gouvernance de vérification formelle dans Free TON?

    Il y a quelques mois, lorsque nous avons commencé à lancer le premier concours, nous avons été confrontés au fait que, malheureusement, dans la gouvernance principale, de nombreuses personnes n’avaient pas les compétences pour évaluer objectivement ce qui se passait. Et juste à ce moment-là, l’idée est venue d’unir les experts dans ce domaine dans une SubGovernance distincte, afin que le groupe puisse s’engager délibérément à attirer de nouvelles équipes, à développer le niveau d’expertise, à partager l’expérience, etc.

    • Qu’est-ce que la vérification formelle?

    Il existe un complexe quality assurance — c.-à-d. qu’il ne s’agit pas seulement de tests avancés, mais aussi d’un vaste ensemble de mesures, allant de la bonne architecture intégrée dans le produit logiciel à une surveillance post-produit intensive. Ces tests logiciels visent à rendre le produit raisonnablement fiable. Et dans 99% des cas, pour une utilisation pratique, cela vous suffira.

    Si vous prenez un produit fabriqué par une entreprise décente, alors, très probablement, cela fonctionnera, même si de temps en temps vous rencontrez de petits problèmes — quelque chose est coincé, n’a pas si bien fonctionné… Cela vous attristera, mais pas très fort… Vous ne subirez aucune perte à cause de cela, à cause de laquelle vous arrêtiez d’utiliser le produit. Par conséquent, ce niveau de qualité est juste suffisant.

    Mais il y a des domaines où un autre niveau de qualité est nécessaire: la super-fiabilité. En fait, il n’y en a pas beaucoup. Ce sont, tout d’abord, la médecine (il est clair que si certains appareils chirurgicaux commencent à se comporter de manière incorrecte, tout peut mal se terminer), toutes sortes de transports (aérospatiale), les applications militaires et la finance.Contrairement aux domaines que j’ai mentionnés en premier, la finance est un domaine relativement simple et peu accessible. Si vous développez du matériel médical, vous devez obtenir des certificats, des licences, etc., et la finance est la partie active la plus simple. De plus, une bonne technologie telle que FinTech est apparue — une famille de divers services intéressants développés et lancés par de petits fournisseurs. Mais la question de la fiabilité reste assez aiguë pour les services de ce type.

    La blockchain est ouverte sur le monde entier, contrairement par exemple aux banques, qui se trouvent derrière sept pare-feu avec des services de sécurité de l’information développés, etc. Ici, l’entreprise est ouverte à tous les vents, il est donc facile de devenir victime de pirates informatiques: les fonds peuvent geler en raison d’un contrat intelligent rédigé de manière illettrée et de nombreux problèmes peuvent survenir.

    C’est pour cela, un domaine tel que FinTech pour la détermination de la qualité fait des déclarations spéciales qui, en principe, ne peuvent pas être obtenues par des tests avancés. Et ici, les méthodes de vérification formelle viennent à la rescousse.

    Vous souvenez- vous du théorème de Pythagore? Vous avez dessiné un triangle rectangle, mesuré les côtés, l’hypoténuse et la somme des carrés des deux autres côtés a coïncidé avec le carré de l’hypoténuse. Oh, pensiez-vous, cela s’est avéré intéressant, ou peut-être y a-t-il une sorte de loi? Nous avons dessiné un tel deuxième, troisième, quinzième triangle et à chaque fois vous vous assurez que la somme des carrés des deux autres côtés est égale au carré de l’hypoténuse.

    Autrement dit, vous pouvez dire que cela peut toujours être? Très probablement oui, et c’est à peu près le test. Vous avez effectué 15 tests et montré que cette règle est vraie. Si nous prouvons le théorème de Pythagore, alors nous disons que c’est tout, la question est close — il en sera toujours ainsi. Voilà ce qu’est la méthode formelle.

    • C’est là que réside la magie. Parce que la façon dont cela s’applique aux logiciels est totalement incompréhensible.

    Pour une personne non éclairée, cela peut sembler assez difficile à comprendre – comment les méthodes formelles peuvent-elles être liées aux logiciels, car les mathématiques sont des mathématiques et, par exemple, la blockchain est complètement différente.

    Un programme est essentiellement une description d’un système qui doit avoir certaines propriétés. Supposons que vous ayez, par exemple, un système de tokens TIP-3 et que vous devez vous assurer que, pour toute opération, l’équilibre des jetons est maintenu — c’est une certaine propriété du système. Si cette description du programme satisfait ces règles, vous pouvez prouver que certaines propriétés seront remplies ou non.

    Dans un sens, la magie est bien sûr présente ici. Autrement dit, ce n’est pas une programmation ordinaire, ni des tests tout à fait ordinaires, ni des mathématiques tout à fait ordinaires. C’est ce qui se trouve à la jonction de ces disciplines.

    • Dans le document sur la création de la sous-gouvernance des méthodes formelles dans la première étape, des activités intéressantes liées à la conversation avec les développeurs sont indiquées. Vous déterminez à quoi ressemble le système qu’ils développent, puis construisez un modèle et essayez d’y trouver des vulnérabilités. C’est bien ça?

    En gros, oui. En fait, le principal problème aujourd’hui est d’obtenir une spécification formelle. Pas le seul, mais probablement le principal. Autrement dit, à un niveau simple, nous disons que nous prouvons que le programme fonctionne correctement. Qu’est-ce qui est “juste”? “Juste” signifie qu’il sera conforme à certaines spécifications, mais cette spécification, à son tour, peut être erronée et peut ne pas correspondre à la logique métier souhaitée.

    Si la spécification indique que le solde du compte peut être négatif, alors désolé… Par conséquent, la question de la validation de la spécification formelle est très large et nous la prenons très au sérieux. Et c’est l’un des domaines que nous essayons actuellement de développer activement. C’est ce qui empêche de nombreux développeurs d’utiliser de telles méthodes dans leur travail dans une plus grande mesure — il n’y a pas d’outils normaux, simples et compréhensibles pour définir la spécification et son contrôle.

    Nous prévoyons de faire ces choses très activement dans un proche avenir. Et maintenant, pour créer une spécification normale, nous devons absolument obtenir le maximum d’informations des développeurs sur ce qu’ils voulaient vraiment. Cela n’est souvent pas évident.

    • Pouvons-nous dire que pour chaque produit spécifique, vous devez développer son propre modèle?

    Non, vous n’avez pas besoin de créer complètement son propre modèle. Il est nécessaire de développer une spécification, et la méthode est la même pour tous – une méthode de traduction d’un produit logiciel en un code dans un tel pseudo-langage dans lequel une vérification formelle est effectuée, et dans un sens, nous pouvons dire que oui, c’est son propre modèle pour chaque contrat.

    Il existe plusieurs langages pour la vérification formelle, mais en particulier nous aimons programmer en Coq.

    Mais il est clair qu’il existe un très grand nombre de moments et de technologies reproductibles. Nous ne venons pas à chaque fois comme dans un nouveau monde, à chaque fois c’est plus facile et meilleur. Mais oui, d’une certaine manière, nous devons construire un certain ensemble d’énoncés, un écosystème autour de chaque contrat spécifique.

    • Le système de vérification formelle garantit tout d’abord l’absence d’erreurs dans la conception du système et précisément dans la logique du programme. Mais offre-t-il une garantie contre les erreurs si la vulnérabilité existe dans les outils logiciels eux-mêmes?

    En fonctionnement normal, nous supposons que le nœud fonctionne correctement. Mais dans les plans à moyen terme, nous prévoyons toujours de procéder à une vérification formelle du compilateur et du nœud, de la machine virtuelle et de l’ensemble de la pile technique.

    Dans quelle mesure et quand ces travaux seront réalisés est encore une grande question. Mais j’aimerais le faire, car cela augmentera considérablement la confiance de la communauté. Les gens comprendront que cela fonctionne vraiment comme il se doit et que leurs fonds ne s’envoleront pas à cause d’une erreur stupide.

    • Quel sera le principal objectif du travail dans la sous-gouvernance des méthodes formelles?

    Pour le moment, le travail a été fait avec les contrats intelligents Multisig et DePool, smart contracts nécessaires. En conséquence, SMV en tant que système de vote, TIP-3 et un nouvel “électeur” est ce dont nous avons besoin en premier lieu pour lancer un nouveau nœud. De plus, je pense qu’il y aura du travail sur DeFi, car l’échange DeFi est quelque chose qui est nécessaire de toute urgence pour attirer des fonds vers l’écosystème. Ce qui se passera ensuite est toujours en discussion.

    • La sous-gouvernance des méthodes formelles comprend également des collaborateurs d’Origin Labs, ils sont également spécialisés dans la vérification formelle, les avez-vous rencontrés auparavant dans d’autres projets?

    Nous en avons entendu parler, bien que nous ne les ayons jamais rencontrés dans certains projets auparavant. Ils sont assez qualifiés, bien qu’ils utilisent un système légèrement différent d’utilisation de méthodes formelles. Nous serons heureux de travailler ensemble et d’échanger des expériences.

    10
    0