Mae'r fenter i ddisodli gweithrediadau Python o algorithmau cryptograffig a gynigir yn y modiwlau hashlib a hmac gyda fersiynau wedi'u profi'n fathemategol a baratowyd gan brosiect HACL* wedi'i chyhoeddi fel un sydd wedi'i chwblhau'n llwyddiannus. Mae gwaith ar newid i swyddogaethau gyda phrawf mathemategol o ddibynadwyedd wedi bod yn mynd rhagddo ers 2022 ac fe'i cychwynnwyd ar ôl darganfod gorlif byffer wrth weithredu'r algorithm SHA3 a ddefnyddir yn hashlib modiwl Python.
Mae prif storfa'r prosiect CPython wedi derbyn cod gyda gweithrediadau newydd o swyddogaethau hash cryptograffig ac algorithmau HMAC (mecanwaith dilysu neges). Mae'r holl swyddogaethau hash rhagosodedig a HMAC a ddarperir yn Python wedi'u disodli gan amrywiadau wedi'u dilysu. Ymhlith pethau eraill, mae gweithrediad HMAC-BLAKE2 wedi'i ychwanegu, sy'n defnyddio cyfarwyddiadau AVX2 SIMD i gyflymu cyfrifiannau. Disgwylir i'r cod wedi'i ddilysu gael ei gynnwys yn natganiad cwymp Python 3.14.
Mae'r gweithrediadau newydd o swyddogaethau cryptograffig wedi'u porthi o lyfrgell HACL*, sy'n cael ei datblygu gan ymchwilwyr o Sefydliad Cenedlaethol Ffrainc ar gyfer Ymchwil mewn Technoleg Gwybodaeth ac Awtomeiddio (INRIA), is-adran o Microsoft Research, a Phrifysgol Carnegie Mellon. Mae llyfrgell HACL* yn cefnogi swyddogaethau cryptograffig cyffredin sy'n ddigonol ar gyfer TLS 1.3 a chefnogaeth lawn i'r API NaCl (llyfrgell Rhwydweithio a Chryptograffeg), fel Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, a HKDF. O ran perfformiad, mae llyfrgell HACL* yn agos at OpenSSL, ond yn wahanol i'r olaf, mae'n darparu gwarantau ychwanegol o ddibynadwyedd a diogelwch.
Mae cod HACL* wedi'i ysgrifennu mewn is-set o'r iaith swyddogaethol F*, sy'n darparu system o fathau dibynnol a mireinio sy'n caniatáu rhoi manylebau manwl gywir (y model mathemategol) ac yn gwarantu y bydd y gweithrediad yn rhydd o wallau gan ddefnyddio fformwlâu SMT ac offer prawf ategol. Mae'r cod cyfeirio F* yn cael ei gyfieithu i god C gan ddefnyddio'r crynhoydd KaRaMeL ac mae ar gael i'w integreiddio â phrosiectau eraill.
Mae cynnal dilysu yn cynnwys diffinio manylebau manwl sy'n disgrifio pob ymddygiad posibl y rhaglen a chreu prawf mathemategol bod y cod ysgrifenedig yn cydymffurfio'n llawn â'r manylebau a baratowyd. Mae dilysu yn rhoi sicrwydd y bydd y rhaglen yn gweithredu dim ond fel y bwriadwyd gan y datblygwyr ac ei bod yn rhydd o rai dosbarthiadau o wallau, megis gorlifoedd byffer, dadgyfeirio pwyntydd, mynediad i ardaloedd cof sydd eisoes wedi'u rhyddhau, neu ryddhau dwbl. Mae'r broses lunio yn sicrhau gwirio math a gwerth llym - ni fydd un gydran byth yn trosglwyddo paramedrau i gydran arall nad ydynt yn cyd-fynd â'r fanyleb, ac ni fydd ganddi fynediad at gyflyrau mewnol cydrannau eraill.
Cymerodd y broses o newid i god wedi'i wirio ddwy flynedd a hanner ac roedd angen datblygu'r llyfrgell HACL*, y cafodd ei swyddogaeth ei hehangu gyda'r galluoedd angenrheidiol i ddisodli swyddogaeth bresennol hashlib yn dryloyw. Er enghraifft, ychwanegodd HACL* gefnogaeth ar gyfer modd ffrydio gweithredu HMAC, darparodd ddulliau gweithredu ychwanegol ar gyfer algorithmau Blake2, gweithredodd API newydd ar gyfer SHA3 sy'n cwmpasu pob amrywiad o deulu algorithmau Keccak, darparodd y dulliau angenrheidiol o hysbysu gwallau (er enghraifft, rhag ofn problemau gyda dyrannu cof), a datblygodd sgriptiau ar gyfer awtomeiddio trosglwyddo fersiynau newydd o HACL* i'r storfa Python.
Ffynhonnell: opennet.ru
