Masu bincike daga Cibiyar Nazarin Jiha a Informatics da Automation (INRIYA), Microsoft Research da Carnegie Mellon University aka gabatar fitina ta farko ta da dakin karatun EverCrypt ci gaba tsakanin tsarin aikin Everest da amfani da hanyoyin lissafi na tabbaci na ƙaƙƙarfa amintacce.
Don karfinta da aikinta, EverCrypt yana kusa sosai da dakunan karatun crypto da ake dasu (OpenSSL) amma wannan, ba kamar su ba, yana ba da ƙarin tabbaci na aminci da tsaro.
Alal misali, tsarin tabbatarwa yana sauka don bayyana cikakkun bayanai wanda ke bayyana duk halayen shirin da kuma shaidar lissafi cewa rubutaccen lambar haduwa da bayani dalla-dalla.
Ba kamar hanyoyin kula da ingancin shaida ba, tabbaci yana ba da tabbaci tabbatacce cewa shirin zai gudana ne kawai kamar yadda masu haɓaka suka nufa kuma babu takamaiman azuzuwan kurakurai.
Misali, yarda da bayani dalla-dalla tabbatar da amintaccen aiki tare da ƙwaƙwalwar ajiya da rashin kurakurai waɗanda ke haifar da ambaliyar ajiya, zuwa alamomin rashi, don samun damar zuwa yankuna masu kwakwalwa da aka riga aka yanta, ko kuma 'yantar da tubalan abubuwa biyu.
Menene EverCrypt?
Rariya yana samar da nau'i mai ƙarfi da ƙimar darajar- Wani kayan aiki ba zai taba mika sigogi zuwa wani bangaren da bai dace da shi ba kuma ba zai samu damar shiga cikin jihohin sauran abubuwan ba.
Halin shigarwa / fitarwa yana dacewa da sauƙin ayyukan lissafi, waɗanda aka bayyana a cikin ma'aunin cryptographic.
Don kariya daga hare-hare a cikin tashoshi na ɓangare na uku, hali yayin lissafi (misali, tsawon lokacin aiwatarwa ko kasancewar hanyoyin isa ga wasu ƙwaƙwalwar ajiya) bai dogara da bayanan sirrin da ake sarrafa su ba.
Lambar aikin an rubuta shi a cikin yaren aiki F * (F tauraruwa) , wanda ke samar da tsarin nau'ikan dogaro da tsaftacewa, wanda ke ba da izinin kafa takamaiman bayani dalla-dalla (samfurin lissafi) don shirye-shiryen da kuma tabbatar da daidaito da rashin kurakurai a cikin aiwatarwar ta hanyar dabarun SMT da kayan aikin gwajin taimako.
An rarraba lambar a cikin F * a ƙarƙashin lasisin Apache 2.0, da ƙananan kayayyaki a cikin C da mai haɗuwa a ƙarƙashin lasisin MIT.
Dangane da lambar tunani F *, mai tattarawa, C, OCaml, JavaScript yana samarwa da lambar haɗin yanar gizo.
Wasu sassan lambar shirya ta aikin an riga anyi amfani dashi a Firefox, kwaron Windows , toshewar na Tezos da VPN Wireguard.
Abubuwan haɗin EverCrypt
A cikin mahimmanci, EverCrypt ya haɗu da ayyukan ɓarna a baya guda biyu daga HACL * da Vale, samar da API mai haɗin kai bisa garesu kuma sanya su dacewa don amfani a cikin ainihin ayyukan.
An rubuta HACL * a cikin Lowananan* kuma burinta shine samar da abubuwanda aka kirkira don amfani dasu a cikin shirye-shiryen C suna amfani da libsodium da API na salon NaCL.
Wannan aikin Vale ta haɓaka takamaiman yare yanki don ƙirƙirar tabbaci a cikin mai tarawa.
Kimanin layuka dubu 110 na lambar HACL * a cikin Harshen Low * da layuka dubu 25 na lambar Vale an haɗa su kuma an sake sake rubuta su a kusan layuka dubu 70 na lambar a cikin yaren duniya F *, wanda shima ana ci gaba a matsayin wani ɓangare na aikin Everest.
Farkon sigar ɗakin karatu na EverCrypt fasali tabbatattun aiwatarwa na masu amfani da algorithms masu zuwa samarwa a cikin sifofin C ko masu haɗaka (lokacin amfani da.
Daga cikin waɗannan, waɗannan masu zuwa suna tsaye akan shafin aikin:
- Hash algorithms: duk bambance-bambancen SHA2, SHA3, SHA1, da MD5
- Lambobin tabbatarwa: HMAC akan SHA1, SHA2-256, SHA2-384 da SHA2-512 don tabbatar tushen tushen bayanai
- HKDF Key Generation Algorithm (HMAC na tushen Cire da andara Aikin Maƙallan Maɓalli)
- ChaCha20 ɓoyayyen ɓoyayyen ɓoye (wanda ba ingantaccen C ba akwai)
- Poly1305 Tabbatar da Tabbacin algorithm (MAC) (C da sigar mai haɗawa)
- Yarjejeniyar Diffie-Hellman akan masu lankwasawar lankwasa Curve25519 (C da sigar tarawa tare da ingantawa bisa dogaro da BMI2 da ADX umarnin)
- Toshe yanayin yanayin AEAD (ingantaccen cipher) ChachaPoly (sigar C ba gyara ba)
- Yanayin ɓoye AEAD AES-GCM (sigar tattarawa tare da inganta AES-NI).
A cikin na farko sigar alpha, an riga an kammala tabbatar da lambar galibi, amma har yanzu akwai wasu wuraren da aka gano.
Har ila yau, API bai daidaita ba tukuna, wanda za'a fadada shi a cikin jerin haruffa masu zuwa (An shirya shi ne don haɗa kan tsari don duk APIs.
Daga cikin kurakuran, tallafi ga gine-ginen x86_64 shima an haskaka (a matakin farko, babban burin shine abin dogaro, yayin da ingantawa da dandamali za a aiwatar da shi a wuri na biyu).
Source: https://jonathan.protzenko.fr