Честный обзор ICO CertiK

ICO Website | White Paper | ICO Chat | Medium | Github

Обзор разработан сообществом “Авокадо Одобряет” при поддержке Телеграм канала Золото Бородача. Для удобства читателей структура обзора поделена на пять частей: продукт, команда, партнеры, юридическая часть и заключение. Команду проекта просим публично ответить на вопросы, выделенные жирным шрифтом.

Стоит отметить, что все описанное ниже — это личное мнение автора, которое находится в полном соответствии с законами о Fair Use и Первой Поправкой. Это не торговый совет, а вся информация была собрана только из открытых источников.

Продукт

CertiK — сервис аудита смарт-контрактов и протоколов.

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

Рабочий процесс со стороны клиента выглядит так:

1) Клиент отправляет смарт-контракт в Сертик для проверки.

2) Если смарт-контракт простой, сервис самостоятельно проставляет маркировку кода. Если контракт сложный, метки проставляются клиентом в ручную.

3) Сертик делит смарт-контракт на части и распределяет между узлами сети для проверки кода по принципу Proof of Work.

4) Результаты верификации передаются от узлов к валидаторам для подтверждения правильности проверки.

5) После подтверждения правильности, узлы и валидаторы награждаются токенами проекта, а результаты аудита отправляются клиенту файлом в виде документа [пример].

Продукт делится на шесть инструментов:

1. Умная маркировка;
2. Модульная проверка;
3. Проверка результатов модульной проверки;
4. Открытый протокол для добавления алгоритмов проверки;
5. IDE плагины для улучшения написания кода dApps;
6. Услуги верификации при помощи экспертов;

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

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

1. Умная маркировка кода при помощи глубокого обучения

Наглядный пример маркировки Сертика в смарт-контрактах. @post @pre в комментарии — и есть та самая маркировка. Здесь она обозначает функцию отправки токенов.

Эти метки обозначают действия функций в коде (спецификации) для понимания дизайна контрактов системой Сертика и подготовки к формальной верификации. Также маркировка нужна для проверки контрактов на разных языках программирования. Глубокое обучение (deep learning) нужно для обучения системы самостоятельно ставить метки в нужных местах.

• Как именно работает умная маркировка? Есть ли технические детали?
• Где вы найдете мощности для расстановки умной маркировки? Сколько времени будет занимать этот процесс?
• Умная маркировка будет платной? Если да, то исходя из каких значений будет формироваться цена?
• На каких мощностях будет организованно машинное обучение? И на основе каких данных?
• Кто из программистов занимается реализацией глубокого обучения? У них есть похожий опыт разработки? Просьба указать ссылки на прошлые проекты.
• Какие будут варианты у клиента, если его смарт-контракт оказался слишком сложным для умной маркировки и нужно самому проставить метки, но он этого не умеет?
• Кто проверяет верность спецификаций? Что если умная маркировка создаст спецификацию, которая не соответствуют коду или требованиям клиента?

2. Полная формальная верификация кода с разделением на части

Формальная верификация нужна для автоматической проверки математических моделей смарт-контрактов на соответствие ранее проставленным меткам (спецификациям). Разделение на части нужно для быстрой, тщательной, дешевой и децентрализованной проверки кода. Также разделение решает основную проблему проверки моделей — взрыв состояний (масштабирование).

• Как математические модели могут быть совместимы с любыми языками программирования? Есть ли технические детали реализации?
• Верификация будет включать в себя тестирование работы кода? Если да, то кто этим займется и безопасно ли это для нод, запуск непроверенного кода? Если верификация без тестов, то как вы проверите что математическая модель безошибочна и код не упадет после запуска?
• Если проверяющих узлов и валидаторов несколько, то как результат верификации будет соединяться для отправки клиенту? Кто отправит клиенту файл с результатом?
• Сколько раз код может провериться узлами, пока валидатор не подтвердит его соответствие спецификации? Как будет происходить перепроверка кода — для каждого модуля будут новые узлы или одни и те же?
• Если узлы проверяются валидаторами, то кто проверит валидаторов? Где гарантия, что валидатор не пропустит результат узла без должной проверки?
• Каковы минимальные технические требования, для того чтобы стать валидатором или узлом сети?
• Сколько времени может занимать верификация? Как будет формироваться её цена?
• Чтобы проверить смарт-контракт, оплата должна проходить только в токенах Сертика? Если да, то где клиенту взять токены, кроме как купить на бирже?
• Вы можете дать полную гарантию безопасности смарт-контрактов, которые были проверены платформой CertiK?

