@ramilmust

Про 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 reply

0 recast

6 reactions