Peneliti saka Institut Riset Informatika lan Otomasi Negara (INRIA), Microsoft Research lan Universitas Carnegie Mellon ditampilake edisi sidhang kaping pisanan saka perpustakaan crypto EverCrypt dikembangake ing framework proyek Everest lan nggunakake metode matematika verifikasi linuwih resmi.
Kanggo kapabilitas lan kinerja, EverCrypt cedhak banget karo perpustakaan crypto sing ana (OpenSSL) nanging ora beda karo dheweke, menehi jaminan tambahan linuwih lan keamanan.
Contone, proses verifikasi diwiwiti kanggo nemtokake spesifikasi rinci sing nggambarake kabeh tindak tanduk program lan bukti matematika manawa kode tinulis memenuhi spesifikasi sing wis disiapake.
Beda karo cara kontrol kualitas adhedhasar bukti, verifikasi nyedhiyakake jaminan sing bisa dipercaya program kasebut bakal mbukak kaya sing dienggo para pangembang lan ora ana kelas kesalahan tartamtu.
Contone, tundhuk karo spesifikasi njamin karya sing aman kanthi memori lan ora ana kesalahan sing nyebabake buffer kebanjiran, kanggo nuduhake petunjuk, kanggo ngakses area memori sing wis dibebasake, utawa kanggo mbebasake blok memori kaping pindho.
Apa EverCrypt?
EverCrypt nyedhiyakake jinis lan pamriksa nilai sing kuat- Komponen ora bakal ngliwati paramèter menyang komponen sing ora cocog liyane lan ora bakal entuk akses menyang negara bagian internal komponen liyane.
Prilaku input / output salaras karo tumindak fungsi matematika sing gampang, sing ditemtokake ing standar kriptografi.
Kanggo nglindhungi serangan ing saluran pihak katelu, prilaku sajrone petungan (contone, durasi eksekusi utawa ana akses menyang memori tartamtu) ora gumantung karo data rahasia sing diproses.
Kode proyek ditulis nganggo basa fungsional F * (F bintang) , sing nyedhiyakake sistem jinis gumantung lan perbaikan, sing ngidini nggawe spesifikasi sing tepat (model matematika) kanggo program lan kanggo njamin bener lan ora ana kesalahan implementasine kanthi nggunakake formula SMT lan alat uji bantu tambahan.
Kode ing F * disebarake ing sangisore lisensi Apache 2.0, lan modul pungkasan ing C lan assembler kanthi lisensi MIT.
Adhedhasar kode referensi F *, assembler, C, OCaml, JavaScript digawe lan kode kumpulan web.
Sawetara bagean kode disiapake dening proyek kasebut wis digunakake ing Firefox, kernel Windows , pamblokiran saka Tezos lan VPN Wireguard.
Komponen EverCrypt
Intine, EverCrypt nggabungake rong proyek sing sadurunge beda-beda saka HACL * lan Vale, nyediakake API gabungan adhedhasar lan nggawe dheweke cocog digunakake ing proyek nyata.
HACL * ditulis ing Low* lan tujuane yaiku nyedhiyakake primitif kriptografi kanggo digunakake ing program C sing padha nggunakake API gaya libsodium lan NaCL.
Proyek kasebut Vale ngembangake basa tartamtu domain kanggo nggawe verifikasi ing assembler.
Udakara 110 ewu baris kode HACL * nganggo basa Low * lan 25 ewu baris kode kanggo Vale digabungake lan ditulis maneh udakara 70 ewu baris kode ing basa universal F *, sing uga dikembangake minangka bagean saka proyek Everest.
Versi kapisan perpustakaan EverCrypt fitur implementasi sing wis diverifikasi saka algoritma kriptografi ing ngisor iki diusulake ing versi C utawa assembler (nalika nggunakake.
Iki, ing ngisor iki katon ing kaca proyek:
- Algoritma Hash: kabeh varian SHA2, SHA3, SHA1, lan MD5
- Kode otentikasi: HMAC liwat SHA1, SHA2-256, SHA2-384 lan SHA2-512 kanggo otentikasi sumber data
- Algoritma Generasi Kunci HKDF (Fungsi Derivasi Tombol Ekspansi lan Ekstraksi adhedhasar HMAC)
- Enkripsi stream ChaCha20 (kasedhiya versi C sing ora dioptimalake)
- Algoritma Otentikasi Pesen Poly1305 (MAC) (versi C lan assembler)
- Protokol Diffie-Hellman ing kurva eliptik Curve25519 (versi C lan assembler kanthi optimisasi adhedhasar pandhuan BMI2 lan ADX)
- Blokir mode enkripsi AEAD (enkripsi otentikasi) ChachaPoly (versi C ora dioptimalake)
- Mode enkripsi blok AEAD AES-GCM (versi assembler kanthi optimisasi AES-NI).
Ing kawitan versi alpha, verifikasi kode wis rampung umume, nanging isih ana sawetara wilayah sing ora ditemokake.
Uga, API durung stabil, sing bakal ditambahi ing versi alpha ing ngisor iki (Rencanane nggabungake struktur kanggo kabeh API.
Antarane cacat, dhukungan kanggo arsitektur x86_64 uga disorot (ing tahap kaping pisanan, target utama yaiku reliabilitas, nalika optimasi lan platform bakal diterapake ing urutan nomer loro).
sumber: https://jonathan.protzenko.fr
Dadi pisanan komentar