Kuelekea Uthibitishaji Rasmi wa Algorithmu za Kizalisha Nenosiri katika Meneja wa Nenosiri

1. Utangulizi

Meneja wa nenosiri (PMs) ni zana muhimu kwa usalama wa kisasa wa kidijitali, wakiwezesha watumiaji kutumia nenosiri ngumu na ya kipekee bila mzigo wa kiakili wa kukumbuka. Hata hivyo, upitishaji mkubwa wa watumiaji unazuiliwa na ukosefu wa msingi wa imani katika mifumo hii. Karatasi hii inashughulikia kiini cha msingi cha ukosefu huo wa imani: algorithmu ya kizalisha nenosiri nasibu (RPG). Tunadai kuwa uthibitishaji rasmi wa algorithmu hizi sio mazoezi ya kitaaluma tu, bali ni hatua muhimu kuelekea kujenga mifumo ya usimamizi wa nenosiri yenye usalama na kuaminika kwa uthibitisho.

Karatasi hii inachunguza algorithmu za kawaida katika PM maarufu kama Google Chrome, Bitwarden, na KeePass, na inapendekeza utekelezaji wa kumbukumbu uliothibitishwa rasmi kwa kutumia mfumo wa EasyCrypt. Lengo ni kuhamia kutoka kwa usalama wa heuristik kwenda kwenye sifa za usahihi na usalama zilizothibitishwa kihisabati.

2. Algorithmu za Sasa za Kizalisha Nenosiri

Uchunguzi wa meneja 15 wa nenosiri unaonyesha mifumo ya kawaida na tofauti kubwa katika jinsi nenosiri nasibu zinavyozalishwa, zikiathiri moja kwa moja usalama na utii wa sera ya mtumiaji.

3. Mbinu ya Uthibitishaji Rasmi

Tunachukua mbinu ya uthibitisho wa kriptografia yenye msingi wa mchezo ndani ya msaidizi wa uthibitisho wa EasyCrypt. Mbinu hii inahusisha:

1. Ufafanuzi: Kufafanua rasmi tabia ya kazi ya algorithmu ya RPG na mahitaji ya usalama.
2. Utekelezaji: Kuandika algorithmu kwa lugha ya EasyCrypt.
3. Uthibitishaji: Kuthibitisha kuwa utekelezaji unakidhi ufafanuzi wake. Hii inajumuisha:
   • Usahihi wa Kazi: Matokeo daima yanakidhi sera iliyofafanuliwa na mtumiaji.
   • Usalama (Nasibu): Matokeo hayawezi kutofautishwa na mfuatano wa nasibu wa kweli wa sera ile ile, kwa kudhania kizalisha nambari nasibu (RNG) salama. Hii imeigwa kama mchezo wa uwezekano ambapo adui hawezi kutofautisha matokeo ya RPG na nasibu.

Hii inabadilisha imani kutoka kwa ukaguzi wa msimbo na majaribio kwenda kwenye uthibitisho wa kihisabati.

4. Utekelezaji wa Kumbukumbu Unaopendekezwa

Karatasi hii inapendekeza algorithmu ya RPG ya umoja, yenye moduli iliyoundwa kwa ajili ya uthibitishaji. Sifa zake kuu ni pamoja na:

• Utofautishaji wa Sera: Muundo rasmi wa data unaowakilisha vikwazo vyote vya mtumiaji.
• Uzalishaji wa Awamu Mbili: Awamu ya hakikisho ya kukidhi kwa viwango vya chini, ikifuatiwa na awamu ya sampuli sare kwa nafasi zilizobaki.
• Mpangilio Unaothibitika: Hatua ya mwisho ya kuchanganya yenye uthibitisho wa usawa.

Utekelezaji katika EasyCrypt hutumika kama "kiwango cha dhahabu" ambacho algorithmu za kibiashara zinaweza kulinganishwa au hata kutolewa.

5. Matokeo ya Majaribio & Maelezo ya Chati

Wakati PDF inalenga pendekezo rasmi, matokeo ya majaribio yanayodokezwa ni uthibitishaji wa mafanikio wa utekelezaji wa kumbukumbu ndani ya EasyCrypt. "Chati" ya kazi hii ni muundo wa uthibitisho yenyewe.

6. Maelezo ya Kiufundi & Mfumo wa Kihisabati

Sifa ya msingi ya usalama imefafanuliwa rasmi kama mchezo usioweza kutofautishwa. Acha $\mathcal{A}$ awe adui wa wakati wa polynomial wenye uwezekano. Acha $\text{RPG}(\text{sera})$ iwe algorithmu yetu na $\text{RAND}(\text{sera})$ iwe kizalisha bora kinachotoa mfuatano wa nasibu kamili unaokidhi sera.

Mchezo $\text{IND}^{\text{RPG}}_{\mathcal{A}}$ umefafanuliwa kama:
1. Mshindani hupiga sarafu $b \xleftarrow{\$} \{0,1\}$.
2. Ikiwa $b=0$, mshindani humpa $s \leftarrow \text{RPG}(\text{sera})$ kwa $\mathcal{A}$.
3. Ikiwa $b=1$, mshindani humpa $s \leftarrow \text{RAND}(\text{sera})$ kwa $\mathcal{A}$.
4. $\mathcal{A}$ hutoa nadhani $b'$.
$\mathcal{A}$ anashinda ikiwa $b' = b$.

