Искусство постоянных улучшений

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

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

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

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

В итоге многие криптовалюты описаны или только “на бумаге” (что годится разве что для строчки в резюме), или написанным на скорую руку кодом. Ни одна из десяти18 криптовалют, на данный момент лидирующих по показателю рыночной капитализации, не имеет в своей основе протокола, прошедшего рецензирование. Ни одна из этих десяти криптовалют не была создана на основе формальной спецификации19.

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

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

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

Факты и мнения

Другой важный вопрос — где заканчиваются факты и начинаются мнения. Существуют сотни языков программирования, десятки парадигм разработки и более чем одна философия управления проектами. В научных кругах много своих проблем, которые возникают из-за того, что ученые не думают о практичности и о коммерческой стороне вопроса.

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

Протокол Ouroboros — наше первое исследование в данной области. Он спроектирован командой криптографов с огромной, разносторонней и общепризнанной историей публикаций. Его создатели использовали стандартную криптографическую методологию с использованием доказательств, допущений о безопасности, а также модели угроз. Доказательства прошли проверку на конференциях20, а также независимую проверку доказательными вычислениями, написанными на языке Isabelle командой Кембриджского университета21.

Но одно это не предоставляет никаких гарантий полезности протокола — просто тщательная проверка модели безопасности с некоторыми допущениями. Чтобы проверить полезность протокола, нужно его реализовать и протестировать. Наши разработчики реализовали протокол и на Haskell, и на Rust. Эта работа показала, что следует сосредоточить больше усилий на модели синхронизации, и это привело к созданию Ouroboros Praos.

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

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

Функциональные огрехи

Тема, которую мы будем обсуждать, достаточно субъективна: инструменты, языки программирования и методологии, используемые в разработке — все это больше вопрос “приверженства религии”, чем объективной реальности. Исходный код — это как проза. У всех есть мнение насчет того, что такое “хорошо” — и то, что говорится, зачастую не так важно, как то, как это говорится.

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

Протоколы, делающие возможным создание Cardano, реализованы на Haskell. Пользовательский интерфейс воплощен форком Electron, который мы назвали Daedalus. Мы решили использовать веб-архитектурную модель там, где это возможно, а для базы данных выбрали парадигму key-value с использованием RocksDB.

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

Выбор WebGUI позволит нам использовать React и разрабатывать фронтенд при помощи инструментов, знакомых сотням тысяч JavaScript-разработчиков. Использование веб-архитектуры означает, что с компонентами можно работать как со службами, а модель безопасности достаточно разумна.

Самым сложным решением оказалось выбрать Haskell для разработки протокола. Даже в мире функциональных языков программирования выбора достаточно. Более гибкие языки, но с побочными эффектами — например, Clojure, Scala and F# — пользуются огромными библиотеками из экосистем Java и .Net и при этом сохраняют некоторые из лучших черт функционального программирования.

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

В случае Cardano мы выбирали из Ocaml и Haskell. Ocaml — прекрасный язык с отличным сообществом, хорошими инструментами, приятным опытом разработки на нем и прекрасным наследием в области формальных верификаций (см. Coq23). Так почему же мы выбрали Haskell?

Почему именно Haskell?

Протоколы, из которых состоит Cardano, — распределенные, связаны с криптографией и должны обладать высокой отказоустойчивостью. Даже при самом удачном раскладе все равно будут “византийские генералы”, искаженные сообщения и неисправные клиенты, невольно устраивающие в сети разгром.

Во-первых, мы хотели язык с мощной системой типов, где мы бы могли с легкостью использовать инструменты вроде QuickCheck и более сложные техники вроде Refinement Types, при этом предполагая достаточную степень отказоустойчивости. OTP model в стиле Erlang удовлетворяет последнему требованию, а языки вроде Haskell и Ocaml — первому.

С появлением Cloud Haskell Haskell унаследовал множество преимуществ Erlang, не потеряв собственных плюсов. Кроме того, модульность и компонуемость Haskell позволила нам использовать для Cardano специальную облегченную библиотеку под названием Time Warp.

Во-вторых, последние несколько лет библиотеки Haskell быстро развивались благодаря масштабной работе коммерческих компаний, например, Galois, FP Complete и Well-Typed. В итоге Haskell можно использовать для написания промышленных приложений24.

В-третьих, быстрое развитие PureScript привело к появлению давно ожидаемого моста к миру JavaScript — так язык Clojurescript многое дал Clojure. Мы ожидаем, что PureScript будет особенно полезен, когда нам нужно будет заставить Cardano работать в браузере, а также при разработке мобильных кошельков.

В-четвертых, разрешение зависимостей в Haskell в последние годы значительно улучшилось в результате значительных общественных и технологических усилий, возглавленных такими специалистами, как Michael Snoyman. Эти работы велись с помощью платформы Stackage, которую легко использовать, а также она поддерживается компанией FP Complete.

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

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

Формальная спецификация и верификация

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

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

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

Для того, чтобы решить, насколько подробной должна быть спецификация и сколько труда и проверок следует вложить в протокол, приходится применять интуицию. Например, такие проекты, как SeL4 Microkernel project, являются отличной иллюстрацией того, как попытки избежать неопределенности потребовали почти 200 тысяч строк кода на Isabelle для проверки менее 10 тысяч строк кода на C. Но ядро операционной системы — важнейшая часть инфраструктуры, и если ее реализовать неправильно, может получиться серьезная брешь в безопасности.

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

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

