On the successful completion of the initiative to replace the cryptographic algorithms implemented in Pythonâs hashlib and hmac modules with mathematically proven reliability variants prepared by the 'HACL*' project. The work to transition to mathematically proven reliability functions has been underway since 2022 and was initiated after the discovery of a buffer overflow in the implementation of the SHA3 algorithm used in the Python hashlib module.
The main repository of the CPython project accepted code with new implementations of cryptographic hash functions and HMAC (hash-based message authentication code). All default hash functions and HMACs provided in Python have been replaced with verified variants. Among other things, an implementation of HMAC-BLAKE2, which uses AVX2 SIMD instructions to accelerate computations, has been added. It is expected that the verified code will be included in the upcoming autumn release of Python 3.14.
New implementations of cryptographic functions have been ported from the HACL* library, developed by researchers from the French National Institute for Research in Computer Science and Automation (INRIA), Microsoft Research, and Carnegie Mellon University. The HACL* library supports standard cryptographic functions sufficient for TLS 1.3 operations and complete support for the NaCl (Networking and Cryptography library) API, such as Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, and HKDF. In terms of performance, the HACL* library is close to OpenSSL, but unlike the latter, provides additional reliability and security guarantees.
The HACL* code is written in a subset of the functional language F*, which offers a system of dependent types and refinements that allow for precise specifications (mathematical models) and ensures the absence of implementation errors through SMT formulas and supporting proof tools. The reference code in F* is translated into C code using the KaRaMeL compiler and is available for integration with other projects.
Verifitseerimine hĂ”lmab kĂ”ikide programmikĂ€itumise variantide kirjeldamiseks vajalike tĂ€psete spetsifikatsioonide mÀÀratlemist ning matemaatilise tĂ”estuse koostamist, et kirjutatud kood vastab tĂ€ielikult koostatud spetsifikatsioonidele. Verifitseerimine tagab, et programm kĂ€itab end ainult nii, nagu arendajad ette nĂ€gid, ja selles puuduvad teatud vigade klassid, nagu mĂ€luaadresside ĂŒletĂ€itumine, pointerite de-referentsimine, juurdepÀÀs juba vabastatud mĂ€lupiirkondadele vĂ”i mĂ€lublokki kahekordne vabastamine. Kompileerimise kĂ€igus tagatakse rangete tĂŒĂŒpide ja vÀÀrtuste kontroll â ĂŒks komponent ei edasta kunagi teisele komponendile spetsifikatsioonile mittevastavaid parameetreid ega saa juurdepÀÀsu teiste komponentide sisestate.
Ăleminekuprotsess verifitseeritud koodile vĂ”ttis aega kaks ja pool aastat ning nĂ”udis HACL* teegi tĂ€iustamist, mille funktsionaalsust laiendati olemasoleva hashlib funktsionaalsuse sujuvaks asendamiseks vajalike omadustega. NĂ€iteks HACL*s lisati HMAC-i voogedastuse reĆŸiimi toimetamine, laiendati Blake2 algoritmide tööreĆŸiime ning rakendati uus SHA3 API, mis katab kĂ”ik Keclaki perekonna algoritmide variandid, samuti tagatakse vajalikke veateate vahendeid (nt mĂ€luhaldusprobleemide puhul) ja töötati vĂ€lja skriptid HACL* uute versioonide automaatseks Python reposse ĂŒleviimiseks.
Allikas: opennet.ru
