Penyelidik dari Institut Penyelidikan Informatik dan Automasi Negeri (INRIA), Microsoft Research dan Carnegie Mellon University dibentangkan edisi percubaan pertama perpustakaan kripto EverCrypt dikembangkan dalam kerangka projek Everest dan menggunakan kaedah matematik pengesahan kebolehpercayaan formal.
Untuk keupayaan dan prestasinya, EverCrypt sangat dekat dengan perpustakaan crypto yang ada (OpenSSL) tetapi itu, tidak seperti mereka, menawarkan jaminan kebolehpercayaan dan keselamatan tambahan.
Contohnya proses pengesahan bermula untuk menentukan spesifikasi terperinci yang menggambarkan semua tingkah laku program dan bukti matematik bahawa kod bertulis memenuhi spesifikasi yang disediakan.
Tidak seperti kaedah kawalan kualiti berdasarkan bukti, pengesahan memberikan jaminan yang boleh dipercayai bahawa program akan berjalan hanya seperti yang diharapkan oleh pembangun dan tidak ada jenis kesalahan tertentu.
Contohnya, pematuhan dengan spesifikasi memastikan kerja yang selamat dengan memori dan tidak adanya kesalahan yang menyebabkan buffer overflow, ke dereference pointers, untuk mengakses ke kawasan memori yang sudah dibebaskan, atau untuk membebaskan dua kali blok memori.
Apa itu EverCrypt?
EverCrypt menyediakan pemeriksaan jenis dan nilai yang mantap- Komponen tidak akan melewati parameter ke komponen lain yang tidak patuh dan tidak akan mendapat akses ke keadaan dalaman komponen lain.
Kelakuan input / output sepenuhnya mematuhi tindakan fungsi matematik sederhana, yang ditakrifkan dalam piawaian kriptografi.
Untuk melindungi daripada serangan di saluran pihak ketiga, tingkah laku semasa pengiraan (misalnya, jangka masa pelaksanaan atau kehadiran akses ke memori tertentu) ia tidak bergantung pada data rahsia yang diproses.
Kod projek ditulis dalam bahasa fungsional F * (Bintang F) , yang menyediakan sistem jenis dan penyempurnaan yang bergantung, yang memungkinkan untuk menetapkan spesifikasi yang tepat (model matematik) untuk program-program dan untuk menjamin kebenaran dan ketiadaan kesalahan dalam pelaksanaannya dengan formula SMT dan alat ujian tambahan.
Kod di F * diedarkan di bawah lesen Apache 2.0, dan modul terakhir di C dan assembler di bawah lesen MIT.
Berdasarkan kod rujukan F *, assembler, C, OCaml, JavaScript dihasilkan dan kod pemasangan web.
Beberapa bahagian kod disediakan oleh projek tersebut sudah digunakan dalam Firefox, kernel Windows , blockchain dari Wireguard Tezos dan VPN.
Komponen EverCrypt
Pada asasnya, EverCrypt menggabungkan dua projek yang sebelumnya berbeza dari HACL * dan Vale, menyediakan API bersatu berdasarkan mereka dan menjadikannya sesuai untuk digunakan dalam projek sebenar.
HACL * ditulis dalam Bahasa Rendah* dan tujuannya adalah untuk menyediakan primitif kriptografi untuk digunakan dalam program C yang mereka menggunakan API gaya libsodium dan NaCL.
Projek itu Vale mengembangkan bahasa tertentu domain untuk membuat pengesahan dalam assembler.
Lebih kurang 110 ribu baris kod HACL * dalam bahasa Low * dan 25 ribu baris kod untuk Vale digabungkan dan mereka ditulis semula dalam sekitar 70 ribu baris kod dalam bahasa universal F *, yang juga sedang dikembangkan sebagai sebahagian daripada projek Everest.
Versi pertama perpustakaan EverCrypt ciri pelaksanaan yang disahkan daripada algoritma kriptografi berikut dicadangkan dalam versi C atau assembler (semasa menggunakan.
Daripada jumlah ini, berikut menonjol di halaman projek:
- Algoritma Hash: semua varian SHA2, SHA3, SHA1, dan MD5
- Kod pengesahan: HMAC over SHA1, SHA2-256, SHA2-384, dan SHA2-512 untuk pengesahan sumber data
- Algoritma Penjanaan Kunci HKDF (Ekstrak Berasaskan HMAC dan Kembangkan Fungsi Derivasi Kunci)
- Penyulitan aliran ChaCha20 (tersedia versi C yang tidak dioptimumkan)
- Algoritma Pengesahan Mesej Poly1305 (MAC) (versi C dan assembler)
- Protokol Diffie-Hellman pada kurva elips Curve25519 (versi C dan assembler dengan pengoptimuman berdasarkan petunjuk BMI2 dan ADX)
- Blok mod cipher AEAD (cipher yang disahkan) ChachaPoly (versi C tidak dioptimumkan)
- Mod penyulitan blok AEAD AES-GCM (versi assembler dengan pengoptimuman AES-NI).
Yang pertama versi alpha, pengesahan kod telah selesai sebahagian besarnya, tetapi masih terdapat beberapa kawasan yang belum ditemui.
Selain itu, API belum stabil, yang akan diperluas dalam versi alpha berikut (Ia dirancang untuk menyatukan struktur untuk semua API.
Di antara kekurangan, sokongan untuk seni bina x86_64 juga diserlahkan (pada peringkat pertama, tujuan utamanya adalah kebolehpercayaan, sementara pengoptimuman dan platform akan dilaksanakan di tempat kedua).
Fuente: https://jonathan.protzenko.fr