{"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\/nl\/blog\/news\/v-python-zadejstvovany-kriptofunkczii-s-matematicheskim-dokazatelstvom-nadyozhnosti","title":{"rendered":"Python maakt gebruik van cryptofunctions met wiskundig bewijs van betrouwbaarheid","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Er is bekendgemaakt dat de initiatief ter vervanging van de cryptografische algoritmes in Python's hashlib en hmac modules met wiskundig bewijs van betrouwbaarheid, voorbereid door het project \u2018HACL*\u2019, succesvol is afgerond. Het werk aan de overstap naar functies met wiskundig bewijs is begonnen in 2022 en werd ge\u00efnitieerd na het ontdekken van een buffer overflow in de implementatie van het SHA3-algoritme, dat in de Python-module hashlib wordt gebruikt. <\/p>\n
De code met de nieuwe implementaties van cryptografische hash-functies en HMAC-algoritmen (mechanisme voor message-authenticatie) is in de hoofdrepository van het CPython-project opgenomen. Alle standaard hash-functies en HMAC in Python zijn vervangen door gevalideerde versies. Onder andere is de implementatie van HMAC-BLAKE2 toegevoegd, die SIMD-instructies AVX2 gebruikt om de berekeningen te versnellen. Verwacht wordt dat de gevalideerde code deel uitmaakt van de herfstrelease van Python 3.14. <\/p>\n
De nieuwe implementaties van cryptografische functies zijn overgezet vanuit de HACL*-bibliotheek, ontwikkeld door onderzoekers van het Franse nationale instituut voor informatica en automatisering (INRIA), een afdeling van Microsoft Research en de Carnegie Mellon Universiteit. De HACL*-bibliotheek ondersteunt de gebruikelijke cryptografische functies die nodig zijn voor TLS 1.3 en volledige ondersteuning van de NaCl API (Networking and Cryptography library), zoals Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC en HKDF. Wat betreft prestaties is de HACL*-bibliotheek vergelijkbaar met OpenSSL, maar biedt, in tegenstelling tot laatstgenoemde, extra garanties voor betrouwbaarheid en veiligheid. <\/p>\n
De HACL*-code is geschreven in een subset van de functionele taal F*, die een systeem van afhankelijke types en qualifiers biedt, waarmee exacte specificaties (wiskundige modellen) kunnen worden vastgesteld en de afwezigheid van fouten in de implementatie kan worden gegarandeerd met behulp van SMT-formules en ondersteunende bewijsinstrumenten. De referentiecode in F* wordt met behulp van de KaRaMeL-compiler omgezet in C-code en is beschikbaar voor integratie met andere projecten. <\/p>\n
Verificatie houdt in dat gedetailleerde specificaties worden opgesteld die alle mogelijke gedragingen van het programma beschrijven, en dat er een wiskundig bewijs wordt gevormd dat de geschreven code volledig overeenkomt met de opgestelde specificaties. Verificatie garandeert dat het programma alleen zal functioneren zoals de ontwikkelaars het hebben bedoeld en dat het vrij is van bepaalde klassen fouten, zoals buffer overflows, dereferentie van pointers, toegang tot al vrijgegeven geheugenruimten of dubbele vrijgave van geheugenblokken. Tijdens de compilatie wordt een strikte controle op typen en waarden gegarandeerd - \u00e9\u00e9n component zal nooit parameters die niet aan de specificaties voldoen aan een andere component doorgeven en zal geen toegang krijgen tot de interne toestanden van andere componenten. <\/p>\n
Het proces van overschakelen naar verificatieve code duurde twee\u00ebnhalf jaar en vereiste aanpassingen aan de HACL*-bibliotheek, waarvan de functionaliteit werd uitgebreid met de mogelijkheden die nodig waren voor de transparante vervanging van de bestaande functionaliteit van hashlib. Bijvoorbeeld, in HACL* werd ondersteuning toegevoegd voor de stroommodus van HMAC, werden extra werkmodi voor de algoritmen Blake2 geboden, werd een nieuwe API voor SHA3 ge\u00efmplementeerd, die alle varianten van de Keccak-familie dekt, en werden de noodzakelijke foutmeldingtools ontwikkeld (bijvoorbeeld bij geheugenallocatieproblemen), en werden scripts ontwikkeld voor de automatisering van de overdracht van nieuwe versies van HACL* naar de Python-repository. \n Bron: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"