Faida ya adui imefafanuliwa kama: $$\mathbf{Adv}^{\text{ind}}_{\text{RPG}}(\mathcal{A}) = \left| \Pr[\mathcal{A} \text{ anashinda}] - \frac{1}{2} \right|$$

Lengo la uthibitisho ni kuonyesha kuwa faida hii ni ndogo kwa $\mathcal{A}$ wote wenye ufanisi, chini ya dhana kwamba oracle ya nasibu ya msingi au PRF ni salama. Hii inafikiwa kwa mlolongo wa kuruka kwa michezo, ambapo kila kuruka hubadilisha mchezo asilia kuwa sawa kimaana au ambapo tofauti inathibitika kuwa ndogo.

7. Mfumo wa Uchambuzi: Mfano wa Kesi

Hali: Kuchambua kipengele cha "Watoe Herufi Zinazofanana" katika algorithmu ya Chrome.
Muundo Rasmi: Acha seti kamili ya wahusika iwe $C$. Sehemu ndogo ya "zinazofanana" ni $S \subset C$. Seti iliyoruhusiwa ni $A = C \setminus S$.
Kasoro Inayowezekana (Bila Uthibitishaji): Algorithmu lazima ihakikishe sampuli sare kutoka $A$. Utekelezaji wa kijinga unaweza: 1. Kuchukua sampuli kutoka $C$. 2. Ikiwa sampuli iko katika $S$, kataa na uchukue sampuli tena. Hii ni sahihi tu ikiwa sampuli kutoka $C$ ni sare na kitanzi cha kukataa kinahakikishiwa kumalizika. Katika muktadha wa RNG yenye hali au upendeleo, hii inaweza kutoa habari au kusababisha kutokoma.
Mbinu Iliyothibitishwa: Utekelezaji uliothibitishwa rasmi unge: 1. Kuwa na sharti la awali kwamba $A$ sio tupu. 2. Moja kwa moja kuchukua sampuli kutoka kwa usambazaji sare juu ya $A$ kwa kutumia mabadiliko yaliyothibitika ya matokeo ya RNG. 3. Kujumuisha uthibitisho uliokaguliwa na mashine kwamba usambazaji wa matokeo ni sare juu ya $A$ na haitegemei $S$.
Kesi hii inaonyesha jinsi uthibitishaji rasmi unavyolazimisha utunzaji wazi wa kesi za makali ($A$ tupu) na kuhakikisha sifa ya usalama iliyokusudiwa (usawa).

8. Mtazamo wa Mchambuzi wa Sekta

Uelewa wa Msingi: Sekta ya meneja wa nenosiri imejengwa kwenye msingi wa imani iliyodokezwa, sio usalama uliothibitishwa. Karatasi hii inatambua kwa usahihi kizalisha nenosiri kama kiini muhimu, lakini kilichopuuzwa rasmi, cha imani. Uelewa halisi sio ugumu wa algorithmu—mara nyingi ni rahisi—lakini ukosefu mkubwa wa dhamana za kihisabati kwa kazi nyeti kama hii ya usalama. Ni kama kujenga chumba salama cha benki lakini kutumia kufuli ambayo utaratibu wake umeangaliwa tu kwa kuangalia, sio kupimwa kwa mikazo na michoro ya uhandisi.

Mtiririko wa Kimantiki: Hoja ni ya kulazimisha: 1) Imani ndio kikwazo cha kwanza kwa upitishaji wa PM. 2) RPG ni kipengele muhimu kinachoathiri imani. 3) RPG za sasa zinatekelezwa kwa msimbo wa juhudi bora, sio miundo iliyothibitishwa. 4) Kwa hivyo, uthibitishaji rasmi wa RPG ni njia ya moja kwa moja, yenye athari kubwa ya kuongeza imani. Mtiririko kutoka kwa shida (kutokuamini kwa mtumiaji) hadi suluhisho (uthibitishaji) ni wazi na una motisha nzuri. Uchaguzi wa EasyCrypt na uthibitisho wenye msingi wa michezo ni sahihi, ukilingana na mazoea yaliyokua katika kriptografia iliyothibitishwa kama vile utekelezaji uliothibitishwa katika miradi kama HACL*.

Nguvu & Kasoro:
Nguvu: Karatasi hii inashughulikia shida halisi ya ulimwengu, yenye hatari kubwa kwa mbinu madhubuti. Kutoa utekelezaji wa kumbukumbu uliothibitishwa ni wa vitendo zaidi kuliko kukosoa tu. Kulenga viongozi wa chanzo wazi (Chrome, Bitwarden, KeePass) hufanya uchambuzi uwe halisi na unaohusika.
Kasoro: Tembo katika chumba ni muunganiko. Algorithmu ya msingi iliyothibitishwa haina maana ikiwa mfumo unaozunguka—UI, usimbaji fiche wa hifadhidata ya nenosiri, utaratibu wa kujaza kiotomatiki—una hatari. Karatasi inadhania kwa dhana "kiini" safi cha kriptografia, lakini uvamizi wa ulimwengu halisi mara nyingi hulenga msimbo wa kuunganisha, kama inavyoonekana katika udhaifu mbalimbali wa nyongeza ya kivinjari. Zaidi ya hayo, utendaji wa algorithmu iliyopendekezwa dhidi ya zile za heuristik haujadiliwa; uthibitishaji unaweza kuongeza mzigo.

