Sécurité, tests et vérification formelle

Nous sommes Runtime Verification, une entreprise de recherche et développement qui conçoit des outils rigoureux pour garantir la sécurité et l'exactitude des systèmes critiques. Notre équipe a développé KEVM, la sémantique formelle la plus complète et la plus éprouvée de la machine virtuelle Ethereum (EVM), écrite dans le K Framework. KEVM n'est pas seulement une spécification, c'est une spécification exécutable qui peut être utilisée pour raisonner symboliquement sur les contrats intelligents, exécuter des tests de conformité, analyser l'utilisation du gaz, déboguer des programmes et vérifier formellement les propriétés d'exactitude. Il passe l'intégralité de la suite de tests Ethereum et est utilisé pour vérifier des contrats de grande valeur, y compris les jetons ERC-20 en Solidity et Vyper. Nous avons récemment mis à jour la sémantique pour prendre en charge la mise à niveau Pectra. KEVM est activement utilisé par Kontrol - notre outil de vérification formelle pour Solidity, qui est activement utilisé par les principales équipes de l'écosystème EVM, y compris Optimism, la Fondation Ethereum, Lido, Uniswap, ainsi que par des chercheurs en sécurité et des auditeurs de la communauté Ethereum au sens large. Nous maintenons activement ce dépôt, contribuons à l'évolution du protocole d'Ethereum et nous intégrons aux outils de développement comme Foundry. Grâce à KEVM, nous repoussons les limites de ce qui est possible en matière d'infrastructure de contrats intelligents dont l'exactitude et la sécurité sont prouvables.

Act est un langage de spécification de contrats intelligents et une boîte à outils pour la vérification formelle. Les spécifications Act sont une description formelle de haut niveau de tous les comportements possibles d'un programme EVM. Act permet d'exploiter de nombreux outils de vérification à usage général existants pour prouver les propriétés de la spécification. Ces outils incluent des solveurs SMT (cvc5, z3, bitwuzla), des démonstrateurs de théorèmes (Coq) et des outils d'analyse économique (CheckMate, Open Games). Les spécifications Act peuvent être automatiquement prouvées équivalentes à des implémentations concrètes dans l'EVM. Pour les contrats très simples, les spécifications Act peuvent être générées automatiquement à partir du bytecode EVM. Il s'agit d'un pipeline de bout en bout qui prend en charge un raisonnement fondé sur des principes concernant les propriétés de haut niveau du bytecode EVM. Il prend en charge le raisonnement sur l'exactitude (par exemple, les invariants comptables) et les propriétés économiques (par exemple, la compatibilité des incitations). Les spécifications Act servent de représentation de contrat intelligent de haut niveau, permettant une intégration facile des outils d'analyse et de vérification à usage général existants dans le contexte de l'EVM.

Titanoboa est un interpréteur et un framework de test Vyper qui offre une expérience de développement moderne et intégrée pour les contrats intelligents Vyper. Il permet aux développeurs de tester et de déboguer des contrats Vyper directement dans Python, offrant des fonctionnalités telles que de jolies traces d'exécution (tracebacks), le forking, des capacités de débogage, l'intégration de pytest et le fuzzing prêt à l'emploi. Au-delà de ses capacités autonomes, Titanoboa sert de base à d'autres frameworks de test populaires comme Ape et Moccasin, et constitue un élément central de l'infrastructure de l'écosystème Vyper.