„Safegcd“ įgyvendinimas oficialiai patvirtintas
Įvadas
Bitcoin ir kitų blokų grandinių, tokių kaip Liquid, saugumas priklauso nuo skaitmeninių parašų algoritmų, tokių kaip ECDSA ir Schnorr parašai, naudojimo. AC biblioteka, vadinama libsecp256k1, pavadinta pagal elipsinę kreivę, kurią biblioteka veikia, naudoja tiek Bitcoin Core, tiek Liquid, kad pateiktų šiuos skaitmeninio parašo algoritmus. Šie algoritmai naudoja matematinį skaičiavimą, vadinamą a modulinis atvirkštiniskuris yra gana brangus skaičiavimo komponentas.
„Greitas pastovaus laiko gcd skaičiavimas ir modulinė inversija“ Daniel J. Bernstein ir Bo-Yin Yang sukuria naują modulinės inversijos algoritmą. 2021 m. šį algoritmą, vadinamą „safegcd“, libsecp256k1 įdiegė Peteris Dettmanas. Atlikdama šio naujojo algoritmo patikros procesą, „Blockstream Research“ pirmoji užbaigė oficialų algoritmo konstrukcijos patikrinimą, naudodama „Coq proof“ asistentą, kad oficialiai patikrintų, ar algoritmas iš tikrųjų baigiasi tinkamu moduliniu atvirkštiniu 256 bitų rezultatu. įvestis.
Atotrūkis tarp algoritmo ir įgyvendinimo
Įforminimo pastangos 2021 m. tik parodė, kad Bernsteino ir Yango sukurtas algoritmas veikia tinkamai. Tačiau norint naudoti šį algoritmą libsecp256k1, reikia įdiegti matematinį safegcd algoritmo aprašymą C programavimo kalba. Pavyzdžiui, matematinis algoritmo aprašymas atlieka vektorių, kurių plotis gali siekti 256 bitų ženklų sveikuosius skaičius, matricos dauginimą, tačiau C programavimo kalba natūraliai pateiks sveikuosius skaičius iki 64 bitų (arba 128 bitų su kai kuriais kalbos plėtiniais).
Norint įgyvendinti „saegcd“ algoritmą, reikia užprogramuoti matricos daugybą ir kitus skaičiavimus naudojant C 64 bitų sveikuosius skaičius. Be to, buvo pridėta daug kitų optimizacijų, kad diegimas būtų greitas. Galų gale, yra keturi atskiri safegcd algoritmo diegimai libsecp256k1: du pastovaus laiko algoritmai parašams generuoti, vienas optimizuotas 32 bitų sistemoms ir vienas optimizuotas 64 bitų sistemoms ir du kintamo laiko algoritmai parašo tikrinimui. vienas skirtas 32 bitų sistemoms ir vienas 64 bitų sistemoms.
Patikrinama C
Norint patikrinti, ar C kodas tinkamai įgyvendina safegcd algoritmą, reikia patikrinti visą įgyvendinimo informaciją. Mes naudojame Verifiable C, patvirtintos programinės įrangos įrankių grandinės dalį, norėdami samprotauti apie C kodą, naudodami Coq teoremos tikrintuvą.
Tikrinimas vyksta nurodant išankstines ir posąlygas naudojant atskyrimo logiką kiekvienai tikrinamai funkcijai. Atskyrimo logika yra logika, skirta samprotauti apie paprogrames, atminties paskirstymą, lygiagretumą ir kt.
Kai kiekvienai funkcijai suteikiama specifikacija, tikrinama pradedant nuo funkcijos išankstinės sąlygos ir po kiekvieno funkcijos teksto teiginio sukuriamas naujas invariantas, kol galiausiai nustatoma post sąlyga funkcijos korpuso pabaigoje arba kiekvienos funkcijos pabaigoje. grąžinimo pareiškimas. Didžioji dalis formalizavimo pastangų praleidžiama „tarp“ kodo eilučių, naudojant invariantus, kad kiekvienos C išraiškos neapdorotos operacijos būtų išverstos į aukštesnio lygio teiginius apie tai, ką matematiškai reprezentuoja manipuliuojamos duomenų struktūros. Pavyzdžiui, tai, ką C kalba laiko 64 bitų sveikųjų skaičių masyvu, iš tikrųjų gali būti 256 bitų sveikojo skaičiaus atvaizdas.
Galutinis rezultatas yra oficialus įrodymas, patvirtintas Coq proof asistento, kad libsecp256k1 64 bitų kintamo laiko safegcd modulinio atvirkštinio algoritmo įgyvendinimas yra funkcionaliai teisingas.
Patikrinimo apribojimai
Funkcinio teisingumo įrodymas turi tam tikrų apribojimų. Atskyrimo logika, naudojama Verifiable C, įgyvendina tai, kas žinoma kaip dalinis teisingumas. Tai reiškia, kad tai tik įrodo, kad C kodas grįžta su teisingu rezultatu jeigu jis grįžta, bet tai neįrodo paties nutraukimo. Sušvelniname šį apribojimą naudodami ankstesnį Coq saugescd algoritmo ribų įrodymą, kad įrodytume, kad pagrindinės kilpos ciklo skaitiklio vertė iš tikrųjų niekada neviršija 11 iteracijų.
Kita problema yra ta, kad pati C kalba neturi formalių specifikacijų. Vietoje to Verifiable C projektas naudoja CompCert kompiliatoriaus projektą, kad pateiktų oficialią C kalbos specifikaciją. Tai garantuoja, kad su CompCert kompiliatoriumi sukompiliavus patikrintą C programą, gautas surinkimo kodas atitiks jo specifikaciją (atsižvelgiant į pirmiau nurodytus apribojimus). Tačiau tai negarantuoja, kad GCC, clang ar bet kurio kito kompiliatoriaus sugeneruotas kodas būtinai veiks. Pavyzdžiui, C kompiliatoriams funkcijos iškvietime leidžiama turėti skirtingas argumentų vertinimo eiles. Ir net jei C kalba turėtų oficialią specifikaciją, bet kuris kompiliatorius, kuris pats nėra oficialiai patikrintas, vis tiek galėtų neteisingai kompiliuoti programas. Tai pasitaiko praktikoje.
Galiausiai, Verifiable C nepalaiko praeinančių struktūrų, struktūrų grąžinimo ar struktūrų priskyrimo. Nors libsecp256k1 struktūros visada perduodamos rodykle (tai leidžiama Verifiable C), yra keletas atvejų, kai naudojamas struktūros priskyrimas. Moduliniam atvirkštinio teisingumo įrodymui buvo 3 priskyrimai, kurie turėjo būti pakeisti specializuotu funkcijos iškvietimu, kuris atlieka struktūros priskyrimą pagal lauką.
Santrauka
„Blockstream Research“ oficialiai patvirtino libsecp256k1 modulinės atvirkštinės funkcijos teisingumą. Šis darbas suteikia papildomų įrodymų, kad praktiškai įmanoma patikrinti C kodą. Naudodami bendrosios paskirties įrodymo asistentą galime patikrinti programinę įrangą, sukurtą remiantis sudėtingais matematiniais argumentais.
Niekas netrukdo patikrinti ir kitų libsecp256k1 įdiegtų funkcijų. Taigi libsecp256k1 gali gauti didžiausias įmanomas programinės įrangos teisingumo garantijas.
Tai Russello O'Connor ir Andrew Poelstra svečių įrašas. Išsakytos nuomonės yra visiškai jų pačių ir nebūtinai atspindi BTC Inc arba Bitcoin Magazine nuomonę.