Quanstamp. Немного о технической составляющей проекта

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

Первое с чего стоит начать, это с идеи. Идея проекта - создать инструмент автоматического аудита безопасности исходного кода смартконтрактов сети Ethereum. Реализация этой идеи основана на использовании передовых исследований в области алгоритмов верификации и блокчейн технологий. Ссылаясь на передовые исследования, авторы проекта указывают на алгоритмические решения описанные в книге Дэниела Крининга и Офера Стричмана "Процедуры принятия решения". Есть отличная рецензия-описание книги (на англ.) - http://theory.stanford.edu/~barrett/pubs/B13.pdf

Процедура принятия решения (Decision Procedure) - алгоритм, который решая определенную задачу, всегда оканчивается четким ответом да/нет. В книге авторы фокусируются на применении такого рода алгоритмов для решения теорий первого порядка, которые используются в реальной жизни, например в автоматизированной проверке и анализе, теоретическом доказательстве, оптимизации компилятора и исследовании операций. Данную исследовательскую область в настоящий момент принято называть "Задачей выполнимости формул в теориях" (Satisfiability Modulo Theories - SMT). Также существует понятие "Задача выполнимости булевых формул" (Boolean satisfiability problem - SAT). Отличие SAT и SMT лишь в формате систем уравнений, в одной это произвольный формат, в другой ограничен булевыми уравнениями. Для понимания, что это такое и с чем его едят, мне очень помогло "Краткое введение в SAT/SMT-солверы и символьное исполнение" Дениса Юричева. В нем представлено очень много примеров решения систем уравнений разного уровня сложности с помощью SAT и SMT солверов The Z3.

Итак, основой всего проекта Quanstamp являются узлы валидации (Validator Nodes). Узел валидации - это сильно модифицированный узел сети Ethereum, содержащий в себе аналитический инструментарий, который применяет формальные методы: статический анализ кода, символьное выполнение программ и символьно-конкретное тестирование (Concolic testing), инструменты автоматической проверки (automated reasoning) такие как SAT и SMT солверы. Хотя исследования в области автоматизированных инструментов проверки начались несколько десятилетий назад, практическая применимость их началась только после достижения необходимой производительности вычислительных систем, а это буквально несколько лет назад, поэтому важно чтобы за проектом Quanstamp стояли технически подкованные люди с большим багажом знаний и опыта в этой области. И судя по всему именно такой команда и является. Приведу небольшой пример: они внесли вклад в разработку SAT солвера MapleSAT, который стал одним из победителей на SAT Competition 2016. Лидером проекта был технический советник Quanstamp - Vijay Ganesh. Также он является лидером таких проектов как The Z3 String Solver, MathCheck SAT+CAS system и Attack Resistance.

Рассмотрим работу узла валидации более подробно.

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

Теперь подробнее из чего состоит инструментарий проверки в узле валидации:

SAT солверы. Компьютерные программы моделируются как булевые формулы и передаются в таком виде солверу. При моделировании и тестировании определенной ситуации, булевую формулу можно построить так, что наличии определенных показателей может расцениваться как ошибка. Солвер сообщает "выполнимо", если может найти решение, если нет - "не выполнимо". SAT солверы очень важный инструмент в некоторых областях разработки ПО, включая проверку ПО, анализ программ, их синтез и автоматическое тестирование. SAT солверы уже доказали свою удивительную эффективность, сочетая эвристику решения, дедуктивные рассуждения и различные экспериментально подтвержденные методы.
SMT солверы. Инструмент, который решает выполнимость формул в сочетании различных теорий первого порядка. Общие теории первого порядка, которые могут моделировать фрагменты компьютерного кода для анализа уязвимости, включают в себя равенство, битовые векторы, массивы, рациональные методы, целые числа и разностную логику. Это очень активная область исследований и существует много приложений, самые известные SMT солверы включают Yices (SRI), Z3 (Microsoft), CVC3 (NYU, Айова), STP (Стэнфорд), MathSAT (U. Trento, Италия), Barcelogic (Каталония, Испания).
Проверка моделей. Основана на исполнении кода необычным способом, что часто приводит к обнаружению несоответствий. Метод исследует всевозможные состояния системы методом полного перебора - брутфорсом.
Статический анализ кода. Определяет свойства программы не исполняя ее.
Символьное выполнение программ и Символьно-конкретное тестирование (Concolic testing). Символьное выполнение - техника, которая позволяет проводить моделирование выполнения программы, при котором часть входных переменных представляется в символьном виде. Основным преимуществом метода символьного выполнения является простота и очевидность концепции, на которой он основан: метод использует идею "симуляции" выполнения программы , так, как это делает программист. Метод символьного выполнения получил распространение не только в инструментах статического, но и смешанного анализа. Хорошо зарекомендовали себя инструменты, использующие подход concolic testing (символьно-конкретное - CONCrete+symbOLIC). Concolic testing - это метод поиска дефектов, осуществляющий генерацию тестовых данных, при использовании которых программа проявляет некорректное поведение, на основе символьного выполнения.

Стоит также упомянуть идею распараллеливать аудит проверки с помощью SAT солвера на несколько узлов. Почему вообще появилась такая идея, причина в недостаточных ресурсах вычислительных машин. В зависимости от сложности задач время выполнения проверки может растянуться с нескольких миллисекунд до дней или недель. Типичный параллельный SAT солвер использует подход master-slave, разбивая пространство поиска и параллельно анализируя подпространства в отдельных процессах. Ярким примером такого подхода является Parallel MiniSAT (PMSAT). PMSAT - это распределенный параллельный SAT солвер, реализованный на C++ с использованием интерфейса передачи сообщений (Message Passing Interface MPI) для связи между узлами. Мастер управляет планированием клиентов и распределяет между ними различные задачи.

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

Используя выше описанные концепции, авторы проекта планируют повысить уверенность общественности в безопасности смарт-контрактов, которые будут проходить прозрачный аудит. Это в свою очередь будет мотивировать разработчиков использовать функции Quanstamp каждый раз при создании нового смартконтракта. Таким образом планируется Qunastamp сделать стандартом использования в сети Ethereum.

Послесловие. С технической стороны проект очень хорош, по крайней мере на уровне концепта. И мне лично очень интересно посмотреть во что это в итоге выльется. Но есть один огромный минус - то как они проводят свое ICO. От прочтения условий продажи первичных токенов у меня осталось очень много негативных эмоций. Напомню, что для ограниченного числа людей, прошедший их proof-of-care, предполагалось выделить 3млн.$ для предпродажи со 100% бонусом. Этот факт вызывал очень много вопросов, основным был "Зачем?". Их ответом было то, что они хотят уже в ближайшее время нанять в штат инженеров, чтобы уже сейчас начать пилить проект, им для этого необходим базовый капитал, и именно за счет предпродажи они собираются его получить. Я открыто им написал что это не верная тактика и они обещали ее пересмотреть. И вот итог их пересмотра:

1 уровень потолок 3 млн.$ бонус 100%
2 уровень потолок 4 млн.$ бонус 40%
3 уровень потолок 4 млн.$ бонус 20%

Мне сложно что-либо тут комментировать, лишь то, что такими бонусами ребята убивают свой проект.

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