🥇Архитектурная шизофрения Facebook Libra

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

Недавно Facebook выпустил то, что именует «новой платформой финансовых сервисов» под названием Libra. Она позиционируется как цифровая расчётная система, основанная на корзине международных валют, которые управляются на «блокчейне» и хранятся в денежном пуле, управляемом из Швейцарии. Цели проекта амбициозны и влекут масштабные геополитические последствия.

В Financial Times и New York Times много разумных статей о необоснованных денежных и экономических предположениях в основе предлагаемой финансовой системы. Но не хватает специалистов, способных на анализ с технической точки зрения. Не так много людей работают над финансовой инфраструктурой и публично говорят о своей работе, поэтому данный проект не слишком освещён в технических СМИ, хотя его внутренности открыты для всего мира. Я имею в виду открытые исходники в репозиториях Libra и Calibra Organisation.

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

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

Не буду претендовать на объективное мнение о Facebook как компании. Мало кто в IT-индустрии смотрит на неё с симпатией. Но сравнение её заявлений и опубликованного кода ясно показывает, что в заявленной цели фундаментальный обман. Если вкратце, этот проект никого не наделяет полномочиями. Он останется полностью под управлением компании, чей рекламный бизнес настолько запутан в скандалах и коррупции, что у него нет выбора, кроме как попытаться диверсифицировать платежи и кредитный скоринг, чтобы выжить. Чёткая долгосрочная цель состоит в том, чтобы действовать в качестве брокера данных и посредника в доступе потребителей к кредиту на основе их личных данных в социальных сетях. Это совершенно ужасающая и мрачная история, которой не уделяют того внимания, которой она заслуживает.

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

Решение задачи византийских генералов в сети с контролем доступа — это непоследовательный дизайн

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

Оверхед временнóй сложности от этой дополнительной структуры зависит от алгоритма. Есть много литературы по разновидностям протоколов Паксос и Raft с решением задачи византийских генералов, но все эти структуры вводят дополнительные накладные издержки на связь поверх для поддержания кворума. Для Libra выбрали алгоритм с максимально возможной стоимостью связи в случае неудачи лидерства. И возникают дополнительные накладные расходы от потенциальных переизбраний лидеров по нескольким типам событий сбоя сети.

Для системы, работающей в консорциуме высокорегулируемых транснациональных корпораций, где у всех пользователей подписанный Facebook код, а доступ в сеть контролируется со стороны Facebook, просто нет смысла рассматривать злонамеренных участников на консенсусном уровне. Непонятно, зачем вообще эта система решает задачу византийских генералов, а не просто поддерживает согласованный журнал аудита для проверки соответствия. Возможность того, что узел Libra, управляемый Mastercard или Andressen Horrowitz, внезапно начнёт запускать вредоносный код, является странным сценарием для планирования и лучше решается простым обеспечением целостности протокола и нетехническими (т. е. юридическими) средствами.

В свидетельских показаниях для Конгресса продукт объявлен конкурентом новых международных платёжных протоколов, таких как WeChat, Alipay и M-Pesa. Однако ни одна из этих систем не предназначена для работы на пулах валидаторов с решением задачи византийских генералов. Они просто разработаны на традиционной шине высокой пропускной способности, которая делает проводки в соответствии с фиксированным набором правил. Это естественный подход к проектированию платёжной системы. Грамотно спроектированная платёжная система просто не встретится с проблемой двойных трат и форков.

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

У Libra нет никакой конфиденциальности транзакций

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

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

Libra HotStuff BFT не способен достичь пропускной способности, необходимой для платёжной системы

В Великобритании клиринговые системы вроде BAC способны проводить порядка 580 000 000 транзакций в месяц. В то же время сильно оптимизированные системы вроде Visa могут обрабатывать 150 000 000 транзакций в день. Производительность зависит от размера транзакций, сетевой маршрутизации, загрузки системы и проверок AML (anti-money laundering, схемы отмывания денег).

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

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

Для потребителей нет никаких причин, по которым сделка в Великобритании не пройдёт клиринг в считанные секунды. Розничные транзакции в ЕС действительно замедляются на проверку KYC (Знай своего клиента) и ограничения AML, наложенные правительствами и регуляторами, которые в равной степени применимы к платежам Libra. Даже если бы Facebook преодолел препятствия на пути международных переводов и передачи приватных данных, предложенная модель находится в сотнях человеко-лет от пропускной способности глобальных транзакций и, вероятно, подлежит переработке с нуля.

