Интересный пост в Сиолошной (https://t.me/seeallochnaya/3167), про то как AI модели могут находить и эксплуатировать уязвимости в смарт-контрактах уже сейчас оригинал статьи (https://red.anthropic.com/2025/smart-contracts/) на английском от Антропик В статье указаны две уязвимости в коде: - в первом случае в контракте все пользователи имели доступ к функции калькулятора, меняющей storage переменные и модель смогла провести inflation attack, про которые я писал (https://t.me/web3securityresearch/39) - во втором случае в контракте, выпускающем токены в один клик, можно было задеплоить токен без указания адреса для приема комиссий. Зато его можно было добавить позже Круто, что атакующие скрипты в исходной статье тоже показаны https://t.me/web3securityresearch
- 0 replies
- 0 recasts
- 2 reactions
Formal Verification, часть 2 .conf файл Конфигурационный файл и этим все сказано. Хранит в себе пути к исследуемым контрактам, к файлу спецификации, содержит настройки прувера Имеет расширение .conf, пишется как JSON Типичный файл выглядит так { "files": [ "./src/OurContract.sol:OurContract", "./src/AnotherContract.sol:AnotherContract" ], "verify": "OurContract:certora/spec/OurContractInvariant.spec", "wait_for_results": "all", "rule_sanity": "basic", "optimistic_loop": true, "msg":"Verification of OurContractInvariant" } После разделов files и verify находятся настройки анализа, альтернативно их можно писать в CLI при вызове команды certoraRun, которая запускает верификацию То есть можно было бы написать certoraRun ./certora/conf/OurContract.conf --verify OurContract:certora/spec/OurContractInvariant.spec --wait_for_results all --rule_sanity basic --optimistic_loop true --msg Verification of OurContractInvariant Кроме прочего таким образом могут быть заданы настройки самого прувера После запуска команды certoraRun компилируются контракты, затем проверяется корректность локально, если все ок, то задача уходит в работу на сервер, когда будет готово - вам пришлют ссылку на отчет Потому что Certora работает по freemium модели и вам доступны 2000 минут работы сервиса в месяц https://t.me/web3securityresearch
- 0 replies
- 0 recasts
- 5 reactions
Про Formal Verification, часть 1 Упоминал про этот метод анализа кода здесь (https://t.me/web3securityresearch/48) Рассказывать буду на примере Certora (https://www.certora.com/), так как сам пользуюсь их сервисом. Это будет серией постов неопределенной длины, поскольку нюансов работы множество. Формальная верификация - это метод, при котором корректность кода подтверждается математически. Идея в том, что доказывается соответствие анализируемой кодовой базы заявленным свойствам. Именно соответствие свойствам и является уникальной чертой формальной верификации, так как остальное тестирование по сути проверяет только работу системы в частных случаях, что не дает полной картины даже если этих частных случаев десятки тысяч. Certora (произносится как «сертора») как система состоит из двух частей: - Certora Verification Language - Certora Prover Certora Verification Language (https://docs.certora.com/en/latest/docs/cvl/index.html)- CVL Это специальный язык, который используется для написания спецификаций для смарт контрактов Certora Prover Прувер (в переводе с англ. проверяющий/доказывающий) основывается на общеизвестных техниках формальной верификации. По сути это широкое понятие, которое включает в себя несколько частей, включающее в себя компилятор, декомпилятор, статический анализатор и прочее, подробно его устройство разбирается вот здесь (https://docs.certora.com/en/latest/_downloads/7ef350bb9818a0b10467fa47e9e22877/09-pipeline.pdf), на 57 слайдах В спецификациях определяются правила анализируемого контракта, которые несут в себе некоторые предположения о его поведении. Эти правила компилируются в логические формулы, которые называются verification condition. Обычно их создается некоторое множество, которое затем отправляется на анализ в SMT Solver (https://docs.certora.com/en/latest/docs/user-guide/glossary.html#term-SMT-solver) SMT Solver - Satisfiability Modulo Theories Solver. Проверяет могут ли быть удовлетворены условия выражения Для написания теста формальной верификации по стандарту создается в корне проекта папка certora с двумя подпасками: conf и spec и в них соответственно два файла с расширениями .spec и .conf На этом сегодня закончу, хороших выходных! https://t.me/web3securityresearch
- 0 replies
- 0 recasts
- 6 reactions