Во-вторых, для проверки кода на Haskell на соответствие техническому описанию мы можем выбрать два распространенных варианта: работать с SMT-решателями при помощи LiquidHaskell или использовать Isabelle/HOL.

SMT-решатели (от “satisfiability modulo theories” — задача выполнимости формул в теориях) решают задачу нахождения переменных, которые удовлетворяют уравнению или неравенству, или показывают, что подобные параметры не существуют. Как обсуждалось авторами De Moura и Bjørner, SMT могут использоваться в различных случаях, но главное — эти очень мощные техники могут значительно уменьшить количество неполадок и семантических ошибок.

С другой стороны, Isabelle/HOL — более выразительный и гибкий инструмент, который можно использовать и для описания, и для проверки реализации протокола. Isabelle — классический инструмент для доказательства теорем, он работает с логическими конструкциями высшего порядка и способен представлять множества и другие математические объекты для использования их в доказательствах. Isabelle можно совмещать с доказателем теорем Z3 SMT, если необходимо работать с задачами, в которых есть соответствующие ограничения.

Оба подхода имеют свои преимущества, поэтому мы решили использовать их оба поэтапно. Написанные человеком доказательства мы превратим в код на Isabelle, чтобы убедиться в их корректности и удовлетворить требование о машинных проверках. А потом мы собираемся постепенно вводить Liquid Haskell в исходный код Cardano на протяжении 2017 и 2018 года.

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

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

Прозрачность

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

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

Кроме того, сторонние участники могут влиться в беседу и увести ее в бесполезное (но интересное им самим) русло. У каждого есть своя “священная корова”.

Как совместить прозрачный процесс разработки, нужный сообществу, доверившемуся нашей команде разработчиков, и возможность открыто высказывать свое мнение, ничего не боясь?

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

С кодом все не так просто. Мы доверили организации Cardano Foundation право быть конечным аудитором работы IOHK. В частности, у этой организации следующие обязанности:

  1. Регулярная проверка исходного кода в Github-репозитории Cardano на качество, полноту тестов, подробные комментарии и завершенность

  2. Проверка всей документации Cardano на корректность и полезность

  3. Проверка того, что протоколы, разработанные учеными, полностью реализованы

Для выполнения этого задания IOHK будет предоставлять регулярные и своевременные отчеты Cardano Foundation и уполномоченным этой организацией третьим сторонам. Cardano Foundation, в свою очередь, будет публиковать для сообщества Cardano доклад по итогам надзорной деятельности как минимум раз в квартал.

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

И поэтому после того, как в CSL появится система казначейства, Cardano Foundation наймет дополнительные команды разработчиков для создания альтернативных клиентов по формальной спецификации, разработанной в сотрудничестве с IOHK. Разнообразие в разработке — отличная техника, которую использовал проект Ethereum, чтобы избежать формирования монокультуры вокруг одного набора идей или одной команды разработчиков.

Говоря о спецификациях, многое можно почерпнуть из стандартоориентированных процессов, которым следуют WC3 и IETF. Но каждый протокол, который используется в Cardano, требует спецификации, которая не ссылается на научные работы или исходный код. Она должна быть в подходящем формате, например, RFC.

Одна из важнейших задач Cardano Foundation — выступать в качестве комитета стандартов для протоколов Cardano и создавать условия для ведения дискуссий по обновлению, добавлению и изменению стандартов, имеющих отношение к Cardano. Если интернет — продукт стандартов — с помощью IETF смог достигнуть согласия по поводу того, какие ключевые протоколы использовать, то вполне разумно предположить, что специализированный орган может помочь решить ту же задачу.

В завершение скажем, что интересно было бы попробовать переместить подобные обсуждения в децентрализованную сущность на базе блокчейна. Эта концепция называется ДАО, децентрализованная автономная организация (DAO, decentralized autonomous organization), и на данный момент мы ведем предварительные работы в этой области. IOHK собирается разработать эталонную DAO-модель для сущностей, взаимодействующих с Cardano, чтобы при желании можно было ей воспользоваться. Cardano Foundation решит, следует ли включать ее в требования по стандартам.


18: На coinmarketcap.com можно найти наглядный список криптовалют, отсортированный по рыночной доле.

19: У Ethereum есть полуформальная спецификация, известная под названием Yellow Paper. Однако в ней не полностью прописана семантика EVM (виртуальной машины Ethereum), и этого недостаточно для точной реализации протокола.

20: Принятая статья номер 71 на ежегодной криптоконференции IACR (International Association for Cryptologic Research, рус. Международная ассоциация криптологических исследований) в Калифорнии.

21: Автор — Kawin Worrasangasilpa, супервизор — профессор Lawrence Paulson.

22: Слегка отходя от темы — развлечения ради стоит посмотреть видеоролик Professor Halmos’s discussion about how to write a math textbook.

23: Раз уж мы об этом говорим, у IOHK вообще-то есть проект на Ocaml под названием Qeditas, который нам передал некто под псевдонимом Bill White.

24: Bryan O’Sullivan отлично рассказывает о промышленном применении Haskell здесь.