Input Output демонстрирует Blaster для верификации смартконтрактов Cardano

Cardano Community опубликовало презентацию Blaster, автоматизированного инструмента верификации, предназначенного для проверки того, соблюдают ли смартконтракты Cardano заданные правила. Инженеры Input Output Romain Soulat и Jean-Frédéric Etienne демонстрируют, как инструмент исследует эти свойства и может выдать контрпример при обнаружении нарушения. Они также обсуждают текущую работу над реконструкцией доказательств и способы упростить проверку результатов.

Определение того, что должен делать контракт Cardano

Смартконтракты задают условия для транзакций в блокчейне и определяют, как приложения управляют активами. Разработчик может указать, например, что только авторизованный пользователь может разблокировать средства, находящиеся под управлением контракта. Формальная верификация использует математические методы для проверки того, удовлетворяет ли система свойствам, описанным в спецификации. Тогда как обычное тестирование рассматривает выбранные случаи, формальная верификация стремится установить, выполняется ли заявленное свойство во всех случаях, охватываемых моделью.

Soulat, технический руководитель Cardano High Assurance, пояснил, что Blaster предназначен для автоматизации значительной части доказательной работы. Разработчикам все же нужно задать поведение, которое они хотят проверить, и предоставить соответствующую спецификацию. Когда инструмент находит нарушение, он может выдать контрпример для анализа. Soulat описал транзакцию или последовательность транзакций, которые могут показать, как некто, не являющийся авторизованным пользователем, разблокирует выход.

Как Blaster проверяет свойства контрактов

Blaster использует Lean 4, систему для выражения математических утверждений и работы с доказательствами, вместе с автоматическим решателем. Сначала он упрощает задачу, если свойство не разрешается на этом этапе, оставшаяся задача может быть передана решателю. Чтобы сделать проверки релевантными для Cardano, команда формализовала части окружения, в котором выполняются контракты, включая исполнение скриптов и правила транзакций.

Etienne, ведущий инженер по формальным методам, обозначил три возможных результата, свойство может быть признано корректным, опровергнутым или неопределенным. Контрпример, связанный с опровергнутым результатом, может помочь разработчикам выявить ошибку контракта, отсутствующее предположение или ошибку в спецификации. Неопределенный результат означает, что решатель не установил, выполняется ли свойство. Объем проверки зависит от того, какие свойства разработчики выбирают выразить.

[NEWSBREAK]

Реконструкция доказательств находится в разработке

Разработчики могут компилировать контракты, написанные на таких языках, как Plinth, Aiken или Plutarch, в Untyped Plutus Core, представление, используемое для выполнения скриптов Cardano. Затем они могут импортировать скомпилированный код в Lean 4 и задать свойства для проверки. Ранее Input Output выпустила две библиотеки с открытым исходным кодом, которые предоставляют специфичные для Cardano модели для этого процесса. В более ранней демонстрации команда использовала этот конвейер на учебном контракте из задачи по безопасности, сгенерировав контекст транзакции, который показал, как контракт может быть эксплуатирован.

Etienne пояснил, что реконструкция доказательств все еще находится в разработке. Цель состоит в том, чтобы позволить Lean самостоятельно проверять доказательства, поддерживающие корректный результат, текущая версия инструмента пока не создает реконструированное доказательство Lean, когда решатель возвращает такой результат. Soulat также обозначил планы по более наглядному представлению контрпримеров, что позволит разработчикам изучать детали транзакций, лежащие в основе несостоявшегося свойства.