Noobing Security Research: “Formal Verification, часть 2 .conf файл Конфигурационный файл и этим в…”

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