Безопасность, тестирование и формальная верификация

Мы — Runtime Verification, научно-исследовательская компания, создающая строгие инструменты для обеспечения безопасности и корректности критически важных систем. Наша команда разработала KEVM, наиболее полную и проверенную в боях формальную семантику виртуальной машины Ethereum (EVM), написанную на K Framework. KEVM — это не просто спецификация, это исполняемая спецификация, которую можно использовать для символьного рассуждения о смарт-контрактах, запуска тестов на соответствие, анализа использования газа, отладки программ и формальной проверки свойств корректности. Она проходит полный набор тестов Ethereum и используется для проверки ценных контрактах, включая токены ERC-20 как на Solidity, так и на Vyper. Недавно мы обновили семантику для поддержки обновления Pectra. KEVM активно используется Kontrol — нашим инструментом формальной верификации для Solidity, который активно применяется ведущими командами в экосистеме EVM, включая Optimism, Ethereum Foundation, Lido, Uniswap, а также исследователями безопасности и аудиторами в более широком сообществе Ethereum. Мы активно поддерживаем этот репозиторий, вносим вклад в эволюцию протокола Ethereum и интегрируемся с инструментами разработчиков, такими как Foundry. С помощью KEVM мы расширяем границы возможного в доказуемо корректной и безопасной инфраструктуре смарт-контрактов.

Act — это язык спецификации смарт-контрактов и набор инструментов для формальной верификации. Спецификации Act представляют собой формальное высокоуровневое описание всех возможных вариантов поведения программы EVM. Act позволяет использовать множество существующих инструментов верификации общего назначения для доказательства свойств спецификации. К таким инструментам относятся SMT-решатели (cvc5, z3, bitwuzla), средства доказательства теорем (Coq) и инструменты экономического анализа (CheckMate, Open Games). Спецификации Act могут быть автоматически доказаны как эквивалентные конкретным реализациям в EVM. Для очень простых контрактов спецификации Act могут быть автоматически сгенерированы из байт-кода EVM. Это сквозной конвейер, который поддерживает принципиальное рассуждение о высокоуровневых свойствах байт-кода EVM. Он поддерживает рассуждения как о корректности (например, учетные инварианты), так и об экономических свойствах (например, совместимость стимулов). Спецификации Act служат высокоуровневым представлением смарт-контракта, позволяя легко интегрировать существующие инструменты анализа и верификации общего назначения в контекст EVM.

Titanoboa — это интерпретатор и фреймворк для тестирования Vyper, который обеспечивает современный интегрированный опыт разработки смарт-контрактов на Vyper. Он позволяет разработчикам тестировать и отлаживать контракты Vyper непосредственно в Python, предлагая такие функции, как красивые трассировки (tracebacks), форкинг, возможности отладки, интеграцию с pytest и фаззинг «из коробки». Помимо своих автономных возможностей, Titanoboa служит основой для других популярных фреймворков тестирования, таких как Ape и Moccasin, и является ключевой частью инфраструктуры для экосистемы Vyper.