Язык Libra Move некорректен

Технический документ делает смелые утверждения о новом непроверенном языке под названием Move. Эти утверждения довольно сомнительны с точки зрения теории языков программирования (PLT).

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

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

В публичных блокчейнах смарт-контракты сталкиваются с логикой публичных сетей с эскроу-счетами, отмыванием денег, выпуском внебиржевых токенов и азартными играми. Всё это выполняется на потрясающе плохо разработанном языке под названием Solidity, который с академической точки зрения делает автора PHP похожим на гения. Как ни странно, новый язык от Facebook, похоже, не имеет ничего общего с этими технологиями, поскольку это фактически скриптовый язык, предназначенный для неясных корпоративных задач.

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

После заявлений о его безопасности мы должны посмотреть на семантику языка. Корректность в теории языков программирования обычно состоит из двух различных доказательств: «продвижение» (progress) и «сохранение» (preservation), которые определяют согласованность всего пространства правил оценки для языка. Более конкретно, в теории типов функция является «линейной», если использует свой аргумент ровно один раз, и «аффинной», если использует его не более одного раза. Система линейных типов даёт статическую гарантию, что заявленная линейная функция действительно линейна, назначая типы всем подвыражениям функций и отслеживая места вызовов. Это тонкое свойство для доказательства, и его непросто реализовать для всей программы. Линейная типизация по-прежнему остаётся очень академической областью исследований, под влиянием которой реализована уникальность типов в Clean и собственность типов в Rust. Есть некоторые предварительные предложения по добавлению линейных типов в Glasgow Haskell Compiler.

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

Кроме того, формальная семантика предположительно безопасного языка нигде не встречается ни в реализации, ни в документе. Язык достаточно мал, чтобы найти полное доказательство корректности семантики в Coq или Isabelle. В реальности, сквозной компилятор полного преобразования с переносом доказательств до байт-кода вполне можно реализовать современными инструментами, изобретёнными в последнее десятилетие. Мы знаем, как это сделать, начиная с работы Джорджа Некулы и Питера Ли ещё в 1996 году.

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

Криптография Libra некорректна

Построение надёжных криптосистем — очень сложная инженерная проблема, и к работе с опасным кодом всегда лучше относиться с хорошей дозой здоровой паранойи. В этой области есть серьёзные прорывы, как проект Microsoft Everest, который строит проверяемый безопасный стек TLS. Уже существуют инструменты для создания поддающихся проверке примитивов. Хотя это дорого, но явно не выходит за рамки экономических возможностей Facebook. Тем не менее, команда решила не участвовать в проекте, заявленном как надёжный фундамент для мировой финансовой системы.

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

Библиотека libra становится ещё более экспериментальной и выходит за рамки стандартной модели, применяя очень новые методы, такие как проверяемые случайные функции (VRF), билинейные пары и пороговые сигнатуры. Эти методы и библиотеки могут быть разумными, но объединение их всех в одной системе вызывает серьёзные опасения по поводу площади поверхности атаки. Сочетание всех этих новых инструментов и методов значительно повышает сложность доказательства безопасности.

Следует предположить, что весь этот криптографический стек уязвим для различных атак, пока не доказано обратное. Известную фейсбуковскую модель ‘Move Fast and Break Things’ нельзя применять к криптографическим инструментам, которые обрабатывают финансовые данные клиентов.

Libra не может реализовать механизмы защиты прав потребителей

Отличительной особенностью платёжной системы является возможность откатить транзакцию в случае, если платёж отменён судебным иском или приводит к случайному или системному сбою. Система Libra спроектирована для «полной завершённости» и не включает тип транзакции для отмены платежа. В Великобритании все платежи от £100 до £30,000 регулируются законом «О потребительском кредите» (Consumer Credit Act). Это означает, что платёжная система делит с продавцом ответственность в случае проблемы с купленным товаром или если получатель платежа не оказал услугу. Аналогичные правила действуют в ЕС, Азии и Северной Америке.

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

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

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

Источник: habr.com