Формальная верификация во Free TON: рассказывает Сергей Егоров

Формальная верификация во Free TON: рассказывает Сергей Егоров

В апреле сооснователь компании Pruvendo и один из инициаторов создания субуправления Формальных Методов (Formal Methods Sub-Governance) Сергей Егоров рассказал Free TON House о формальной верификации.

Теперь мы попросили Сергея поделиться новостями о том, как проходит процесс формальной верификации во Free TON и подвести промежуточные итоги.

Начать с нуля: этапы верификации

Процесс формальной верификации будет состоять из четырех или пяти фаз: нулевой, первой, второй, третьей и опциональной четвертой.

Начальный этап мы разделили на две фазы неслучайно. Нулевая фаза — это аудит исходного кода, который мы проводим вручную, исходя из своего опыта. Это делается для того чтобы, во-первых, убедиться в качестве кода, а во-вторых, отправить его на выход для бета-использования, в случае необходимости. 

Формальная верификация — процесс длительный, а бизнес зачастую требует гораздо более быстрой реакции. Поэтому мы предоставляем бизнесу опцию: или выходить быстро, но с более низким уровнем надежности, или долго, но с более высоким уровнем надежности.

Что уже сделано?

Над формальной верификацией активно работают три команды: 

  • Pruvendo 
  • Московский коллектив Infotech
  • Парижский OCamlPro

Полностью прошли верификацию:

Проведены аудиты смарт-контрактов: 

  • SMV 
  • Flex (реализация DEX от TON Labs)
  • DuneSwap (решение для выплаты вознаграждений членам Dune Community) 

В работе — реализация DEX от Radiance.

Что дальше?

Сейчас мы преимущественно погружены в реализацию нулевой и первой фазы. Постепенно приближаемся ко второй — верификации на так называемом функциональном уровне (по сути, экватор всего процесса). В ближайшие дни планируем начать такую работу для контракта Flex, а затем — для SMV.

В планах на относительно ближайшее будущее — большая и масштабная работа по BFTG.

Помимо верификации контрактов мы готовы начать верификацию виртуальной машины Free TON. Первым модулем, который будет подлежать верификации, скорее всего, станет Executor.

Кроме того, когда верифицированных смарт-контрактов станет больше, планируем придумать решение, которое сможет выделить их среди остальных: подпись, каталог или что-то в этом роде.

Есть ли трудности?

Многие нюансы приходится уточнять у разработчиков — есть специфическая информация, которая не покрыта документацией. 

Качество смарт-контрактов пока еще оставляет желать лучшего. Можно выделить только контракты от TON Labs, остальным пока не хватает спецификаций и примеров. Но прогресс есть.

Узнайте больше про Everscale
Подпишитесь на наши социальные сети и будьте в курсе актуальных новостей
SUBSCRIBE ON SOCIAL
Free TON House
Первоисточник