Общие вопросы по проекту

• Кто будет пополнять базу Сертика известными уязвимостями смарт-контрактов? Как это будет происходить?
• Кто будет проверять алгоритмы добавляемые в протокол?
• Для каких IDE и языков программирования будут разработаны сертифицированные плагины? Код этих плагинов будет в открытом доступе?
• Кто будет предоставлять экспертные услуги аудита на платформе? Возможно ли самому стать экспертом? Какие для этого требования?

На момент написания обзора, на гитхабе Сертика четыре репозитория, три из которых форки чужих смарт-контрактов. Четвертый репозиторий хранит документацию CertiK, в которой приведен пример маркировки части кода на Solidity. Продукта Сертика в открытом доступе нет.

• Планируется ли публикация кода продукта в открытом доступе? Если да, то что именно опубликуете и когда?

В конце августа 2018 года Сертик объявили о запуске инструмента автоматической проверки смарт-контрактов — Certik AutoScan Engine. По утверждениям команды, с помощью этого инструмента проведена полная проверка контрактов токенов на Etherscan. Также опубликован 30-секундный ролик с демонстрацией проверки.

Первоначальные результаты проверки опубликованы в статье Сертика на Medium. Команда не может раскрыть имена токенов и расположение уязвимостей из-за соображений безопасности. Они написали владельцам контрактов, и после решения вопросов обещают опубликовать результаты. Ещё CertiK обещают связаться с криптобиржами для интеграции в них авто-сканера контрактов.

• Будет ли исходный код или сам AutoScan Engine публичен? Если да, то когда?
• Какие гарантии того, что видео выше — не простой рендер, а 500 токенов не были просто вручную проверены экспертом, у которого занимает всего 10–15 минут на проверку короткого кода большинства смарт-контрактов?

На сайте CertiK есть бланк для отправки заявок на аудит контрактов. Проект опубликовал отчеты об аудите контрактов у пяти ICO проектов: Blockcloud, MultiVAC, IoTeX, Top Network и Celer. Все они имеют 100 или около ста очков без серьезных ошибок.

• У вас есть примеры аудитов, где CertiK находит бэкдоры или критические ошибки в смарт-контрактах проектов?

Запуск тестнета запланирован на июнь 2019 года, а майннета на декабрь. Судя по дорожной карте, уже выпущена стабильная версия сервиса проверки контрактов и бета-версия умной маркировки.

• Где можно попробовать стабильную версию проверки контрактов и бета-версию умной маркировки?

Команда

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

История проекта начинается с 2016 года, когда текущий соучредитель Сертика, Ronghui Gu, написал докторскую диссертацию в Йельском университете США. Тема диссертации: “Расширяемая архитектура для создания сертифицированных последовательных и параллельных ядер ОС”. В результате этой работы, во главе со вторым соучредителем Сертика, Zhong Shao, разработано CertiKOS — ядро операционной системы с высокой защитой от хакерских атак. Позднее CertiKOS стал частью научного проекта DeepSpec, что разрабатывает спецификации и верификации для софта. И соответственно команда Сертика участвовала в этих исследованиях. Также утверждается, что CertiKOS широко используется в военных целях. Это правда, что CertiKOS популярное исследование в сети, но публичной связи с военными мы не нашли.

• Где найти доказательства того что военные используют CertiKOS и работа над ним не осталась на этапе исследований?

