XRPL bando matematiškai įrodyti, kad jos naujoji skolinimo rinka negali būti nusausinta
XRP Ledger (XRPL) kūrėjai naudoja matematinius įrodymus, kad patikrintų, ar būsima tinklo skolinimo rinka gali išsekti ar tapti nemokia.
Rugsėjo 17 d. protokolų tyrimų įmonė „Common Prefix“ pranešė oficialiai tikrinanti XRPL skolinimo protokolą „Lean 4“ – teoremų patvirtinimo kalba, skirta nustatyti, ar programinė įranga atitinka nustatytas matematines savybes visose galimose sistemos būsenose.
Įmonė teigė, kad darbu siekiama parodyti, kad protokolas negali patekti į valstybes, kurios pažeidžia jos apskaitos ir saugos taisykles.
Po to darbas įgavo didesnę reikšmę xrpld 3.4.0 versija buvo išsiųsta šią savaitę kartu su LendingProtocolV1_1, pakeitimu, kuris įveda uždarojo tipo skolinimo saugyklas ir grynųjų pinigų apskaitą. Pakeitimas įtrauktas į serverio programinę įrangą, tačiau prieš įsigaliojant jį vis tiek reikia patvirtinti per XRP Ledger pakeitimų procesą.
XRPL skolinimo dizainas leistų indėlininkams sutelkti turtą, kurį paskolų brokeriai gali panaudoti į terminuotas paskolas be užstato. Paskolos gavėjo pasirašymas ir kredito vertinimas vyksta ne grandinėje, o knygoje registruojamas paskolos suteikimas, grąžinimas ir apskaita.
Tai padidina protokolo vidinės apskaitos vedimą. Klaidos, susijusios su saugyklos likučiais, paskolų mokėjimais ar akcijų skaičiavimais, gali turėti įtakos sutelktoms indėlininkų lėšoms, o ne atskirai programai.
Užblokuotas kapitalas padidina XRPL skolinimo akcijas
Skolinimo protokolasV1_1 padidina apskaitos nesėkmių pasekmes, nes indėlininko turtas gali likti įsipareigojęs per iš anksto nustatytą investavimo laikotarpį.
Uždarojo tipo saugyklos vyksta trimis etapais: prenumerata, investavimas ir išpirkimas. Indėlininkai gali pridėti arba atsiimti turtą pasirašymo etapo metu, tačiau abu veiksmai blokuojami, kai saugykla pradeda investuoti ir kapitalas tampa prieinamas skolinimui. Išėmimai atnaujinami, kai saugykla pasiekia išpirkimo terminą.
Tvarkaraštis nustatomas sukūrus saugyklą ir vėliau jo keisti negalima, todėl dalyviai iš anksto mato, kiek laiko gali likti įsipareigojęs kapitalas.
3.4.0 versija taip pat keičia tai, kaip naujos saugyklos pripažįsta palūkanų pajamas.
Pagal ankstesnį modelį numatytos palūkanos galėjo būti įtrauktos į pajamas, kai buvo suteikta paskola, net prieš skolininkui sumokėjus tuos mokėjimus. Grynųjų pinigų apskaitoje palūkanos pripažįstamos tik tada, kai gaunami mokėjimai, todėl sumažėja rizika, kad saugyklos akcijų vertės atspindės dar negautas pajamas.
Šie pakeitimai prideda daugiau būsenų ir perėjimų, kurie turi išlikti nuoseklūs, kai priimami indėliai, išduodamos paskolos, grąžinami pinigai, skolininkai nevykdo įsipareigojimų, o saugyklos ilgainiui vėl atidaromos išėmimui.
Bendrasis priešdėlis naudoja formalų patikrinimą, kad išbandytų tuos ryšius, nei scenarijus, kurių inžinieriai gali numatyti naudodami įprastą bandymų rinkinį.
Tyrėjai nesistengia matematiškai patikrinti viso xrpld C++ kodų bazė. Vietoj to jie atkuria atitinkamą Lean 4 protokolo logiką ir apibrėžia savybes, kurias turėtų išsaugoti sistema.
Tada orakulas gali paleisti lygiavertes įvestis pagal matematinį modelį ir gamybos įgyvendinimą, padėdamas nustatyti atvejus, kai jie elgiasi skirtingai.
Šis skirtumas yra svarbus, nes matematinis įrodymas yra tiek stiprus, kiek yra modelis ir jo prielaidos. Procesas gali nustatyti, kad apibrėžtos savybės galioja visoje modeliuojamoje būsenos erdvėje, o palyginimas su įgyvendinimu padeda patikrinti, ar gamybos kodas ir toliau atitinka šias prielaidas.
Ankstesni įrodymai jau atskleidė XRPL gedimus
Šis metodas jau atskleidė kraštutinius atvejus, kurių įprastiniai bandymai praleido.
Per tiriamąjį tikrinimo etapą nuo vasario iki balandžio mėn. Bendrasis prefiksas sumodeliavo skolinimo protokolo dalis ir apibrėžė invariantus, kuriuos sistema turėtų išlaikyti.
„RippleX“ teigė, kad šis darbas atskleidė kintamus saugyklos pažeidimus, paskolos mokėjimo patvirtinimo klaidas, aritmetines apvalinimo klaidas ir skirtumus tarp rašytinių XLS specifikacijų ir jų įgyvendinimo.
Vėliau nustatytos problemos buvo sprendžiamos xrpld 3.1.3 ir 3.2.0 versijos.
Šis įrašas suteikia dabartinėms patikros pastangoms praktinį vaidmenį prieš įtraukiant didelį indėlininko kapitalą į protokolą. Formalūs metodai gali nuginčyti prielaidas, įtvirtintas skolinimo logikoje, o kūrėjai vis tiek gali pakeisti įgyvendinimą, kol nebus pritaikyti plačiau.
Problema tampa sudėtingesnė, nes vietinis skolinimas sąveikauja su esamomis knygos funkcijomis, įskaitant turto perkėlimą, įšaldymą ir susigrąžinimą. Kiekviena papildoma sąveika padidina sistemos būsenų, į kurias kūrėjai turi atsižvelgti, skaičių.
„RippleX“ anksčiau teigė, kad šis sudėtingumas padidina ribas pasikliauti tik funkciniais testais, auditais, klaidų kompensacijomis ir patvirtinimo testais.
Stalai taip pat tampa komerciniai.
„RippleX“ nustatė, kad „Evernorth“, kuri ruošiasi tapti „Nasdaq“ listinguojama XRP iždo bendrove, ir „VS1.Finance“ yra tarp įmonių, besiruošiančių naudoti arba kurti pagal „Single Asset Vaults“ ir skolinimo protokolą, todėl pagrindinėms apskaitos taisyklėms daromas didesnis spaudimas, kad jos elgtųsi nuspėjamai prieš atvykstant instituciniam kapitalui.
Matematiniai įrodymai vis tiek palieka kredito riziką už knygos ribų
Netgi sėkmingas patikrinimas paliktų vieną didžiausių XRPL skolinimo rizikų už matematinio modelio ribų: ar skolininkai grąžins.
Protokolas remiasi ne grandine, kad būtų nustatytas skolininko kreditingumas, ir šiuo metu nepriklauso nuo automatizuoto užstato grandinėje ir likvidavimo mechanizmų, dažniausiai naudojamų decentralizuotose skolinimo rinkose.
Paskolų brokeriai gali pateikti pirmojo nuostolio kapitalą, skirtą padengti dalį įsipareigojimų neįvykdymo, kol nuostoliai pasiekia indėlininkus, tačiau XRPL dokumentuose pažymima, kad šis mechanizmas nepašalina kredito rizikos.
Oficialus patikrinimas taip pat negali įrodyti, kad kiekvienas išorinis integravimas, veiklos procesas ar garantinis sprendimas elgsis saugiai. Jo garantijos taikomos tik toms savybėms, kurias apibrėžia kūrėjai, ir prielaidoms, pateiktoms modelyje.
Tai sukuria du atskirus indėlininkų užtikrinimo sluoksnius.
Pirma, ar XRPL apskaitos mechanizmai nuosekliai elgiasi indėlių, skolinimo, grąžinimo ir išėmimo metu. Antra, ar paskolų brokeriai teisingai nustato ir valdo skolininkus, kurių įsipareigojimai išlieka realiai rizikingi.
Bendrojo prefikso darbas yra orientuotas į pirmojo stiprinimą. Su LendingProtocolV1_1 dabar platinama xrpld 3.4.0, tikrintojai galiausiai nustatys, ar pakeitimas bus aktyvus.
Prieš tai įvyksta, kūrėjai bando nustatyti tvirtesnius įrodymus, kad pati skolinimo mašina elgiasi taip, kaip nurodyta, kai su ja pradeda sąveikauti tikrasis kapitalas, paskolų brokeriai ir negrandiniai kredito sprendimai.
