В пятницу, 16 августа, 2018, в 8 часов вечера (KST), АМА (Спроси меня что угодно) с соучредителем CertiK профессором Ronghui Gu была проведена в телеграм группе BlockDaily.

BlockDaily AMA — это проект сообщества, который приглашает блокчейн-проекты или лидеров отрасли в онлайн — сообщество отвечать на вопросы в режиме реального времени.

Ниже приведены вопросы и ответы.

Привет Ronghui, нам очень повезло что у нас появилась возможность пригласить Вас в BlockDaily АМА. Могли бы вы представиться?

Ronghui: конечно, это Ronghui Gu. Сейчас я доцент кафедры компьютерных наук Колумбийского университета. Я получил ученую степень компьютерных наук в Йеле, перед этим мой учебный путь начинался в Цинхуа (Китай). Мое исследование сосредоточено на области формальной верификации и это положило начало компании CertiK (https://certik.org/) вместе с профессором Zhong Shao (председатель Компьютерных Наук Йельского Университета), целью которого является создание более надежных блокчейн экосистем с помощью формальных методов проверки.

Вопрос 1. Давайте сначала зададим легкий вопрос. Как вы придумали проект (немного информации из бекграунда)?

Ответ: Мы работаем в области формальной проверки уже много времени. (проф. Shao, более 30 лет в этой области). Вообще говоря, формальная проверка заключается в использовании математических способов доказать, что реализация кода соответствует дизайну (или тому, что мы назвали спецификацией, или архитектуре). В 2017 году многие люди в блокчейн сообществе поняли, что это именно тот метод, который может улучшить существующую малонадежную безопасность в мире блокчейн. Люди из Consensys и многих авторитетных общественных сетей (включая Ethereum Foundation) обратились к нам и надеялись, что мы сможем помочь. Именно поэтому мы сделали CertiK.

Вопрос 2. Что такое “Формальная Верификационная платформа для смарт-контрактов и Блокчейн-экосистем”?

Ответ: Как я только что объяснил, формальная проверка заключается в использовании математических способов доказать, что реализация кода соответствует спецификации. Во многих случаях, особенно в параллельных и распределенных параметрах, такие доказательства слишком сложны для поиска из-за проблемы эксплойта. В 2016 году мы с профессором Shao ввели новую концепцию под названием “DeepSpec”, чтобы сделать такую проверку намного проще для сложных систем, и построили CertiKOS, первое в мире полностью проверенное параллельное ядро ОС. Ядро было развернуто на машине ландшарка (будущей военной машине), которая широко рассматривается как настоящий прорыв (https://news.yale.edu/2016/11/14/certikos-breakthrough-toward-hacker-resistant-operating-systems). Эта формальная Платформа проверки построена на основе наших методов DeepSpec, которые могут быть использованы для обеспечения того, чтобы смарт-контракты и даже сложные реализации блокчейн были безопасными и устойчивы к хакерским атакам.

Вопрос 3. Чем эта технология отличается от других, таких как Quantstamp? (имеется в виду, как вы моделируете все возможности и как исключаете ошибки) и как построен процесс проверки?

Ответ: Это действительно хороший вопрос. 🙂 Во-первых, как я только что объяснил, традиционные методы формальной проверки, как и другие компании, не могут справиться с проблемой эксплойта. Методы DeepSpec, которые мы ввели, решают проблему, обнаруживая “иерархическую структуру” системного программного обеспечения. Все мы знаем, что современные системы строятся с использованием слоев абстракции. Но когда мы проверяем эти системы, структура слоев теряется. Используя DeepSpec, вы можете использовать то, что мы назвали “сертифицированные слоями абстракции”, чтобы разложить сложное обязательство доказательства на множество более мелких и решить каждый из них на слоях, к которым он принадлежит.

Во-вторых, то, что мы можем доказать, называется “функциональной корректностью”. Большинство традиционных формальных методов верификации пытаются доказать некоторые свойства безопасности программы (например, нет переполнения буфера и т.д.). Мы можем доказать, что программа действительно соответствует архитектуре разработчика.

Как сказал Виталик, все ошибки — это “различия” между кодом и намерением разработчика.

Чтобы выявить архитектуру или намерения разработчика, мы вводим легкий язык маркировки, чтобы добавить обозначения в исходный код. Как только маркеры добавлены, наш движок доказательства CertiK может сделать доказательство или найти ошибки автоматически.

Ниже приведена демонстрация, показывающая, как мы можем добавлять маркеры и находить проблемы в смарт-контрактах Bancor:

Вопрос 4. Говорят, что исходный код проверяется с помощью меток, а механизм проверки кода скомпилирован и повторно проверен для улучшения полноты. Однако из-за сложности обучения или языковых ограничений языка Solidity, используются также блокчейны, которые разрабатывают существующий язык БД, Oracle или любой другой собственный язык. Это растущая тенденция. Для исходного кода, который использует эти не популярные языки, будет ли доступна возможность проверить код, или же они получат отказ? Или вы сможете оказать поддержку позже? Если вы собираетесь поддерживать его в будущем, вы понимаете, что проведенные проверки источника будут низкими по качеству, пока у вас не будет накоплен опыт глубокого изучения исходного кода. Есть ли какая-либо контрмера в этом вопросе?

Ответ: Хороший вопрос. Механизм доказательства не зависит от языка. Но на самом деле мы должны создавать интерфейсы для различных языков. Например, многие общественные сети, такие как Neo и Nebulous, предоставили фронт-энд , чтобы CertiK смог помочь разнообразным экосистемам в дополнение к Ethereum. https://medium.com/neo-smart-economy/neo-partners-with-certik-for-next-secure-smart-economic-model-7f342d98e30e

Что касается второго вопроса, да, это правда, количество контрактов, которые могут быть проверены (доказаны) до разработки метода «умной маркировки» (метод, который использует глубокое обучение, чтобы понять архитектуру кода, описанную в техническом документе), будет очень ограничено.

Сегодня я хочу объявить о последней демо-версии нашей разработки (первый в мире выпуск). Мы уже разработали альфа-версию интеллектуального механизма маркировки (Smart labelling) и автоматического сканирования. Движок и автосканирование показан ниже. https://cdn-images-1.medium.com/max/1600/0*tOL9F4NM9Yi6xorV

Мы просмотрели 500 лучших смарт-контрактов. Через 3 часа мы обнаружили, что около 50 из них имеют проблемы уровня безопасности. 🙁 Более подробная информация будет объявлена в ближайшее время. Это первый раз, когда мы покажем эту демонстрацию.

https://www.youtube.com/watch?v=K6GD6URJ8cQ

Вопрос 5. Я знаю, что недавно разработана специальная умная метка под названием OWNER_ONLY_TRANSFER_WARNING в качестве контрмеры из-за взлома учетной записи администратора Bancor, и я хотел бы узнать об этом больше.

Кроме того, после завершения работы над службой проверки контрактов 1.0, я думаю, что вы готовитесь к версии 2.0 для мультиплатформ.

Сможет ли Certik исправлять код, после проверки и обнаружения в нем багов?

Ответ:

Этот ярлык — метка предупреждает разработчика о том, что у владельца больше привилегий, чем это действительно необходимо. Разработка этой метки завершена и оказалась очень полезной для обнаружения проблем.
Мы разрабатываем CertiK 2.0 с более DeepSpec методы были интегрированы. Он может выполнять большую часть задачи проверки автоматически. Более подробная информация будет выпущена в ближайшее время.
CertiK может только помочь обнаружить ошибки или сделать доказательство. Мы или разработчики должны исправить код вручную. Но CertiK может предоставить контрпримеры в качестве подсказок для разработчиков.

Вопрос 6. Вы думаете, что безопасность, предлагаемая решением Certik будет востребована во многих других проектах? (С точки зрения других проектов, они попытаются найти и улучшить свои собственные ошибки, даже если их код не идеален, но мне интересно, хотят ли они получить результаты, предоставив свой исходный код (без обновления) в Certik)

Ответ: Да, один из фундаментальных фактов о платформе CertiK. В общем, наши клиенты могут быть разделены на две категории:

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

Начиная с процесса проверки, клиенты обычно предоставляют нам доступ к их готовому к производству исходному коду, затем мы запускаем проверки CertiK Automation и применяем смарт-метки для обеспечения соответствия спецификации реализации. Как правило, проблемы будут обнаружены нашим движком, и мы уведомим наших клиентов с отчетом об ошибках и предлагаемых исправлениях.

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

Вопрос 7. Я слышал, что у вас есть стратегический Альянс между Certik и QuarkChain. Что такое модульная проверка, введенная командой Certik? Можно ли использовать сертифицированные библиотеки DApp и подключаемые модули IDE Certik, чтобы значительно сократить время отладки и проверки безопасности и надежности кода?

Ответ: Да, мы сотрудничаем со многими выдающимися стартапами, которые нацелены на следующее поколение блокчейн-платформ, включая ICON, Aelf, Qtum, NEO, Ontology и так далее.

QuarkChain является одним из них.

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

Что касается сертифицированных библиотек и подключаемых модулей IDE, да, у нас есть планы выпустить больше наших артефактов для общественности, что поможет сократить усилия по разработке (и тестированию) и повысить надежность смарт-контрактов. Следите за нашими объявлениями, и вы будите в курсе наших разработок!

Вопрос 8. Проверка всех смарт-контрактов и ошибок кода займет много времени, так что мне интересно, как вы собираетесь решить эту проблему. Кроме того, по мере увеличения объема кода, это, вероятно, так же замедлит производительность, так что вы думаете?

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

Ответ на второй вопрос заключается в том, что мы должны поддерживать экосистему CertiK. Сообщества должны играть важную роль в ускорении процесса проверки, предоставляя инженерные и вычислительные ресурсы. Это завершает рабочий процесс децентрализованным, масштабируемым способом. Пожалуйста, ознакомьтесь со следующими ссылками для описания экосистемы схемы. https://medium.com/certik/certik-unveiled-ecosystem-d5e93bd6b35d.

Вопрос 9. Я так понимаю, что операция разбивается на более мелкие блоки и решаются распределенно. При разборе, она разбирается с использованием фирменных технологий CertiK — Smart Labeling и Deep Spec, и использованием индивидуальной маркировки специалистов по проверке. Я думаю, что эта декомпозиция на основе слоев займет больше времени, и мне интересно, как мы распознаем и исправляем ошибки в дизассемблировании. Декомпозиция приведет к большему количеству данных, что займет больше времени для поиска и исправления ошибок.

Ответ: Единственный способ исправить сломанные фрагменты — использовать функцию «Композиция». То есть, это зависит от способности перенастроить дезинтегрированные доказательства как сквозное доказательство. Эта конфигурация работает с нашей технологией DeepSpec. В то время как разложение может привести к большему количеству данных (например, больше доказательств), эта процедура делает работу с запрещенными доказательствами более компактной и простой в разрешении. Каждая небольшая единица доказательства будет разрешена почти автоматически в том слое, к которому она принадлежит.

Вопрос 10. Каковы ваши основные ценности в жизни?

Ответ: Профессор Zhong Shao (другой соучредитель CertiK и председатель отдела Yale CS) является ведущей фигурой в области формальной проверки в течение примерно 30 лет. Он внес значительный вклад, чтобы сделать эту технику такой же мощной, как сейчас. Я хотел бы внести свой вклад, чтобы применить эту технику в промышленности.

Приятно было пообщаться! Еще раз спасибо за поддержку CertiK.

Спасибо за то, что пришли к нам, @RonghuiCertik и с нетерпением ждем, чтобы пригласить вас в ближайшее время снова, чтобы получить ответ на еще больше вопросов!! Нам всегда мало информации 🙂

Спасибо за приглашение и отличные вопросы. Надеюсь поговорить со всеми снова в ближайшее время. 🙂

Этот перевод подготовлен специально для Русского сообщества компании CertiK Foundation, — перевод подготовил @MBGBuzzer — Crypto.Red.Team (@crypto.red.team)