Исследование и применение подходов к формальной верификации смарт-контрактов на платформе Ethereum

По мере своего развития технология блокчейн проникает в различные отрасли экономики. Появляется большое число смарт-контрактов, автоматизирующих взаимодействие участников децентрализованной сети. Однако их широкое применение подчеркивает необходимость обеспечения безопасности и надежности кода смарт-контрактов, особенно учитывая невозможность его изменения после развертывания. Методы формальной верификации позволяют математически доказать соответствие исходного кода свойствам корректности, тем самым помогая предотвратить ошибки и финансовые потери, связанные с уязвимостями в смарт-контрактах. В выступлении будет представлен анализ подходов к формальной верификации смарт-контрактов в сети Ethereum, которые используются в индустрии на данный момент. Цель обзора — понять преимущества и недостатки этих подходов, а также выявить общие тенденции в данной области. Более того, будет приведен пример применения метода дедуктивной формальной верификации для доказательства корректности смарт-контрактов голосования и автоматического маркет-мейкера. Кирилл Зиборов Positive Technologies