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.

Um gerador de testes de contratos inteligentes baseado na Técnica de Árvore de Ramificação (Branching Tree Technique).

A Runtime Verification tem estado na vanguarda das ferramentas de verificação formal de código aberto por mais de uma década. Nossa abordagem generalista nos permite usar nossa tecnologia em várias blockchains. Enquanto o KEVM oferece nossa infraestrutura de verificação para todos os contratos inteligentes baseados em EVM, o Kontrol reduz muito a barreira de entrada para a verificação formal de contratos inteligentes em Solidity. Nossas ferramentas são totalmente de código aberto e de livre acesso a todos os desenvolvedores do ecossistema Optimism sem custo adicional. O KEVM é uma semântica formal executável da EVM escrita no K framework. O KEVM passa em todos os testes de conformidade do Ethereum e é o ponto de entrada para verificar formalmente contratos inteligentes com o K framework. No entanto, usar o KEVM puro requer treinamento ad-hoc no K framework para escrever especificações. Além disso, essas especificações podem ser bastante verbosas, aumentando a dificuldade de escrevê-las. O Kontrol resolve isso permitindo que os desenvolvedores escrevam a especificação formal de seus contratos inteligentes diretamente como testes de propriedade do Foundry. Esses testes são traduzidos automaticamente em especificações KEVM, mantendo todas as garantias de verificação e permitindo uma experiência de desenvolvedor muito mais fácil.