Pētnieki no Valsts Informātikas un automatizācijas pētījumu institūts (INRIA), Iepazīstināja ar Microsoft pētījumu un Karnegi Melona universitāti gada pirmais izmēģinājuma izdevums kriptogrāfijas bibliotēka EverCrypt izstrādāts Everest projekta ietvaros un izmantojot formālas uzticamības pārbaudes matemātiskās metodes.
Par savām spējām un veiktspēju EverCrypt ir ļoti tuvu esošajām kripto bibliotēkām (OpenSSL), bet tas atšķirībā no tiem piedāvā papildu uzticamības un drošības garantijas.
Piemēram verifikācijas process nosaka detalizētu specifikāciju noteikšanu kas apraksta visu programmas uzvedību un matemātiskais pierādījums, ka uzrakstītais kods atbilst sagatavotajām specifikācijām.
Atšķirībā no uz pierādījumiem balstītām kvalitātes kontroles metodēm pārbaude nodrošina uzticamas garantijas ka programma darbosies tikai tā, kā to ir paredzējuši izstrādātāji, un nav īpašu kļūdu veidu.
Piemēram, atbilstība specifikācijai garantē drošu darbu ar atmiņu un tādu kļūdu neesamību, kas noved pie bufera pārpildes, uz novirzīšanas norādēm, piekļuvi jau atbrīvotām atmiņas zonām vai divkāršu atmiņas bloku atbrīvošanu.
Kas ir EverCrypt?
EverCrypt nodrošina precīzu veida un vērtības pārbaudi- Komponents nekad nenodos parametrus citam neatbilstošam komponentam un neiegūs piekļuvi pārējo komponentu iekšējiem stāvokļiem.
Ievades / izvades uzvedība pilnībā atbilst vienkāršām matemātikas funkciju darbībām, kas ir definēti kriptogrāfijas standartos.
Lai pasargātu no uzbrukumiem trešo pušu kanālos, uzvedība aprēķinu laikā (piemēram, izpildes ilgums vai piekļuve noteiktai atmiņai) tas nav atkarīgs no slepenajiem datiem, kas tiek apstrādāti.
Projekta kods ir rakstīts funkcionālajā valodā F * (F zvaigzne) , kas nodrošina atkarīgo tipu un precizējumu sistēmu, kas ļauj noteikt precīzas programmu specifikācijas (matemātisko modeli) un garantēt pareizību un kļūdu trūkumu ieviešanā, izmantojot SMT formulas un papildu testēšanas rīkus.
F * kods tiek izplatīts ar Apache 2.0 licenci, bet pēdējie moduļi - C un montētājs - ar MIT licenci.
Pamatojoties uz atsauces kodu F *, tiek ģenerēts montētājs, C, OCaml, JavaScript un tīmekļa montāžas kodu.
Dažas koda daļas sagatavots jau tiek izmantoti Firefox, Windows kodolā , bloka ķēde Tezos un VPN Wireguard.
EverCrypt komponenti
Būtībā, EverCrypt apvieno divus iepriekš atšķirīgus projektus no HACL * un Vale, nodrošinot uz tiem balstītu vienotu API un padarot tos piemērotus lietošanai reālos projektos.
HACL * ir rakstīts zemā valodā* un tā mērķis ir nodrošināt kriptogrāfijas primitīvus lietošanai C programmās, kas viņi izmanto libsodium un NaCL stila API.
Projekts Vale izstrādāja noteiktu valodu domēnu, lai izveidotu verifikācijas montētājā.
Ir apvienoti aptuveni 110 tūkstoši HACL * koda rindiņu Low * valodā un 25 tūkstoši Vale koda rindiņu un tie tiek pārrakstīti aptuveni 70 tūkstošos koda rindiņu universālajā valodā F *, kas arī tiek izstrādāta Everest projekta ietvaros.
Pirmā EverCrypt bibliotēkas versija iezīmes pārbaudītas ieviešanas no šādiem kriptogrāfijas algoritmiem ierosināts C vai montētāja versijās (lietojot.
No tiem projekta lapā izceļas:
- Hash algoritmi: visi SHA2, SHA3, SHA1 un MD5 varianti
- Autentifikācijas kodi: HMAC pār SHA1, SHA2-256, SHA2-384 un SHA2-512 datu avota autentifikācijai
- HKDF atslēgu ģenerēšanas algoritms (paplašināšanas un ekstrakcijas atslēgu atvasināšanas funkcija, kuras pamatā ir HMAC)
- ChaCha20 straumes šifrēšana (pieejama neoptimizēta C versija)
- Poly1305 ziņojumu autentifikācijas algoritms (MAC) (C un montētāja versija)
- Diffie-Hellman protokols uz eliptiskām līknēm Curve25519 (C un montētāja versijas ar optimizāciju, pamatojoties uz BMI2 un ADX instrukcijām)
- Bloķēt šifra režīmu AEAD (autentificēts šifrs) ChachaPoly (C versija nav optimizēta)
- AEAD AES-GCM bloku šifrēšanas režīms (montētāja versija ar AES-NI optimizācijām).
Pirmajā alfa versija, koda pārbaude jau ir pabeigta lielā mērā, bet joprojām ir dažas jomas, kas nav atklātas.
Turklāt, API vēl nav stabilizēta, kas tiks paplašināts šādās alfa versijās (Plānots vienot visu API struktūras.
Starp trūkumiem tiek izcelts arī atbalsts x86_64 arhitektūrai (pirmajā posmā galvenais mērķis ir uzticamība, savukārt otrajā vietā tiks ieviesta optimizācija un platformas).
Fuente: https://jonathan.protzenko.fr