Через два роки я повернувся до блогу заради посту, який відрізняється від звичайних занудних лекцій про Haskell та математику. Останні кілька років я займався фінансовими технологіями в ЄС, і, здається, настав час написати на тему, якій технічні ЗМІ приділили мало уваги.
Нещодавно Facebook випустив те, що називає "новою платформою фінансових сервісів" під назвою Libra. Вона позиціонується як цифрова розрахункова система, заснована на кошику міжнародних валют, які керуються на блокчейні і зберігаються в грошовому пулі, керованому зі Швейцарії. Цілі проекту амбітні та спричиняють масштабні геополітичні наслідки.
В и багато розумних статей про необґрунтовані грошові та економічні припущення в основі запропонованої фінансової системи. Але не вистачає фахівців, здатних на аналіз із технічного погляду. Не так багато людей працюють над фінансовою інфраструктурою і публічно говорять про свою роботу, тому цей проект не надто освітлений у технічних ЗМІ, хоча його нутрощі відкриті для всього світу. Я маю на увазі відкриті вихідники у репозиторіях и .
Те, що відкрито світу, — це архітектурно-шизофренічний артефакт із претензією на роль безпечної платформи для світової платіжної інфраструктури.
Якщо зануритися в кодову базу, то фактична реалізація системи цілком розходиться із заявленою метою, причому найхимернішими способами. Впевнений, що цей проект має цікаву корпоративну історію. Тому логічно припустити, що його розробляли з певною старанністю, але насправді я бачу справді дивний набір архітектурних рішень, які ламають всю систему і ставлять під загрозу користувачів.
Не претендуватиму на об'єктивну думку про 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 транзакцій на день. Продуктивність залежить від розміру транзакцій, мережевої маршрутизації, завантаження системи та (Anti-money laundering, схеми відмивання грошей).
Libra намагається вирішити проблеми, які насправді не є проблемами для внутрішніх трансфертів, оскільки національні держави в останнє десятиліття модернізували свою клірингову інфраструктуру. Для роздрібних споживачів у Євросоюзі переміщення грошей взагалі не є проблемою. На традиційній інфраструктурі це можна зробити із стандартним смартфоном за лічені секунди. Для великих корпоративних трансфертів існують різні механізми та правила, пов'язані з переміщенням великих обсягів грошей.
Немає жодних технічних причин, через які транскордонні платежі також не можна проводити миттєво, за винятком відмінностей у правилах та вимогах між відповідними юрисдикціями. Якщо необхідні превентивні заходи (належна перевірка клієнта, перевірка санкцій тощо) виконуються кілька разів на різних етапах ланцюжка транзакцій, це може призвести до затримки транзакції. Тим не менш, ця затримка є суто функцією регулюючого законодавства та його дотримання, а не технології.
Для споживачів немає жодних причин, через які угода у Великій Британії не пройде кліринг за лічені секунди. Роздрібні транзакції в ЄС справді сповільнюються (Знай свого клієнта) та обмеження 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, який будує безпечний, що перевіряється. . Вже існують інструменти для створення примітивів, що піддаються перевірці. Хоча це дорого, але явно не виходить за межі економічних можливостей Facebook. Проте команда вирішила не брати участі у проекті, заявленому як надійний фундамент для світової фінансової системи.
Проект libra від кількох досить нових бібліотек для створення експериментальних криптосистем, які з'явилися лише останні кілька років. Неможливо сказати, чи є залежно від наступних інструментів безпечними, оскільки жодна з цих бібліотек не проходила аудит і не має стандартних політик розкриття інформації. Зокрема, для деяких основних бібліотеки немає визначеності щодо захисту від атак сторонніми каналами та атаками часу.
Бібліотека libra стає ще експериментальнішою і виходить за рамки , застосовуючи дуже нові методи, такі як випадкові функції, що перевіряються (VRF), білінійні пари і порогові сигнатури. Ці методи та бібліотеки можуть бути розумними, але об'єднання їх усіх в одній системі викликає серйозні побоювання щодо площі поверхні атаки. Поєднання всіх нових інструментів і методів значно підвищує складність докази безпеки.
Слід припустити, що весь цей криптографічний стек вразливий для різних атак, доки не доведено протилежне. Відому фейсбуківську модель 'Move Fast and Break Things' не можна застосовувати до криптографічних інструментів, які опрацьовують фінансові дані клієнтів.
Libra не може реалізувати механізми захисту прав споживачів
Відмінною особливістю платіжної системи є можливість відкотити транзакцію у разі, якщо платіж скасовано судовим позовом або призводить до випадкового чи системного збою. Система Libra спроектована для «повної завершеності» та не включає тип транзакції для скасування платежу. У Великій Британії всі платежі від £100 до £30,000 регулюються законом «Про споживчий кредит» (Consumer Credit Act). Це означає, що платіжна система ділить із продавцем відповідальність у разі проблеми з купленим товаром або якщо одержувач платежу не надав послугу. Аналогічні правила діють у ЄС, Азії та Північній Америці.
Нинішній дизайн Libra не включає протокол для дотримання цих законів і не має чіткого плану щодо його створення. Ще гірше, що з погляду архітектури остаточність структури автентифікованих даних ядра, заснована на стані накопичувача Меркла, не допускає жодного механізму створення такого протоколу без перепроектування ядра.
Після проведення технічної експертизи цього проекту можна зробити висновок, що він просто не пройде перевірку в жодному шановному журналі дослідження розподілених систем або фінансового інжинірингу. Щоб спробувати змінити світову грошово-кредитну політику, необхідно зробити величезний обсяг технічної роботи для створення надійної мережі та безпечної обробки даних користувача, якій громадськість і регулюючі органи могли б довіряти.
Не бачу причин думати, що Facebook у своєму проекті проробив необхідну роботу для подолання цих технічних проблем або що він має якісь технічні переваги перед діючою інфраструктурою. Твердження, що компанія потребує гнучкості регулювання вивчення інновацій, не є виправданням для того, щоб не зробити їх спочатку.
Джерело: habr.com