Bylo oznámeno úspěšné dokončení iniciativy na nahrazení implementací kryptografických algoritmů v Pythonu, které jsou nabízeny v modulech hashlib a hmac, variantami s matematickým důkazem spolehlivosti, vyvinutými projektem „HACL*“. Práce na přechodu na funkce s matematickým důkazem spolehlivosti probíhala od roku 2022 a byla iniciována po zjištění přetečení bufferu v implementaci algoritmu SHA3, používané v Python modulu hashlib.
Do hlavního repozitáře projektu CPython byl přijat kód s novými implementacemi kryptografických hash funkcí a algoritmů HMAC (mechanismus ověřování zpráv). Všechny implicitně poskytované hash funkce a HMAC v Pythonu byly nahrazeny ověřenými variantami. Mezi jinými byla přidána implementace HMAC-BLAKE2, která využívá SIMD instrukce AVX2 pro zrychlení výpočtů. Předpokládá se, že ověřený kód bude součástí podzimní verze Pythonu 3.14.
Nové implementace kryptografických funkcí byly přeneseny z knihovny HACL*, kterou vyvíjejí výzkumníci z francouzského státního institutu pro výzkum v informatice a automatizaci (INRIA), divize Microsoft Research a Carnegie Mellon University. Knihovna HACL* podporuje typické kryptografické funkce, které jsou dostačující pro práci s TLS 1.3 a plnou podporu API NaCl (Networking and Cryptography library), jako jsou Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC a HKDF. Co se týče výkonu, knihovna HACL* je blízká OpenSSL, ale na rozdíl od ní nabízí dodatečné záruky spolehlivosti a bezpečnosti.
Kód HACL* je napsán v podmnožině funkcionálního jazyka F*, který nabízí systém závislých typů a upřesnění, které umožňují stanovit přesné specifikace (matematický model) a zaručit absenci chyb v implementaci pomocí SMT formulí a pomocných nástrojů pro dokazování. Referenční kód v F* je překládán do kódu v jazyce C pomocí kompilátoru KaRaMeL a je dostupný pro integraci s dalšími projekty.
Verifikace zahrnuje stanovení podrobných specifikací, které popisují všechny varianty chování programu, a vytvoření matematického důkazu, že napsaný kód zcela odpovídá připraveným specifikacím. Verifikace zaručuje, že program bude vykonáván pouze tak, jak zamýšleli vývojáři, a neobsahuje určité třídy chyb, jako je přetečení bufferu, dereference ukazatelů, přístup k již uvolněným oblastem paměti nebo dvojité uvolnění bloků paměti. V procesu kompilace je zajištěna přísná kontrola typů a hodnot — jeden komponent nikdy nepředá jinému komponentu parametry, které neodpovídají specifikaci, a nezíská přístup k vnitřním stavům jiných komponentů.
Proces přechodu na verifikovaný kód trval dva a půl roku a vyžadoval úpravy knihovny HACL*, jejíž funkcionalita byla rozšířena o možnosti potřebné pro průhlednou náhradu stávající funkcionality hashlib. Například do HACL* byla přidána podpora pro režim HMAC, poskytnuty další pracovní režimy algoritmů Blake2, implementováno nové API pro SHA3 zahrnující všechny varianty algoritmů rodiny Keccak, zajištěny potřebné prostředky pro oznámení o chybách (např. při problémech s alokací paměti), a vyvinuty skripty pro automatizaci přenosu nových verzí HACL* do repozitáře Python.
Zdroj: opennet.ru
