De succesvolle afronding van het initiatief om de cryptografische algoritmes in Python, aangeboden in de modules hashlib en hmac, te vervangen door wiskundig bewezen varianten, voorbereid door het 'HACL*'-project, is aangekondigd. Het werk aan de overstap naar functies met wiskundige bewijsvoering begon in 2022 en werd geĆÆnitieerd na het ontdekken van een buffer-overloop in de implementatie van het SHA3-algoritme, dat in de Python-module hashlib wordt gebruikt.
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.
De nieuwe implementaties van cryptografische functies zijn overgebracht uit de HACL*-bibliotheek, ontwikkeld door onderzoekers van het Franse staatsinstituut voor informatica en automatisering (INRIA), onderdeel van Microsoft Research en de Carnegie Mellon Universiteit. De HACL*-bibliotheek ondersteunt de typische 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. Qua prestaties is de HACL*-bibliotheek vergelijkbaar met OpenSSL, maar biedt, in tegenstelling tot de laatste, extra garanties voor betrouwbaarheid en veiligheid.
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.
Het uitvoeren van 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 voldoet aan de opgestelde specificaties. Verificatie garandeert dat het programma uitsluitend functioneert zoals de ontwikkelaars dat bedoeld hebben en dat bepaalde klassen van fouten ontbreken, zoals bufferoverloop, het derefereren van pointers, toegang tot al vrijgegeven geheugengebieden of dubbele vrijgave van geheugensegmenten. Tijdens het compileren vindt er een strikte controle plaats op types en waarden - een component zal nooit een parameter die niet aan de specificatie voldoet doorgeven aan een andere component, en zal geen toegang krijgen tot interne toestanden van andere componenten.
Het proces van overschakelen naar verificatieve code duurde tweeĆ«nhalf 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ĆÆmplementeerd, 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.
Bron: opennet.ru
