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.

Un generador de pruebas de contratos inteligentes basado en la técnica de árbol de ramificación (Branching Tree Technique).

Runtime Verification ha estado a la vanguardia de las herramientas de verificación formal de código abierto durante más de una década. Nuestro enfoque generalista nos permite utilizar nuestra tecnología en múltiples cadenas de bloques. Si bien KEVM ofrece nuestra infraestructura de verificación a todos los contratos inteligentes basados en la EVM, Kontrol reduce en gran medida la barrera de entrada a la verificación formal para los contratos inteligentes de Solidity. Nuestras herramientas son completamente de código abierto y de libre acceso para todos los desarrolladores del ecosistema Optimism sin costo adicional. KEVM es una semántica formal ejecutable de la EVM escrita en el marco K. KEVM pasa todas las pruebas de conformidad de Ethereum y es el punto de entrada para verificar formalmente los contratos inteligentes con el marco K. Sin embargo, el uso de KEVM simple requiere capacitación ad-hoc en el marco K para escribir especificaciones. Además, estas especificaciones pueden ser bastante detalladas, lo que aumenta la dificultad de escribirlas. Kontrol resuelve esto permitiendo a los desarrolladores escribir la especificación formal de sus contratos inteligentes directamente como pruebas de propiedad de Foundry. Estas pruebas se traducen automáticamente en especificaciones KEVM, manteniendo todas las garantías de verificación y permitiendo una experiencia de desarrollador mucho más fácil.