Ср. Авг 4th, 2021
    Free TON

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

    • Расскажите, пожалуйста, о вашем бэкграунде и как все начиналось.

    Я довольно долго работал в роли руководителя отделов тестирования в таких компаниях, как например Oracle, и мне хорошо известна область контроля качества. Потом мне все надоело, и я стал заниматься бизнесом вместе с моим партнером Андреем Ляшиным (одним из авторов концепции бинарной системы NOT a TON — ред.). Мы с ним начали с высокотехнологичного консалтинга и нас “бросало” довольно сильно, однако в конце концов мы вернулись в “родную гавань”. Я стал директором по производству программного обеспечения в традиционной аутсорсинговой компании, но хотелось чего-то другого.

    И вот лет восемь назад Андрей узнал о формальной верификации. Было полное ощущение, что за этим есть будущее, бизнес, что-то большое и интересное, но мы никак не понимали — что именно. Пробовали разные варианты, заходили с разных сторон, и в итоге появилась идея о том, что это может быть интересно для смарт-контракта. И действительно, на каком-то этапе нас познакомили с ребятами из Free TON, которые придерживаются того же мнения.

    • Как давно пришла идея создать именно систему субуправления формальной верификации во Free TON?

    Несколько месяцев назад, когда стали запускать первый конкурс, мы столкнулись с тем, что, к сожалению, в главном Governance многие люди не обладали компетенциями, чтобы объективно оценивать происходящее. И вот как раз тогда возникла идея объединить экспертов в этой области в отдельный SubGovernance, чтобы группа могла целенаправленно заниматься привлечением новых команд, развитием уровнем экспертизы, обменом опыта и т.д.

    • Что же такое формальная верификация?

    Существует комплекс quality assurance — т.е. это не только продвинутое тестирование, но и большой комплекс мер, начиная от правильной архитектуры, заложенной в программный продукт, и заканчивая интенсивным пост-продуктовым мониторингом. Такое программное тестирование ставит цель сделать продукт достаточно надежным. И в 99% случаев для практического использования вам этого будет достаточно.

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

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

    В отличие от тех областей, которые я называл первыми, финансы — это часть с относительно простым и низким порогом вхождения. Если разрабатывать медтехнику, нужно получить сертификаты, лицензии и т.д., а финансы — это более простая активная часть. Тем более сейчас появилось такое шикарное направление, как ФинТех — семейство различных интересных сервисов, разработанных и выпущенных небольшими поставщиками. И вопрос надежности остается достаточно острым для сервисов подобного рода.

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

    Поэтому именно такая область, как ФинТех, для определения качества предъявляет особые претензии, которые в принципе не могут быть достигнуты продвинутым тестированием. И тут на помощь приходят именно методы формальной верификации.

    Помните теорему Пифагора? Вы нарисовали прямоугольный треугольник, померили катет, гипотенузу, и сумма квадратов катетов совпала с квадратом гипотенузы. Ох, подумали вы, интересно получилось, а может быть есть какой-то закон? Нарисовали такой второй, третий, пятнадцатый треугольник и каждый раз вы убеждаетесь, что сумма квадратов катетов равна квадрату гипотенузы.

    Т.е. вы можете сказать, что такое может быть всегда? Скорее всего да, и это грубо говоря тестирование. Вы провели 15 тестов и показали, что это правило выполняется. Если же мы теорему Пифагора доказываем, то говорим, что все, вопрос закрыт — так будет всегда. Это то, что является формальным методом.

    • Вот здесь как раз и кроется магия. Потому что, как это применить к программному обеспечению, совершенно непонятно.

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

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

    В определенном смысле, магия тут, конечно, присутствует. То есть это и не обычное программирование, и не вполне обычное тестирование, и не вполне обычная математика. Это то, что находится на стыке этих дисциплин.

    • В документе о создании субуправления Формальных методов на первом этапе указаны интересные мероприятия, касающиеся беседы с разработчиками. Вы выясняете, как выглядит система, которую они разрабатывают, затем каким-то образом строите модель и пытаетесь найти в ней уязвимости. Правильно?

    По сути, да. На самом деле, главная проблема на сегодняшний день — получение формальной спецификации. Не единственная, но, наверное, главная. То есть на простом уровне мы говорим, что доказываем, что программа будет работать правильно. А что такое “правильно”? “Правильно” — значит, что она будет соответствовать какой-то спецификации, но эта спецификация, в свою очередь, может быть ошибочной и не соответствовать желаемой бизнес-логике.

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

    Этими вещами мы планируем заниматься в ближайшее время очень активно. А сейчас для того, чтобы создать нормальную спецификацию, нам обязательно нужно получить максимальную информацию от разработчиков, что же они хотели на самом деле. Зачастую это не очевидно.

    • Можно сказать, что для каждого конкретного продукта надо разработать свою модель?

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

    Существует несколько языков для формальной верификации, но конкретно мы любим программировать на Coq.

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

    • Система формальной верификации в первую очередь гарантирует отсутствие ошибок при проектировании системы и именно в логике работы программы. Но дает ли она гарантию от ошибок, если уязвимость существует в самих программных инструментах?

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

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

    • На чем в первую очередь будет сосредоточена работа в субуправлении Формальных Методов?

    На данный момент проведена работа с мультисигом, депулом, необходимыми смарт-контрактами. Соответственно, SMV как система голосования, TIP-3 и новый электор, необходимый для запуска новой ноды — это то, что нужно в первую очередь. Также, думаю, будет проводиться какая-то работа и по DeFi, потому что DeFi биржа — это то, что крайне необходимо для привлечения средств в экосистему. Что будет дальше — пока еще обсуждается.

    • В субуправление Формальных Методов вошли также сотрудники из Origin Labs, они тоже специализируются на формальной верификации, вы с ними раньше сталкивались в других проектах?

    Мы слышали о них, хотя до этого в одних проектах не сталкивались. Они весьма квалифицированны, хотя используют несколько иную систему использования формальных методов. Мы будем рады поработать вместе и обменяться опытом.

    9
    0