Верифицируемые смарт-контракты на Solidity/Vyper на основе автоматного программирования

Семинар. 45 минут. 07.09.2018 г.

Сергей Оршанский, PhD, Максим Коротков, MBA

Большинство смарт-контрактов пишется на Solidity (Тьюринг-полный язык, который не поддается формальной верификации). При этом объем кода контракта невелик (сотни строк), риски же велики (Dao Attack – ущерб 50 миллионов долларов, Parity attack – 30 миллионов долларов, и т. д.). Мы считаем, что smart contract, используемый в ICO, заслуживает как минимум не меньшего внимания к его валидации, чем алгоритм работы кофе-машины (https://is.ifmo.ru/download/2008-03-12_verification-en.pdf).

В связи с этим, мы в своем проекте Ethereum Smart Contract in Blockchain применили автоматное программирование, что позволяет верифицировать правильность логики контракта. В дальнейших планах язык – автоматного программирования для Ethereum, который мы назвали Etherel (планируется использовать синтаксис похожий на Esterel). Код на этом языке может компилироваться в Vyper/Solidity, но будет поддаваться формальной верификации.

В применении конечных автоматов для Smart Contract обнаружилась специфика Ethereum: в нём нет таймера, поэтому любые изменения smart contract инициируются внешней транзакцией. Чтобы обработать эту ситуацию корректно мы ввели термин «вычислимые состояния». Это означает, что переменная state хранит старое значение, но по любому внешнему воздействию автомат переходит в другое состояние. Пример: окончание продажи токенов уже произошло (по расписанию), но так как никаких запросов к smart contract не было с момента окончания продажи, контракт об этом «не знает».

На семинаре мы расскажем о том, как применение конечных автоматов помогает улучшить надежность Smart Contract, продемонстрируем рабочий код ICO, использующий конечные автоматы, обсудим дальнейшее развитие – переход на Vyper или создание самостоятельного языка автоматного программирования для EVM: Etherel.

Семинар не является введением в blockchain/Ethereum/Solidity. Рекомендуется владение следующими понятиями:

• электронная подпись, асимметричная схема (алгоритмы, математика);

• биткойн (практическое использование и алгоритмы);

• смарт-контракты (практическое использование);

• ICO (Initial Coin Offering) (практическое использование);

• Эфириум и язык Solidity (практическое использование, алгоритмы, программирование);

Если у вас нет базовых знаний по этим областям – рекомендуем следующие материалы:

1. Текущая активность на Эфириуме, https://etherscan.io/;

2. Как создать монетку на Эфириуме, https://ethereum.org/en/developers/docs/standards/tokens/;

3. Зачем нужны смарт-контракты, https://yandex.ru/video/preview/16073551648144989019;

4. Некоторые технические детали биткойна, Anders Brownworth;

5. «Hello, world!» на Эфириуме, язык Solidity;

6. Электронная подпись, асимметричная схема.

Детальных математических знаний о достижении консенсуса на блокчейне не требуется, достаточно общего понимания.

Авторы написали на эту тему статью Building Verifiable Smart Contracts in Solidity/Vyper with Finite State Machines (https://maximk.com/files/fa-draft.pdf).