La iniciato anstataŭigi Python-efektivigojn de ĉifrikaj algoritmoj ofertitaj en la hashlib kaj hmac-moduloj kun matematike pruvitaj versioj preparitaj de la projekto HACL* estis anoncita kiel sukcese kompletigita. Laboro pri ŝanĝado al funkcioj kun matematika pruvo de fidindeco daŭras ekde 2022 kaj estis komencita post la malkovro de bufra superfluo en la efektivigo de la SHA3-algoritmo uzata en la Python-modulo hashlib.
La ĉefa deponejo de la CPython-projekto akceptis kodon kun novaj efektivigoj de ĉifrikaj hash-funkcioj kaj algoritmoj HMAC (mesaĝa aŭtentikiga mekanismo). Ĉiuj defaŭltaj hash-funkcioj kaj HMAC provizitaj en Python estis anstataŭigitaj per kontrolitaj variantoj. Interalie, efektivigo de HMAC-BLAKE2 estis aldonita, kiu uzas AVX2 SIMD-instrukciojn por akceli komputadon. La kontrolita kodo estas atendita esti inkluzivita en la aŭtuna eldono de Python 3.14.
La novaj efektivigoj de kriptografiaj funkcioj estas portitaj de la biblioteko HACL*, kiun disvolvas esploristoj de la Franca Nacia Instituto por Esploro en Informa Teknologio kaj Aŭtomatigo (INRIA), divido de Microsoft Research, kaj la Universitato Carnegie Mellon. La biblioteko HACL* subtenas komunajn kriptografiajn funkciojn, kiuj sufiĉas por TLS 1.3, kaj plenan subtenon por la API NaCl (biblioteko pri retigado kaj kriptografio), kiel ekzemple Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, kaj HKDF. Rilate al rendimento, la biblioteko HACL* estas proksima al OpenSSL, sed male al ĉi-lasta, ĝi provizas pliajn garantiojn pri fidindeco kaj sekureco.
HACL*-kodo estas skribita en subaro de la funkcia lingvo F*, kiu provizas sistemon de dependaj tipoj kaj rafinadoj, kiuj permesas doni precizajn specifojn (la matematika modelo) kaj garantias, ke la efektivigo estos sen eraroj uzante SMT-formulojn kaj helpajn pruvilojn. La referenca kodo F* estas tradukita en C-kodon uzante la kompililon KaRaMeL kaj estas havebla por integriĝo kun aliaj projektoj.
Fari konfirmon implicas difini detalajn specifojn, kiuj priskribas ĉiujn eblajn kondutojn de la programo, kaj krei matematikan pruvon, ke la skriba kodo plene konformas al la pretigitaj specifoj. Konfirmo certigas, ke la programo efektivigos nur kiel intencite de la programistoj kaj estas libera de certaj klasoj de eraroj, kiel bufrotransfluoj, montrilaj dereferencoj, aliro al memorareoj kiuj jam estis liberigitaj, aŭ duoblaj liberigoj. La kompilprocezo certigas striktan tipo- kaj valorkontroladon - unu komponanto neniam transdonos parametrojn al alia komponanto, kiuj ne kongruas kun la specifo, kaj ne havos aliron al la internaj statoj de aliaj komponantoj.
La procezo de ŝanĝo al kontrolita kodo daŭris du jarojn kaj duonon kaj postulis la disvolvon de la biblioteko HACL*, kies funkcioj estis vastigitaj per la kapabloj necesaj por travideble anstataŭigi la ekzistantan funkciojn de hashlib. Ekzemple, HACL* aldonis subtenon por la flua reĝimo de HMAC-operacio, provizis pliajn reĝimojn de operacio por Blake2-algoritmoj, efektivigis novan API-on por SHA3, kiu kovras ĉiujn variaĵojn de la Keccak-familio de algoritmoj, provizis la necesajn rimedojn por erarsciigo (ekzemple, en kazo de problemoj kun memorasigno), kaj evoluigis skriptojn por aŭtomatigi la translokigon de novaj versioj de HACL* al la Python-deponejo.
fonto: opennet.ru
