Segurança, testes e verificação formal

Somos a Runtime Verification, uma empresa de pesquisa e desenvolvimento que constrói ferramentas rigorosas para garantir a segurança e a correção de sistemas críticos. Nossa equipe desenvolveu o KEVM, a semântica formal mais completa e testada em batalha da Ethereum Virtual Machine (EVM), escrita no K Framework. O KEVM não é apenas uma especificação, é uma especificação executável que pode ser usada para raciocinar simbolicamente sobre contratos inteligentes, executar testes de conformidade, analisar o uso de gás, depurar programas e verificar formalmente as propriedades de correção. Ele passa em todo o conjunto de testes do Ethereum e é usado para verificar contratos de alto valor, incluindo tokens ERC-20 em Solidity e Vyper. Atualizamos recentemente a semântica para suportar a atualização Pectra. O KEVM está sendo ativamente utilizado pelo Kontrol - nossa ferramenta de verificação formal para Solidity, que é ativamente usada pelas principais equipes no ecossistema EVM, incluindo Optimism, Ethereum Foundation, Lido, Uniswap, bem como pesquisadores de segurança e auditores em toda a comunidade Ethereum em geral. Mantemos ativamente este repositório, contribuímos para a evolução do protocolo do Ethereum e integramos com ferramentas de desenvolvedor como o Foundry. Por meio do KEVM, estamos expandindo os limites do que é possível em infraestrutura de contratos inteligentes comprovadamente correta e segura.

Act é uma linguagem de especificação de contratos inteligentes e um conjunto de ferramentas para verificação formal. As especificações do Act são uma descrição formal e de alto nível de todos os comportamentos possíveis de um programa EVM. O Act permite que muitas ferramentas de verificação de uso geral existentes sejam aproveitadas para provar propriedades sobre a especificação. Tais ferramentas incluem solucionadores SMT (cvc5, z3, bitwuzla), provadores de teoremas (Coq) e ferramentas de análise econômica (CheckMate, Open Games). As especificações do Act podem ser automaticamente provadas como equivalentes a implementações concretas na EVM. Para contratos muito simples, as especificações do Act podem ser geradas automaticamente a partir do bytecode da EVM. Este é um pipeline de ponta a ponta que suporta o raciocínio fundamentado sobre propriedades de alto nível do bytecode da EVM. Ele suporta o raciocínio tanto sobre a correção (por exemplo, invariantes contábeis) quanto sobre propriedades econômicas (por exemplo, compatibilidade de incentivos). As especificações do Act servem como uma representação de contrato inteligente de alto nível, permitindo a fácil integração de ferramentas de análise e verificação de uso geral existentes no contexto da EVM.

O Titanoboa é um interpretador e framework de testes para Vyper que fornece uma experiência de desenvolvimento moderna e integrada para contratos inteligentes em Vyper. Ele permite que os desenvolvedores testem e depurem contratos Vyper diretamente no Python, oferecendo recursos como rastreamentos (tracebacks) aprimorados, forking, recursos de depuração, integração com pytest e fuzzing pronto para uso. Além de seus recursos independentes, o Titanoboa serve como base para outros frameworks de teste populares, como Ape e Moccasin, e é uma peça central da infraestrutura para o ecossistema Vyper.