Упоминал про этот метод анализа кода здесь
Рассказывать буду на примере Certora, так как сам пользуюсь их сервисом. Это будет серией постов неопределенной длины, поскольку нюансов работы множество.
Формальная верификация - это метод, при котором корректность кода подтверждается математически. Идея в том, что доказывается соответствие анализируемой кодовой базы заявленным свойствам.
Именно соответствие свойствам и является уникальной чертой формальной верификации, так как остальное тестирование по сути проверяет только работу системы в частных случаях, что не дает полной картины даже если этих частных случаев десятки тысяч.
Certora (произносится как «сертора») как система состоит из двух частей:
- Certora Verification Language
- Certora Prover
Certora Verification Language - CVL
Это специальный язык, который используется для написания спецификаций для смарт контрактов
Certora Prover
Прувер (в переводе с англ. проверяющий/доказывающий) основывается на общеизвестных техниках формальной верификации. По сути это широкое понятие, которое включает в себя несколько частей, включающее в себя компилятор, декомпилятор, статический анализатор и прочее, подробно его устройство разбирается вот здесь, на 57 слайдах
В спецификациях определяются правила анализируемого контракта, которые несут в себе некоторые предположения о его поведении. Эти правила компилируются в логические формулы, которые называются verification condition. Обычно их создается некоторое множество, которое затем отправляется на анализ в SMT Solver
SMT Solver - Satisfiability Modulo Theories Solver. Проверяет могут ли быть удовлетворены условия выражения
Для написания теста формальной верификации по стандарту создается в корне проекта папка certora с двумя подпасками: conf и spec и в них соответственно два файла с расширениями .spec и .conf
На этом сегодня закончу, хороших выходных!
https://t.me/web3securityresearch