Araştırmacılar Devlet Bilişim ve Otomasyon Araştırma Enstitüsü (INRIA), Microsoft Research ve Carnegie Mellon University sunuldu ilk deneme sürümü EverCrypt kripto kitaplığı Everest projesi çerçevesinde ve matematiksel yöntemlerle biçimsel güvenilirlik doğrulaması kullanılarak geliştirilmiştir.
Yetenekleri ve performansı için, EverCrypt, mevcut kripto kitaplıklarına çok yakın (OpenSSL) ancak bu, onlardan farklı olarak, ek güvenilirlik ve güvenlik garantisi sunar.
Örnek doğrulama süreci, ayrıntılı spesifikasyonların tanımlanmasına indirgenir programın tüm davranışlarını açıklayan ve yazılı kodun matematiksel kanıtı hazırlanan spesifikasyonları karşılar.
Kanıta dayalı kalite kontrol yöntemlerinden farklı olarak, doğrulama güvenilir garantiler sağlar programın yalnızca geliştiricilerin amaçladığı şekilde çalışacağını ve belirli bir hata sınıfının olmadığını.
Örneğin, spesifikasyona uygunluk bellekle güvenli çalışmayı ve arabellek taşmasına neden olan hataların olmamasını sağlar, işaretçilerin referansını kaldırmak, halihazırda serbest kalmış bellek alanlarına erişmek veya bellek bloklarını iki katına çıkarmak için.
EverCrypt nedir?
EverCrypt sağlam tip ve değer kontrolü sağlar- Bir bileşen, parametreleri diğer uygun olmayan bileşene asla iletmez ve diğer bileşenlerin dahili durumlarına erişim sağlamaz.
Girdi / çıktı davranışı basit matematik fonksiyon eylemlerine tamamen uygundur, kriptografik standartlarda tanımlanan.
Saldırılara karşı korumak için üçüncü taraf kanallarda, hesaplamalar sırasında davranış (örneğin, yürütme süresi veya belirli belleğe erişimlerin varlığı) işlenen gizli verilere bağlı değildir.
Proje kodu F * fonksiyonel dilinde yazılmıştır (F yıldızı) , bağımlı türler ve iyileştirmelerden oluşan bir sistem sağlayanSMT formülleri ve yardımcı test araçları ile programlar için kesin spesifikasyonların (matematiksel model) oluşturulmasına ve uygulamadaki hataların doğruluğunun ve eksikliğinin garanti edilmesine izin veren.
F * kodundaki kod, Apache 2.0 lisansı altında ve C'deki son modüller ve MIT lisansı altında birleştirici altında dağıtılır.
F * referans koduna göre, assembler, C, OCaml, JavaScript oluşturulur ve web derleme kodu.
Kodun bazı bölümleri hazırlanan proje tarafından zaten Firefox'ta kullanılıyor, Windows çekirdeği , blok zinciri Tezos ve VPN Wireguard.
EverCrypt bileşenleri
Özünde, EverCrypt, HACL * ve Vale'den önceden farklı iki projeyi birleştirir, bunlara dayalı birleşik bir API sağlamak ve bunları gerçek projelerde kullanıma uygun hale getirmek.
HACL * Düşük olarak yazılmıştır* ve amacı, C programlarında kullanılmak üzere şifreleme ilkelleri sağlamaktır. libsodium ve NaCL tarzı API'leri kullanırlar.
proje Vale belirli bir dil geliştirdi derleyicide doğrulamalar oluşturmak için etki alanı.
Low * dilinde yaklaşık 110 bin HACL * kodu satırı ve Vale için 25 bin kod satırı birleştirildi ve yine geliştirilmekte olan evrensel F * dilinde yaklaşık 70 bin satır kodda yeniden yazılıyorlar Everest projesinin bir parçası olarak.
EverCrypt kütüphanesinin ilk versiyonu doğrulanmış uygulamaları içerir aşağıdaki şifreleme algoritmalarının C veya assembler sürümlerinde önerilen (.
Bunlardan aşağıdakiler proje sayfasında öne çıkıyor:
- Karma algoritmalar: SHA2, SHA3, SHA1 ve MD5'in tüm varyantları
- Kimlik doğrulama kodları: Veri kaynağı kimlik doğrulaması için SHA1, SHA2-256, SHA2-384 ve SHA2-512 üzerinden HMAC
- HKDF Anahtar Oluşturma Algoritması (HMAC Tabanlı Çıkartma ve Genişletme Anahtar Türetme İşlevi)
- ChaCha20 akış şifreleme (optimize edilmemiş C sürümü mevcuttur)
- Poly1305 Mesaj Kimlik Doğrulama Algoritması (MAC) (C ve assembler sürümü)
- Eliptik eğrilerde Diffie-Hellman protokolü Curve25519 (BMI2 ve ADX talimatlarına dayalı optimizasyonlara sahip C ve assembler sürümleri)
- Blok şifreleme modu AEAD (kimlik doğrulamalı şifre) ChachaPoly (sürüm C optimize edilmemiş)
- AEAD AES-GCM blok şifreleme modu (AES-NI optimizasyonlu montajcı sürümü).
İlk olarak alfa sürümü, kod doğrulama zaten tamamlandı büyük ölçüde, ancak hala ortaya çıkarılan bazı alanlar var.
Buna ek olarak, API henüz stabilize edilmedi, hangisi genişletilecek aşağıdaki alfa sürümlerinde (Tüm API'ler için yapıların birleştirilmesi planlanmaktadır.
Kusurlar arasında, x86_64 mimarisi desteği de vurgulanmıştır (ilk aşamada temel amaç güvenilirliktir, ikinci sırada optimizasyon ve platformlar uygulanacaktır).
kaynak: https://jonathan.protzenko.fr