Uelewa Unaoweza Kutekelezeka:
1. Kwa Wauzaji wa PM: Kupitisha au kukagua dhidi ya utekelezaji wa kumbukumbu uliothibitishwa. Anza kuchukulia RPG kama moduli ya kriptografia, sio tu kazi ya matumizi. Fadhili juhudi za ndani za uthibitishaji au ukaguzi unaolenga sehemu hii.
2. Kwa Vyombo vya Viwango (mfano, NIST, FIDO): Kukuza na kuchapisha ufafanuzi rasmi wa kizalisha nenosiri. Miongozo ya sasa (mfano, NIST SP 800-63B) inategemea maandishi; ufafanuzi unaoweza kuthibitishwa na mashine ungebadilisha mchezo kabisa.
3. Kwa Wakaguzi wa Usalama: Badilisha kutoka kwa majaribio ya kisanduku nyeusi ya RPG hadi kukagua muundo wao dhidi ya miundo iliyothibitishwa. Orodha ya ukaguzi kutoka kwa uchambuzi wa sera wa karatasi hii hutoa mahali pa kuanzia.
4. Kwa Watafiti: Panua kazi hii juu ili kuthibitisha ukusanyaji wa entropy/kuanda kwa RNG na chini ili kuthibitisha mzunguko mzima wa usimamizi wa nenosiri. Lengo la mwisho linapaswa kuwa meneja wa nenosiri uliothibitishwa kutoka mwanzo hadi mwisho, mwelekeo unaodokezwa na miradi katika programu ya mifumo iliyothibitishwa.

9. Matumizi ya Baadaye & Mwelekeo wa Utafiti

Matokeo ya kazi hii yanapanuka zaidi ya meneja wa nenosiri:

• Uthibitishaji bila Nenosiri: Shida ya msingi ya kuzalisha na kusimamia tokeni za kriptografia (mfano, kwa nambari za rudufu za WebAuthn) ni sawa. Algorithmu za kizalisha zilizothibitishwa zitakuwa muhimu kwa mifumo hii.
• Usanikishaji wa Vifaa vya IoT: Uwekaji mkubwa wa vifaa vya IoT mara nyingi hutumia nenosiri chaguo-msingi zilizozalishwa kialgorithmu. Kizalisha kilichothibitishwa kinaweza kuondoa darasa zima la hati za chaguo-msingi dhaifu.
• Muunganiko na Usalama wa Vifaa: RPG za baadaye zinaweza kutekelezwa kama msimbo uliothibitishwa unaoendeshwa katika Mazingira ya Utendaji Yanayoaminika (TEE) au kipengele salama, na uthibitisho rasmi ukiongezeka hadi kwenye kiolesura cha vifaa.
• Sera Zinazobadilika: Utafiti unahitajika katika algorithmu zilizothibitishwa rasmi ambazo zinaweza kubadilisha sera kulingana na ujasusi wa vitisho vya wakati halisi au mahitaji maalum ya tovuti huku zikidumisha dhamana za usalama.
• Muundo wa Pamoja wa Utumiaji-Uthibitishaji: Changamoto inayofuata ni kuiga rasmi na kuthibitisha sifa zinazohusiana na utumiaji, kama vile uwezo wa kukumbukwa kwa nenosiri (kwa madhumuni ya rudufu) na uwezo wa kuandika kwenye kibodi tofauti, kuhakikisha vikwazo hivi "laini" havileti kasoro za usalama.

Mwelekeo unaonyesha siku zijazo ambapo vipengele muhimu vya programu ya usalama sio tu chanzo wazi lakini huja na uthibitisho uliokaguliwa na mashine wa sifa zao za msingi, na kuongeza uwazi na imani wakati huo huo.

10. Marejeo

1. Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Towards Formal Verification of Password Generation Algorithms used in Password Managers. arXiv preprint arXiv:2106.03626v2.
2. Bhargavan, K., et al. (2017). HACL*: A Verified Modern Cryptographic Library. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17).
3. Grassi, P. A., et al. (2017). Digital Identity Guidelines: Authentication and Lifecycle Management (NIST Special Publication 800-63B). National Institute of Standards and Technology.
4. Chothia, T., et al. (2016). Automatically Detecting Vulnerabilities in Browser Extensions. IEEE Security & Privacy.
5. Bellare, M., & Rogaway, P. (2006). The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. Advances in Cryptology – EUROCRYPT 2006.
6. EasyCrypt Proof Assistant. (n.d.). Retrieved from https://easycrypt.info/