Команда CertiK состоит из экспертов мирового уровня по формальной верификации, которые являются профессорами Колумбийского и Йельского университетов, а также старшими разработчиками и исследователями Google, Facebook и Microsoft Research.
— Белая Книга CertiK, 5 страница

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

Zhong Shao — соучредитель

• Профессор информатики в Йельском университете;
• Доктор компьютерных наук Университета Принстон;
• Главный исследователь проекта DeepSpec и основатель исследовательской команды FLINT, которые разрабатывают многоядерную защищенную от кибератак ОС — CertikOS. Команда Flint имеет около 90 исследовательских статей, где Чжун Шао автор или соавтор. Также они разработали сертифицированный компилятор SML / NJ;
• Длинное резюме из списка исследований, активностей и грантов. В 2008 году был приглашенным исследователем Microsoft Research;
• Сильный информационный след в сети;
• Гитхаб давний, но неактивный.

Ronghui Gu — соучредитель

• Доцент информатики в Колумбийском университете;
• Доктор компьютерных наук Йельского университета;
• В резюме указывает, что в 2016–2017 годах работал разработчиком Google;
• Соавтор восьми исследований по теме сертифицированного и верифицированного кода;
• Сильный информационный след в сети;
• Гитхаб давний, но слабо активный.

Muhan Zou — соучредитель, исполнительный вице-президент, директор по стратегии

• Более двух лет работал веб-разработчиком SaaS сервиса Oracle;
• Около трех лет работал старшим разработчиком в рекламной компании FreeWheel;
• Гитхаб давний, но неактивный.

Vilhelm Sjoberg — главный исследователь

• Доктор компьютерных наук Университета Пенсильвании.
• Около четырех лет работал научным сотрудником исследовательской группы FLINT.
• Соавтор 14 научных публикаций по темам верификации и языков программирования.
• Гитхаб давний, но неактивный.

Zhaozhong Ni — вице-президент по инжинирингу

• Доктор компьютерных наук Йельского университета;
• Автор и соавтор около 12 научных публикаций по теме верификации кода, в том числе и модульной;
• Соавтор двух патентов, связанных с системой хранения данных;
• Три года работал исследователем сертификации кода в Microsoft;
• Около трех лет работал системным инженером 3PAR — оборудования хранилища данных, приобретенное Hewlett-Packard;
• Долгое время (по коммитам на Гитхабе 1 год, по Линкедину 7 лет) работал в Google разработчиком над gVisor — фреймворком, что интегрируется в Docker или Kubernetes для улучшения защиты контейнеров.

Daryl Hok — главный операционный директор. Если верить Линкедину Дэрила, он имеет около семи лет опыта развития и управления двумя технологическими компаниями среднего размера.

Yvan Nasr — руководитель отдела развития бизнеса. MBA из Чикаго. Пол года работал старшим директором по партнерствам в блокчейн-стартапе Hosho, что предоставляет аудиторские услуги смарт-контрактов и протоколов. Также Иван указывает хороший опыт консалтингового управления компаниями в течение десяти лет, среди которых есть Samsung, финтех Barclays и торговая сеть Kingfisher.

Kai Yan — директор по бизнесу. Доктор философии по экономике. Почти шесть лет работал экономистом в Международном Валютном Фонде и около двух лет стратегом в хедж-фонде Light Sky Macro.

Указаны явно не все члены команды. Судя по тому, какие люди указывают в LinkedIn местом работы CertiK, есть еще аналитики, менеджеры, бухгалтер и фронтенд разработчик.

В Белой Книге Сертика написано, что они планируют нанять 20 инженеров-программистов и научных исследователей. На сайте проекта открыты 8 вакансий. Также принимают студентов на практику.

Партнеры

Партнеры, фонды и клиенты Сертика

Большая часть партнеров публично подтверждаются. Всего у Сертика около двадцати одного клиента по аудиту смарт-контрактов.

