{"id":123602,"date":"2025-04-19T15:05:06","date_gmt":"2025-04-19T13:05:06","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti"},"modified":"2025-04-19T15:05:06","modified_gmt":"2025-04-19T13:05:06","slug":"v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","status":"publish","type":"post","link":"https:\/\/prohoster.info\/en\/blog\/news\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","title":{"rendered":"Cryptographic functions with mathematical proof of reliability are involved in Python","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
The successful completion of the initiative to replace the implementations of cryptographic algorithms offered in the hashlib and hmac modules in Python with mathematically proven secure variants, prepared by the 'HACL*' project, has been announced. Work on transitioning to functions with mathematical proof of security began in 2022 and was initiated after the discovery of a buffer overflow in the implementation of the SHA3 algorithm used in the Python hashlib module. <\/p>\n
The main repository of the CPython project has accepted code with new implementations of cryptographic hash functions and HMAC (hash-based message authentication code) algorithms. All hash functions and HMACs provided by default in Python have been replaced with verified variants. Among other things, an HMAC-BLAKE2 implementation has been added that utilizes AVX2 SIMD instructions to accelerate computations. It is expected that the verified code will be included in the upcoming release of Python 3.14 in the fall. <\/p>\n
The new implementations of cryptographic functions have been transferred 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 and full 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 guarantees of reliability and security. <\/p>\n
The HACL* code is written in a subset of the functional programming language F*, which offers a system of dependent types and refinements that allow for precise specifications (mathematical models) and guarantees the absence of errors in the implementation through SMT formulas and auxiliary proof tools. The reference code in F* is translated into C code using the KaRaMeL compiler and is available for integration with other projects. <\/p>\n
Verification involves defining detailed specifications that describe all possible behaviors of the program and creating a mathematical proof that the written code fully complies with the prepared specifications. Verification guarantees that the program will execute only as intended by the developers and that it is free from certain classes of errors, such as buffer overflows, pointer dereferencing, access to already freed memory areas, or double freeing of memory blocks. During compilation, strict type and value checking is enforced\u2014one component will never pass parameters that do not match the specification to another component and will not gain access to the internal states of other components. <\/p>\n
The process of transitioning to verified code took two and a half years and required further development of the HACL* library, which was extended with capabilities necessary for the transparent replacement of the existing functionality of hashlib. For instance, HACL* added support for HMAC streaming mode, provided additional operational modes for the Blake2 algorithms, implemented a new API for SHA3 covering all variants of the Keccak family of algorithms, ensured necessary error notification mechanisms (e.g., for memory allocation issues), and developed scripts for automating the migration of new versions of HACL* into the Python repository. \n Source: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"