Сб. Янв 1st, 2022
    Formal verification, 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, остальным пока не хватает спецификаций и примеров. Но прогресс есть.

    7
    0