Seguridad, pruebas y verificación formal

Somos Runtime Verification, una empresa de investigación y desarrollo que crea herramientas rigurosas para garantizar la seguridad y corrección de sistemas críticos. Nuestro equipo ha desarrollado KEVM, la semántica formal más completa y probada en batalla de la Máquina Virtual de Ethereum (EVM), escrita en el K Framework. KEVM no es solo una especificación, es una especificación ejecutable que se puede utilizar para razonar simbólicamente sobre contratos inteligentes, ejecutar pruebas de conformidad, analizar el uso de gas, depurar programas y verificar formalmente las propiedades de corrección. Pasa el conjunto completo de pruebas de Ethereum y se utiliza para verificar contratos de alto valor, incluidos los tokens ERC-20 tanto en Solidity como en Vyper. Recientemente actualizamos la semántica para admitir la actualización Pectra. KEVM está siendo utilizado activamente por Kontrol, nuestra herramienta de verificación formal para Solidity, que es utilizada activamente por los principales equipos en el ecosistema EVM, incluidos Optimism, la Fundación Ethereum, Lido, Uniswap, así como investigadores de seguridad y auditores en toda la comunidad de Ethereum en general. Mantenemos activamente este repositorio, contribuimos a la evolución del protocolo de Ethereum y nos integramos con herramientas para desarrolladores como Foundry. A través de KEVM, estamos ampliando los límites de lo que es posible en una infraestructura de contratos inteligentes demostrablemente correcta y segura.

Act es un lenguaje de especificación de contratos inteligentes y un conjunto de herramientas para la verificación formal. Las especificaciones de Act son una descripción formal de alto nivel de todos los comportamientos posibles de un programa de la EVM. Act permite aprovechar muchas herramientas de verificación de propósito general existentes para probar propiedades sobre la especificación. Dichas herramientas incluyen solucionadores SMT (cvc5, z3, bitwuzla), demostradores de teoremas (Coq) y herramientas de análisis económico (CheckMate, Open Games). Las especificaciones de Act pueden demostrarse automáticamente como equivalentes a implementaciones concretas en la EVM. Para contratos muy simples, las especificaciones de Act pueden generarse automáticamente a partir del bytecode de la EVM. Este es un flujo de trabajo integral que respalda el razonamiento fundamentado sobre las propiedades de alto nivel del bytecode de la EVM. Admite el razonamiento tanto sobre la corrección (por ejemplo, invariantes contables) como sobre las propiedades económicas (por ejemplo, compatibilidad de incentivos). Las especificaciones de Act sirven como una representación de contratos inteligentes de alto nivel, lo que permite una fácil integración de las herramientas de análisis y verificación de propósito general existentes en el contexto de la EVM.

Titanoboa es un intérprete y marco de pruebas de Vyper que proporciona una experiencia de desarrollo moderna e integrada para contratos inteligentes de Vyper. Permite a los desarrolladores probar y depurar contratos de Vyper directamente dentro de Python, ofreciendo características como rastreos bonitos, bifurcación, capacidades de depuración, integración de pytest y fuzzing listo para usar. Más allá de sus capacidades independientes, Titanoboa sirve como base para otros marcos de prueba populares como Ape y Moccasin, y es una pieza central de infraestructura para el ecosistema de Vyper.