Разработчики XRP Ledger (XRPL) используют математические доказательства для проверки того, может ли предстоящий кредитный рынок сети быть опустошен или стать неплатежеспособным.
17 сентября фирма по исследованию протоколов Common Prefix сообщила, что она формально проверяет протокол кредитования XRPL с помощью Lean 4, языка доказательства теорем, предназначенного для установления того, удовлетворяет ли программное обеспечение определенным математическим свойствам во всех возможных состояниях системы.
Фирма заявила, что эта работа призвана показать, что протокол не может перейти в состояния, нарушающие его правила учета и безопасности.
Работа приобрела еще большее значение после того, как на этой неделе была выпущена версия xrpld 3.4.0 с LendingProtocolV1_1 — поправкой, которая вводит замкнутые кредитные хранилища и кассовый учет. Поправка включена в серверное программное обеспечение, но все еще требует одобрения в рамках процесса поправок XRP Ledger, прежде чем вступить в силу.
Дизайн кредитования XRPL позволит вкладчикам объединять активы, которые кредитные брокеры могут использовать для предоставления срочных необеспеченных займов. Андеррайтинг заемщиков и оценка кредитоспособности происходят вне сети (off-chain), в то время как реестр записывает выдачу кредитов, погашения и учет.
Это повышает важность правильности внутреннего учета протокола. Ошибки, связанные с балансами хранилищ, платежами по кредитам или расчетами долей, могут затронуть объединенные средства вкладчиков, а не изолированное приложение.
Заблокированный капитал повышает ставки для кредитования XRPL
LendingProtocolV1_1 увеличивает последствия сбоев в учете, поскольку активы вкладчиков могут быть заблокированы на заранее определенный инвестиционный период.
Замкнутые хранилища проходят три этапа: подписка, инвестирование и погашение. Вкладчики могут добавлять или снимать активы на этапе подписки, но оба действия блокируются, как только хранилище переходит в период инвестирования и капитал становится доступным для кредитования. Снятие средств возобновляется, когда хранилище достигает этапа погашения.
График устанавливается при создании хранилища и не может быть изменен позже, предоставляя участникам заблаговременное представление о том, как долго их капитал может оставаться заблокированным.
Версия 3.4.0 также изменяет способ признания процентного дохода новыми хранилищами.
Согласно предыдущему дизайну, запланированные проценты могли быть учтены как доход при выдаче кредита, еще до того, как заемщик произвел эти платежи. Кассовый учет вместо этого признает проценты только по мере поступления платежей, снижая риск того, что стоимость долей в хранилище будет отражать еще не полученный доход.
Эти изменения добавляют больше состояний и переходов, которые должны оставаться согласованными по мере принятия депозитов, выдачи кредитов, поступления платежей, дефолта заемщиков и открытия хранилищ для снятия средств.
Common Prefix использует формальную верификацию для тестирования этих взаимосвязей за пределами сценариев, которые инженеры могли бы предвидеть в обычном наборе тестов.
Исследователи не пытаются математически проверить весь C++ код xrpld. Вместо этого они воссоздают соответствующую логику протокола в Lean 4 и определяют свойства, которые система должна сохранять.
Оракул затем может запускать эквивалентные входные данные против математической модели и производственной реализации, помогая выявлять случаи, когда они ведут себя по-разному.
Это различие имеет значение, поскольку математическое доказательство так же сильно, как и модель и предположения, лежащие в его основе. Процесс может установить, что определенные свойства сохраняются во всем смоделированном пространстве состояний, в то время как сравнения с реализацией помогают проверить, соответствует ли производственный код этим предположениям.
Предыдущие доказательства уже выявили сбои в XRPL
Этот подход уже выявил крайние случаи, которые обычное тестирование упустило.
Во время разведывательной фазы верификации с февраля по апрель Common Prefix смоделировала части протокола кредитования и определила инварианты, которые система должна была поддерживать.
RippleX сообщила, что работа выявила нарушения инвариантов хранилищ, сбои в утверждениях о платежах по кредитам, ошибки арифметического округления и расхождения между письменными спецификациями XLS и их реализацией.
Выявленные проблемы были впоследствии устранены в версиях xrpld 3.1.3 и 3.2.0.
Этот послужной список придает текущим усилиям по верификации практическую роль до того, как значительный капитал вкладчиков будет размещен за протоколом. Формальные методы могут поставить под сомнение предположения, заложенные в логику кредитования, в то время как разработчики все еще могут изменить реализацию до более широкого принятия.
Проблема становится более сложной по мере того, как нативное кредитование взаимодействует с существующими функциями реестра, включая переводы активов, замораживание и отзыв.
RippleX ранее утверждала, что эта сложность повышает пределы полагания только на функциональные тесты, аудиты, программы вознаграждения за обнаружение ошибок и тестирование валидаторами.
Ставки также становятся коммерческими.
RippleX выделила Evernorth, которая готовится стать зарегистрированной на Nasdaq казначейской компанией XRP, и VS1.Finance среди компаний, готовящихся использовать или строить вокруг Single Asset Vaults и протокола кредитования, что усиливает давление на базовые правила учета, чтобы они вели себя предсказуемо до прихода институционального капитала.
Математические доказательства по-прежнему оставляют кредитный риск за пределами реестра
Даже успешная верификация оставит один из самых больших рисков кредитования XRPL за пределами математической модели: будет ли заемщики погашать кредиты.
Протокол полагается на внесетевой андеррайтинг для определения кредитоспособности заемщика и в настоящее время не зависит от автоматизированных ончейн-механизмов обеспечения и ликвидации, обычно используемых на рынках децентрализованного кредитования.
Кредитные брокеры могут предоставлять капитал первого убытка, предназначенный для покрытия части дефолта до того, как убытки достигнут вкладчиков, но документация XRPL отмечает, что этот механизм не устраняет кредитный риск.
Формальная верификация также не может доказать, что каждая внешняя интеграция, операционный процесс или решение по андеррайтингу будут вести себя безопасно. Ее гарантии распространяются только на свойства, определенные разработчиками, и предположения, представленные в модели.
Это создает два отдельных уровня гарантий для вкладчиков.
Первый — это то, соответствует ли собственный механизм учета XRPL требованиям во время депозитов, кредитования, погашений и снятий средств. Второй — это то, правильно ли кредитные брокеры оценивают и управляют заемщиками, чьи обязательства остаются под реальным кредитным риском.
Работа Common Prefix сосредоточена на усилении первого. Поскольку LendingProtocolV1_1 теперь распространяется в xrpld 3.4.0, валидаторы в конечном итоге определят, станет ли поправка активной.
До этого разработчики пытаются получить более веские доказательства того, что сам механизм кредитования ведет себя в соответствии со спецификациями, когда реальный капитал, кредитные брокеры и внесетевые кредитные решения начнут взаимодействовать с ним.
Всегда имейте в виду, что редакции могут придерживаться предвзятых взглядов в освещении новостей.
Автор – Oluwapelumi Adejumo
