Bejelentették, hogy sikeresen befejeződött a Pythonban a hashlib és hmac modulokban található kriptográfiai algoritmusok cseréjének kezdeményezése, matematikai megbízhatóságú változatokra, amelyeket a „HACL*” projekt készített. A megbízhatósági matematikai bizonyítékkal ellátott funkciókra való áttérést 2022-ben kezdték meg, miután a Python hashlib modulban észleltek egy puffertúlcsordulást a SHA3 algoritmus megvalósításában.
A CPython projekt fő tárolójába bekerült az új kriptográfiai hash-funkciók és HMAC (üzenetek hitelesítési mechanizmus) algoritmusok új implementációja. Minden Pythonban alapértelmezetten biztosított hash-funkció és HMAC lecserélésre került a hitelesített változatokra. Többek között hozzáadták az AVX2 SIMD utasításokat használó HMAC-BLAKE2 implementációt a számítások gyorsítása érdekében. A hitelesített kód a Python 3.14 őszi kiadásába fog bekerülni.
Az új kriptográfiai funkciók implementációja a HACL* könyvtárból származik, amelyet a Francia Informatikai és Automatikai Kutatóintézet (INRIA), a Microsoft Research és a Carnegie Mellon Egyetem kutatói fejlesztenek. A HACL* könyvtár a TLS 1.3 működéséhez és a NaCl (Hálózati és Kriptográfiai Könyvtár) API teljes támogatásához elegendő tipikus kriptográfiai funkciókat támogat, mint például a Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC és HKDF. Teljesítményben a HACL* könyvtár közel áll az OpenSSL-hez, de a legutóbbihoz képest további megbízhatósági és biztonsági garanciákat kínál.
A HACL* kód egy funkcionális nyelv, az F* egy leszűkített részhalmazán íródott, amely egy függő típusú és finomítási rendszert kínál, amely lehetővé teszi a pontos specifikációk (matematikai modell) megadását és garantálja a megvalósítás hibáinak hiányát SMT-formulák és segédproof eszközök segítségével. Az F* referencia kód C nyelvű kódra fordul a KaRaMeL fordító segítségével, és elérhető más projektek integrációjára.
A verifikációs folyamat magában foglalja a részletes specifikációk meghatározását, amelyek a program minden viselkedésváltozatát leírják, valamint egy matematikai bizonyíték kidolgozását, amely igazolja, hogy a megírt kód teljes mértékben megfelel a készített specifikációknak. A verifikáció garanciát nyújt arra, hogy a program csak úgy működik, ahogy azt a fejlesztők megálmodták, és hogy nem tartalmaz bizonyos hibákat, például puffertúlcsordulást, mutató dekódolást, már felszabadított memóriaterületekhez való hozzáférést vagy memória blokkok dupla felszabadítását. A fordítás során szigorú típus- és értékellenőrzést biztosítanak - egyik komponens soha nem ad át egy másik komponensnek olyan paramétereket, amelyek nem felelnek meg a specifikációnak, és nem fér hozzá más komponensek belső állapotaihoz.
A verifikált kódra való áttérés folyamata két és fél évet vett igénybe, és a HACL* könyvtár továbbfejlesztését igényelte, amelynek funkcionalitása bővült a meglévő hashlib funkcionalitás átlátható cseréjéhez szükséges lehetőségekkel. Például a HACL*-ben támogatást kapott a HMAC folyamatos üzemmódja, további üzemmódok lettek hozzáadva a Blake2 algoritmusokhoz, valamint egy új API valósult meg a SHA3-hoz, amely lefedi a Keccak család összes algoritmusának változatát, szükséges hibaértesítési eszközöket biztosítottak (például memória-elosztási problémák esetén), és írtak automatizálási szkripteket az új HACL* verziók Python-repozitóriumba való áttéréséhez.
Forrás: opennet.ru