На сайте Etherscan Сертик добавлен в список рекомендуемых аудиторов смарт-контрактов. Также в Белой Книге проекта на 19 странице утверждается, что Сертик уже стал партнером криптобирж Binance, OKEx, Huobi, Bittrex и Kucoin в качестве рекомендуемого или обязательного аудитора. Но в заявлениях на листинг токенов и вообще на биржах мы не нашли ничего связанного с CertiK.

• Где найти подтверждение того что CertiK рекомендуемый аудитор указанных криптобирж?

Инвесторы Сертика: Binance Labs, NEO Global Capital, LinkVC, Kosmos, Torque Capital, XRP Capital и DFG — все публично подтверждаются. Также прессой и командой проекта утверждается, что они через Колумбийский университет получили гранты IBM, QTUM и Ethereum Foundation для разработки формальной верификации и языка программирования DeepSEA.

Юридическая часть

Технологическая компания Сертика зарегистрирована в штате Delaware под номером 6767945 на Ronghui Gu.

Компания Сертика для приема инвестиций зарегистрирована в Сингапуре под номером 201804796Z. А там по продаже токенов их консультирует юридическая фирма Tzedek Law LLC.

Никто из команды проекта не фигурирует в листингах санкций OFAC.

Пометка про Kai Yan — это ошибочное совпадение с китайской компанией

Судя по результатам Whois, с регистрацией домена certik.org все чисто.

У Сертика два типа токенов — CKT и CKG (газовый, как у NEO), оба нативные Utility. Они нужны для оплаты клиентами за услуги аудита и использование IDE плагинов, а также для вознаграждения узлов, валидаторов и разработчиков за работу.

В Белой Книге Сертика на 12 странице заявлено:

Токены CKT и CKG не подлежат возврату и не могут быть обменены на наличные деньги (или эквивалентную стоимость в любой другой виртуальной валюте) или любое платежное обязательство Фонда и любого аффилированного лица;

• Это значит, что вы не планируете листинг токена на биржах?
• Почему вы отказались принимать токены обратно? Что делать если у команды не получится запустить основную сеть или проект закроется?

Вероятно это отчасти решается тем, что на время ICO токен будет формата ERC-20, его то и будут листить на биржах еще до запуска основной сети. А при запуске основной сети токены перейдут на нативные CKT своего блокчейна.

Проект запрещает инвестировать гражданам США, Канады, Новой Зеландии, Китая и Кореи.

Судя по словам команды, инвестиции аккредитованных инвесторов на сид раундах принимались через контракты SAFT и SAFE.

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

• Вы можете предоставить нам номера заявок или ссылки на патенты CertiK?
• Вы проводили оценку стоимости технологии CertiK? Если да, то где найти отчет оценщика?

Заключение

Автоматизированный аудитор смарт-контрактов — сложный продукт в разработке и продажах. Команда имеет сильный академический опыт, за их спиной два университета и крупные фонды. Часть продукта могут довести до публики, но дальше — искать клиентов — будет сложнее всего. С виду юридически чистые, но за патенты нужно ответить.

Тезисно очертим ключевые риски проекта:

• Нет публичной информации о стратегии и планах продвижения.
• Имеются крупные конкуренты: Quantstamp и Open Zeppelin. Оба активно и давно работают. Используют разные методологии.
• Слабая модель токена из-за необходимости клиентов покупать токены на биржах, конвертировать в нативные и только потом пользоваться сервисом. С этим же препятствием для входа столкнулся Quantstamp, из-за чего они включили эфир и фиат за оплату аудитов.
• Отсутствие публичной информации о токенометрике, пуле ликвидности, политике выкупа и условиях ранних инвесторов.
• На гитхабе кода нет, а продукт приватен. Пощупать то что уже сделал проект невозможно.

В целом о проекте ещё мало информации, но это можно опустить из-за специфики продукта и отсутствия ICO в данный момент.

Не стесняйтесь хлопать в ладоши или кричать в комментариях, если увидите какие-либо упущения или ошибки. Спасибо!