Հայտարարվել է Python-ում hashlib և hmac մոդուլներում առաջարկվող կրիպտոգրաֆիկ ալգորիթմների իրականացումները փոխելու նախաձեռնության հաջող ավարտի մասին, փոխարինելով դրանք HACL* նախագծի կողմից պատրաստված սննդի ապացույցներով տարբերակներով: սննդի ապացույցներով գործառույթներին անցնելու աշխատանքները սկսվել են 2022 թվականին և նախաձեռնվել են SHA3 ալգորիթմի իրականացման մեջ Buffered Overflow-ի հայտնվեցնելուց հետո, որը օգտագործվում էր Python-ում hashlib մոդուլում:
CPython նախագծի հիմնական ռեպոզիտոր է ընդունվել նոր կրիպտոգրաֆիկ hash-ֆունկցիաների և HMAC (հաղորդագրությունների ստուգման մեխանիզմ) ալգորիթմների իրականացումը: Python-ում ըստ ձևի տրամադրված բոլոր hash-ֆունկցիաներն ու HMAC-ները փոխարինվել են հաստատված տարբերակներով: Մյուս բաներից, ավելացվել է HMAC-BLAKE2 իրականացումը, որը օգտագործում է AVX2 SIMD հրահանգները հաշվարկների արագացման համար: Ապահովվում է, որ հաստատված կոդը կմտնի Python 3.14-ի աշնային թողարկման:
Նոր կրիպտոգրաֆիկ գործառույթները փոխանցվել են HACL* գրադարանից, որը զարգանում է Ֆրանսիայի պետական ինֆորմատիկայի և ավտոմատիկայի հետազոտությունների ինստիտուտի (INRIA), Microsoft Research-ի և Քառնեգի Մելոնի համալսարանի հետազոտողների կողմից: HACL* գրադարանը աջակցում է տիպային կրիպտոգրաֆիկ գործառույթներին, որոնք բավարար են TLS 1.3 աշխատանքի և NaCl (Networking and Cryptography library) API-ի լիարժեք աջակցման համար, ինչպիսիք են Curve25519, Ed25519, AES-GCM, ChaCha20, Poly1305, SHA-2, SHA-3, HMAC և HKDF: HACL* գրադարանը արտադրողականությամբ մոտ է OpenSSL-ին, բայց վերջինիս տարբերակով ապահովում է լրացուցիչ ապացույցներ ապահովության և անվտանգության համար:
HACL* կոդը գրված է F* ֆունկցիոնալ լեզվի ենթախմբով, որը առաջարկում է կախված տիպերի և ճշգրտումների համակարգ, որը թույլ է տալիս հստակ սահմանել բնութագրերը (մաթեմատիկական մոդել) և երաշխավորել, որ իրականացման մեջ սխալներ չկան SMT-ֆորմուլների և աջակցող ապացուցման գործիքների միջոցով: F* լեզվով բարոյական կոդը փոխարկվում է C լեզվով կոդի միջոցով KaRaMeL կրիչի միջոցով և հասանելի է միավորելու համար այլ նախագծերի հետ:
Վերիֆիկացիայի գործընթացը ենթադրում է ծրագրի վարքագծի բոլոր տարբերակների վերաբերյալ մանրամասն սահմանումների որոշում և մաթեմատիկական ապացույցի ձևավորում, որ գրած կոդը լիովին համապատասխանում է նախապատրաստված սահմանումներին: Վերիֆիկացիան ապահովում է, որ ծրագիրը կկատարի միայն այնպես, ինչպես նախատեսել են մշակողները, և որ այն չի պարունակում որոշակի այնպիսի սխալների դասեր, ինչպիսիք են բայթերի հպումը, ցուցանիշների անձնագրում, արդեն ազատված հիշողության հատվածների մուտքը կամ հիշողության բլոկների կրկին ազատումը: Compilացիայի գործընթացում ապահովվում է խիստ տեսակների և արժեքների ստուգում՝ մեկ կոմպոնենտը երբեք չի փոխանցի մեկ այլ կոմպոնենտին այն պարամետրերը, որոնք չեն համապատասխանում սահմանմանը, և չի ստանա մուտք այլ կոմպոնենտների ներքին վիճակներին:
Վերիֆիկացված կոդին անցման գործընթացը տևեց երկուուկես տարի և պահանջեց HACL* գրադարանից լրացումներ, որի գործառույթները բարձրացվել են hashlib-ի գոյություն ունեցող գործառույթների փոխարինման համար անհրաժեշտ հնարավորություններով: Օրինակ, HACL*-ում ավելացվել է HMAC-ի հոսքային ռեժիմի աջակցություն, առաջարկվել են ալգորիթմների Blake2 լրացուցիչ ռեժիմներ, իրականացվել է SHA3 համար նոր API, որի մեջ ընդգրկված են Keccak ընտանիքի ալգորիթմների բոլոր տարբերակները, ապահովվել են անհրաժեշտ սխալների ծանուցման միջոցներ (օրինակ, հիշողության հատկացման խնդիրների դեպքում), մշակվել են սցենարներ HACL* նոր վարկածները Python-ի պահպանման համար ավտոմատացման նպատակով:
Ընտանիք: opennet.ru
