Kutatók innen: Állami Informatikai és Automatizálási Kutatóintézet (INRIA), A Microsoft Research és a Carnegie Mellon Egyetem bemutatta első próbakiadása az EverCrypt kriptotár az Everest projekt keretében és a formális megbízhatóság igazolásának matematikai módszereit felhasználva fejlesztették ki.
Képességeinek és teljesítményének Az EverCrypt nagyon közel van a meglévő kriptográfiai könyvtárakhoz (OpenSSL), de ez velük ellentétben további garanciákat nyújt a megbízhatóságra és a biztonságra.
Pl. az ellenőrzési folyamat a részletes specifikációk meghatározásához vezet amelyek leírják a program minden viselkedését és a matematikai bizonyíték arra, hogy az írott kód megfelel az elkészített előírásoknak.
A bizonyítékokon alapuló minőség-ellenőrzési módszerektől eltérően az ellenőrzés megbízható garanciákat nyújt hogy a program csak a fejlesztők szándéka szerint fog futtatni, és nincsenek meghatározott osztályú hibák.
Például a specifikációnak való megfelelés biztosítja a memóriával való biztonságos munkát és a puffer túlcsordulásához vezető hibák hiányát, a dereferencia-mutatókhoz, a már felszabadult memóriaterületekhez való hozzáféréshez vagy a memóriablokkok kettős felszabadításához.
Mi az EverCrypt?
EverCrypt robusztus típus- és értékellenőrzést biztosít- Egy komponens soha nem adja át a paramétereket a másik nem megfelelő komponensnek, és nem jut hozzá a többi komponens belső állapotaihoz.
A bemeneti / kimeneti viselkedés teljes mértékben megfelel az egyszerű matematikai függvény műveleteknek, amelyeket a kriptográfiai szabványok határoznak meg.
A támadások elleni védelem érdekében harmadik fél csatornáin, viselkedés a számítások során (például a végrehajtás időtartama vagy bizonyos memóriákhoz való hozzáférés) nem függ a feldolgozott titkos adatoktól.
A projekt kódja az F * funkcionális nyelven van megírva (F csillag) , amely a függő típusok és finomítások rendszerét biztosítja, amelyek lehetővé teszik a programok pontos specifikációinak (matematikai modell) meghatározását, valamint az SMT-képletek és a kiegészítő teszteszközök révén garantálják a megvalósítás helyességét és hibáinak hiányát.
Az F * -ban lévő kódot az Apache 2.0 licenc alatt terjesztik, a végső modulokat pedig a C-ben és az assemblert az MIT licenc alatt.
Az F * hivatkozási kód alapján, assembler, C, OCaml, JavaScript jön létre és a webes összeállítási kódot.
A kód egyes részei előkészített A projekt által már használt Firefox, Windows kernel , a blokklánc Tezos és VPN Wireguard.
EverCrypt komponensek
Összefoglalva, Az EverCrypt két korábban eltérő projektet ötvöz a HACL * és a Vale részéről, ezek alapján egységes API biztosítása és alkalmassá tétele valós projektekben történő felhasználásra.
A HACL * szót Low-ban írják* és célja kriptográfiai primitívek biztosítása a C programokban való felhasználáshoz a libsodium és a NaCL stílusú API-kat használják.
A projekt Vale kifejlesztett egy sajátos nyelvet tartomány ellenőrzések létrehozásához az assemblerben.
Körülbelül 110 ezer sor HACL * kód Low * nyelven és 25 ezer sor Vale kód kombinálva van és körülbelül 70 ezer kódsorban írják át az univerzális F * nyelven, amelyet szintén fejlesztenek az Everest projekt részeként.
Az EverCrypt könyvtár első verziója ellenőrzött megvalósításokat tartalmaz az alábbi kriptográfiai algoritmusok közül javasolt C vagy assembler változatban (a.
Ezek közül a következők jelennek meg a projekt oldalán:
- Hash algoritmusok: az SHA2, SHA3, SHA1 és MD5 összes változata
- Hitelesítési kódok: HMAC SHA1, SHA2-256, SHA2-384 és SHA2-512 felett az adatforrás hitelesítéséhez
- HKDF kulcsgenerálási algoritmus (HMAC alapú kivonat és kibontás kulcs levezetési függvény)
- ChaCha20 adatfolyam-titkosítás (nem optimalizált C verzió érhető el)
- Poly1305 üzenet hitelesítési algoritmus (MAC) (C és assembler verzió)
- Diffie-Hellman protokoll elliptikus görbéken, Curve25519 (C és assembler verziók a BMI2 és ADX utasításokon alapuló optimalizálásokkal)
- AEAD blokkolt kódolási mód (hitelesített titkosítás) ChachaPoly (a C verzió nincs optimalizálva)
- AEAD AES-GCM blokk titkosítási mód (assembler verzió AES-NI optimalizálásokkal).
Az elsőben alfa verzió, a kód ellenőrzése már befejeződött nagyrészt, de még mindig vannak olyan területek, amelyek nem fedezhetők fel.
Ezen túlmenően, Az API még nem stabilizált, amelyet kibővítenek a következő alfa verziókban (Tervezik az összes API struktúrájának egységesítését.
A hibák közül az x86_64 architektúra támogatását is kiemelik (az első szakaszban a fő cél a megbízhatóság, míg az optimalizálás és a platformok a második helyen valósulnak meg).
forrás: https://jonathan.protzenko.fr