XRP Ledger (XRPL) сүлжээний хөгжүүлэгчид тун удахгүй нэвтрүүлэх зээлийн зах зээл нь хөрөнгөө шавхуулах эсвэл төлбөрийн чадваргүй болох эрсдэлтэй эсэхийг математик баталгаажуулалтын аргаар туршиж байна.
Есдүгээр сарын 17-нд протокол судалгааны Common Prefix пүүс XRPL-ийн Lending Protocol-ийг Lean 4 хэл ашиглан албан ёсоор баталгаажуулж (formal verification) байгаагаа зарласан юм. Lean 4 нь аливаа программ хангамж системд үүсэж болох бүх төлөвт тодорхойлсон математик шинж чанаруудыг хангаж чадаж буй эсэхийг тогтоодог хэл юм. Тус фирмийн мэдээлснээр уг ажлын гол зорилго нь протокол өөрийн бүртгэл болон аюулгүй байдлын дүрмийг зөрчсөн төлөвт орох боломжгүйг харуулахад оршиж байна.
Шинэ шинэчлэл ба хаалттай сангууд
Энэхүү судалгааны ажил нь xrpld 3.4.0 хувилбар гарсны дараа улам чухал ач холбогдолтой болоод байна. Уг хувилбарт хаалттай зээлийн сангууд (closed-ended lending vaults) болон кассын суурьт бүртгэлийг багтаасан LendingProtocolV1_1 нэмэлт өөрчлөлт багтжээ. Энэхүү өөрчлөлт нь серверийн программд орсон хэдий ч хэрэгжиж эхлэхийн тулд XRPL-ийн албан ёсны зөвшөөрлийн процессоор батлагдах шаардлагатай байгаа юм.
XRPL-ийн шинэ загвараар хадгаламж эзэмшигчид хөрөнгөө нэгтгэн төвлөрүүлж, зээлийн зуучлагчид уг хөрөнгийг тогтмол хугацаатай, барьцаагүй зээл болгон олгох боломж бүрдэнэ. Зээлдэгчийг шалгах, зээлжих чадварыг үнэлэх үйл явц блокчэйнээс гадуур (off-chain) явагдах бол зээл олголт, эргэн төлөлт болон санхүүгийн бүртгэлийг дэвтэрт тэмдэглэнэ. Иймээс протоколын дотоод бүртгэл маш нарийн, алдаагүй байх шаардлага тулгарч байна.
Бүртгэлийн алдааны үр дагавар
Хадгаламж эзэмшигчдийн хөрөнгө урьдчилан тодорхойлсон хугацаанд түгжигдэх тул LendingProtocolV1_1 нэмэлт өөрчлөлт нь бүртгэлийн алдаанаас үүдэх хохирлын эрсдэлийг нэмэгдүүлдэг. Хаалттай сангууд нь захиалга хийх, хөрөнгө оруулах, буцаан авах гэсэн гурван үе шаттай. Хөрөнгө оруулалтын шатанд шилжмэгц хөрөнгө нэмэх эсвэл татах үйлдэл бүрэн хаагдаж, зээл олгоход бэлэн болдог бөгөөд буцаан авах үе шат эхлэх хүртэл хүлээгддэг байна.
Мөн 3.4.0 хувилбар нь хүүгийн орлогыг хүлээн зөвшөөрөх аргыг өөрчилж, кассын суурьт бүртгэлийг нэвтрүүлсэн. Ингэснээр зээлдэгч бодит төлбөрөө хийсэн цагт л хүүгийн орлогыг бүртгэх бөгөөд хараахан аваагүй орлогыг сангийн үнэлгээнд тусгах эрсдэлийг бууруулж байна.
Математик загварчлалын онцлог
Судлаачид xrpld-ийн C++ кодыг бүхэлд нь математик аргаар шалгахыг зориогүй байна. Харин холбогдох протоколын логикийг Lean 4 дээр дахин бүтээж, системийн хадгалах ёстой шинж чанаруудыг тодорхойлжээ. Үүний дараа оракл ашиглан математик загвар болон бодит кодыг зэрэг шалгаж, зөрүүтэй ажиллаж буй тохиолдлуудыг илрүүлэх ажлыг гүйцэтгэж байна.
