Teadlased Riiklik informaatika ja automatiseerimise uurimisinstituut (INRIA), Esitati Microsofti uurimistöö ja Carnegie Melloni ülikool aasta esimene prooviversioon krüptoteek EverCrypt välja töötatud Everesti projekti raames ja kasutades ametliku usaldusväärsuse kontrollimise matemaatilisi meetodeid.
Oma võimete ja jõudluse EverCrypt on olemasolevatele krüptoteekudele väga lähedal (OpenSSL), kuid see pakub erinevalt neist täiendavaid usaldusväärsuse ja turvalisuse tagatisi.
Nt taatlusprotsess taandub üksikasjalike spetsifikatsioonide määratlemisele mis kirjeldavad kogu programmi käitumist ja matemaatiline tõestus, et kirjutatud kood vastab ettevalmistatud spetsifikatsioonidele.
Erinevalt tõenduspõhistest kvaliteedikontrollimeetoditest kontrollimine annab usaldusväärsed garantiid et programm töötab ainult nii, nagu arendajad on ette näinud, ja puuduvad konkreetsed klassid vigu.
Näiteks vastavus spetsifikatsioonile tagab turvalise töö mäluga ja puhvri ületäitumiseni viivate vigade puudumise, kõrvalekallekutele, juurdepääsule juba vabanenud mälupiirkondadele või mäluplokide kahekordsele vabastamisele.
Mis on EverCrypt?
EverCrypt pakub tugevat tüübi ja väärtuse kontrollimist- Komponent ei edasta parameetreid kunagi teisele nõuetele mittevastavale komponendile ega pääse teiste komponentide sisemisele olekule.
Sisendi / väljundi käitumine vastab täielikult lihtsatele matemaatikafunktsioonide toimingutele, mis on määratletud krüptograafilistes standardites.
Rünnakute eest kaitsmiseks kolmandate osapoolte kanalites, käitumine arvutuste ajal (näiteks täitmise kestus või juurdepääs teatud mälule) see ei sõltu töödeldavatest salajastest andmetest.
Projekti kood on kirjutatud funktsionaalses keeles F * (F täht) , mis pakub sõltuvate tüüpide ja täpsustuste süsteemi, mis võimaldavad kehtestada programmidele täpsed spetsifikatsioonid (matemaatiline mudel) ning tagada SMT-valemite ja abikatse tööriistade abil rakendamise õigsuse ja vigade puudumise.
F * -is olevat koodi levitatakse Apache 2.0 litsentsi all, lõplikud moodulid C-s ja monteerija MIT-litsentsi all.
Tuginedes viitenumbrile F *, assembler, C, OCaml, JavaScript on loodud ja veebikomplekti kood.
Mõned koodi osad ettevalmistatud projekti juba kasutatakse Windowsi kernelis Firefoxis , plokiahel Tezos ja VPN Wireguard.
EverCrypti komponendid
Sisuliselt, EverCrypt ühendab kaks varem HACL * ja Vale projektist erinevat projekti, pakkudes nende põhjal ühtse API ja muutes need reaalsetes projektides kasutamiseks sobivaks.
HACL * on kirjutatud madala keeles* ja selle eesmärk on pakkuda krüptograafilisi primitiive kasutamiseks C-programmides, mis nad kasutavad libsodium ja NaCL stiilis API-sid.
El proyecto Vale töötas välja kindla keele domeen, et luua monteerijas kontrollimisi.
Kombineeritakse umbes 110 tuhat rida HACL * koodi Low * keeles ja 25 tuhat Vale koodi rida ja need kirjutatakse ümber umbes 70 tuhandes koodireas universaalses keeles F *, mida samuti arendatakse projekti Everest raames.
EverCrypti teegi esimene versioon funktsioonid kontrollitud rakendused järgmistest krüptograafilistest algoritmidest pakutakse C - või assembleri versioonides (.
Neist paistavad projekti lehel silma järgmised:
- Hash-algoritmid: SHA2, SHA3, SHA1 ja MD5 kõik variandid
- Autentimiskoodid: andmeallika autentimiseks HMAC üle SHA1, SHA2-256, SHA2-384 ja SHA2-512
- HKDF-i võtmete genereerimise algoritm (HMAC-põhine ekstraktimis- ja laiendusvõtmete tuletamisfunktsioon)
- ChaCha20 voo krüptimine (saadaval pole optimeeritud C-versiooni)
- Poly1305 sõnumi autentimise algoritm (MAC) (C ja assembleri versioon)
- Diffie-Hellmani protokoll elliptilistel kõveratel Curve25519 (C ja assembleri versioonid koos optimeerimisega BMI2 ja ADX juhiste alusel)
- Blokeeri krüptimisrežiim AEAD (autentitud krüptimine) ChachaPoly (versioon C pole optimeeritud)
- AEAD AES-GCM plokkkrüptimisrežiim (assamblee versioon koos AES-NI optimeerimisega).
Esimesel alfaversioon, koodi kontrollimine on juba lõpule viidud suures osas, kuid siiski on mõned valdkonnad katmata.
Lisaks API pole veel stabiliseerunud, mida laiendatakse järgmistes alfaversioonides (Kavas on kõigi API-de struktuurid ühtlustada.
Puuduste hulgas tuuakse välja ka x86_64 arhitektuuri tugi (esimeses etapis on peamine eesmärk töökindlus, teiseks rakendatakse optimeerimist ja platvorme).
allikas: https://jonathan.protzenko.fr