Chagua Lugha

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

Karatasi ya utafiti inayopendekeza utekelezaji wa kumbukumbu uliothibitishwa kwa rasmi kwa jenereta za nenosiri za nasibu katika meneja wa nenosiri, kwa kutumia EasyCrypt kwa usahihi wa kazi na uthibitisho wa usalama.
computationalcoin.com | PDF Size: 0.1 MB
Ukadiriaji: 4.5/5
★ ★ ★ ★ ★
Ukadiriaji Wako
Umekadiria waraka huu tayari
Kifuniko cha Waraka PDF - Kuelekea Uthibitishaji Rasmi wa Algorithmu za Uundaji wa Nenosiri katika Meneja wa Nenosiri
Tazama Waraka PDF Pakua PDF Tafsiri PDF
Nyumbani » Nyaraka » Kuelekea Uthibitishaji Rasmi wa Algorithmu za Uundaji wa Nenosiri katika Meneja wa Nenosiri

1. Utangulizi

Meneja wa nenosiri (PMs) ni zana muhimu zinazopendekezwa na wataalamu wa usalama ili kupunguza udhaifu unaohusishwa na uthibitishaji wa nenosiri. Wanafacilita matumizi ya nenosiri thabiti na ya kipekee, na hivyo kupunguza mzigo wa kiakili kwa watumiaji. Hata hivyo, matumizi makubwa na yanayoenea yamezuiliwa na ukosefu wa imani katika programu hizi. Karatasi hii inabainisha kipengele cha uundaji wa nenosiri wa nasibu (RPG) kama kipengele muhimu kinachoathiri imani ya mtumiaji. Waandishi wanadai kuwa utekelezaji wa RPG uliothibitishwa kwa rasmi na wenye usalama unaoweza kuthibitishwa ni muhimu ili kuziba pengo hili la imani na kuhimiza matumizi ya PM. Mchango wa msingi wa karatasi hii ni kupendekeza utekelezaji wa kumbukumbu kama huo, pamoja na uthibitisho rasmi wa usahihi wa kazi na sifa za usalama kwa kutumia mfumo wa EasyCrypt.

2. Algorithmu za Sasa za Uundaji wa Nenosiri

Karatasi hii inachunguza meneja 15 wa nenosiri, ikizingatia mifano mitatu ya chanzo wazi na inayotumika sana: meneja wa ndani wa Google Chrome, Bitwarden, na KeePass. Uchambuzi unaonyesha muundo wa kawaida na mapungufu muhimu katika utekelezaji uliopo.

2.1 Sera za Muundo wa Nenosiri

PMs huruhusu watumiaji kufafanua sera zinazoweka vikwazo kwa nenosiri zinazoundwa. Sera hizi hubainisha urefu, seti za herufi zinazoruhusiwa (k.m., herufi ndogo, herufi kubwa, nambari, herufi maalum), na idadi ya chini/ya juu inayoruhusiwa kwa kila seti. Karatasi hii inatoa jedwali la kulinganisha lenye maelezo (Jedwali 1 kwenye PDF) linaloonyesha chaguzi za sera katika PM tatu zilizosomwa. Uchunguzi muhimu unajumuisha urefu tofauti wa juu (hadi 30,000 kwenye KeePass), ufafanuzi tofauti wa "herufi maalum," na usimamizi usio sawa wa "herufi zinazofanana" (kama 'l', '1', 'O', '0') ili kuepuka utata wa kuona. KeePass inatoa udhibiti wa kina zaidi, ikiruhusu seti za kujumuisha/kutenga zilizobinafsishwa na kuondoa nakala zinazorudiwa.

2.2 Uundaji wa Nenosiri wa Nasibu

Algorithmu zilizochunguzwa kwa ujumla hufuata mchakato wa awamu mbili: 1) Unda herufi za nasibu ili kukidhi idadi ya chini inayohitajika kwa kila seti maalum ya herufi. 2) Jaza urefu uliobaki wa nenosiri kwa herufi za nasibu kutoka kwa seti yoyote ambayo haijafikia kikomo chake cha juu cha matukio. Hatimaye, mlolongo wa herufi hubadilishwa kwa nasibu. Karatasi hii inadokeza kwamba ingawa mantiki hii ni wazi, utekelezaji wake—hasa chanzo cha nasibu na utekelezaji wa vikwazo changamano—ni nadra kufafanuliwa au kuthibitishwa kwa rasmi, na hivyo kuacha nafasi kwa makosa madogo ambayo yanaweza kudhoofisha usalama.

3. Njia ya Uthibitishaji Rasmi

Waandishi wanahimiza matumizi ya njia rasmi ili kuondoa makosa ya utekelezaji. Walichagua EasyCrypt, mfumo wa kujenga na kuthibitisha uthibitisho wa kriptografia unaotegemea mchezo. Njia hii inajumuisha:

  1. Ufafanuzi: Kufafanua kwa rasmi mahitaji ya kazi ya RPG (sera ya ingizo -> nenosiri la pato linalokidhi sera).
  2. Utekelezaji: Kuandika msimbo wa algorithmu ndani ya EasyCrypt.
  3. Uthibitishaji: Kuthibitisha kuwa utekelezaji unarekebisha kwa usahihi ufafanuzi (usahihi wa kazi).
  4. Uthibitisho wa Usalama: Kuiga algorithmu kama mchezo wa kriptografia ili kuthibitisha sifa kama usambazaji sawa wa matokeo kutoka kwa nafasi iliyofafanuliwa (usalama).

Njia hii inatoa hakika ya kihisabati kwamba msimbo unafanya kazi hasa kama ilivyokusudiwa na una sifa za usalama zinazohitajika, ikizingatiwa kuwa misingi ya msingi ya kriptografia (jenereta ya nambari za nasibu) ni salama.

4. Utekelezaji wa Kumbukumbu Unaopendekezwa

Karatasi hii inapendekeza muundo mpya, wenye moduli za RPG unaokusudiwa kutumika kama kumbukumbu iliyothibitishwa. Ingawa msimbo kamili haujaonyeshwa katika dondoo iliyotolewa, muundo huo hutenganisha kwa mantiki:

  • Kichanganuzi cha Sera & Kithibitishaji: Kuhakikisha sera zilizobainishwa na mtumiaji zinapatana ndani (k.m., viwango vya chini havizidi vya juu, jumla ya viwango vya chini havizidi urefu wa nenosiri).
  • Kichaguzi Kilichowekwa Vikwazo: Injini ya msingi ambayo hufanya uzalishaji wa awamu mbili chini ya vikwazo vya sera.
  • Mpangilio wa Nasibu: Hutumia mchanganyiko wa mwisho kwa mlolongo wa herufi.

Kila moduli ingekuwa na ufafanuzi rasmi na utekelezaji uliothibitishwa katika EasyCrypt.

5. Maelezo ya Kiufundi & Uundaji wa Kihisabati

Usalama wa RPG unategemea entropy na usambazaji sawa wa matokeo yake. Acha $\mathcal{P}$ iwe seti ya nenosiri zote zilizofafanuliwa na sera (urefu $l$, seti za herufi $C_1, C_2, ..., C_n$ zikiwa na vikwazo vya chini/ya juu). RPG bora ni kazi $G$ ambayo huchukua sampuli kwa usawa kutoka $\mathcal{P}$.

Uwezekano wa nenosiri maalum $p \in \mathcal{P}$ kuundwa unapaswa kuwa: $$Pr[G() = p] = \frac{1}{|\mathcal{P}|}$$ ambapo $|\mathcal{P}|$ ni ukubwa wa nafasi ya nenosiri. Kasoro ya kawaida katika utekelezaji wa kijinga ni kuanzisha upendeleo, na kufanya baadhi ya nenosiri ziwe na uwezekano mkubwa zaidi kuliko nyingine. Kwa mfano, ikiwa algorithmu kwanza huchagua herufi za seti zinazohitajika na kisha hujaza zilizobaki, nenosiri zilizo na herufi zinazohitajika mwanzoni zinaonyeshwa kupita kiasi isipokuwa mpangilio kamili wa nasibu utatumika. Uthibitishaji rasmi unathibitisha kutokuwepo kwa upendeleo kama huo.

Entropy $H$ ya nenosiri lililoundwa (kwa bits) ni: $$H = \log_2(|\mathcal{P}|)$$ Uthibitishaji unahakikisha utekelezaji haupunguzi entropy hii chini ya kiwango cha juu cha kinadharia kwa sera hiyo.

6. Matokeo ya Majaribio & Maelezo ya Chati

Ingawa dondoo la PDF lililotolewa halina matokeo ya jadi ya majaribio au chati, "matokeo" yake ya msingi ni uthibitisho rasmi wenyewe. Uthibitishaji uliofanikiwa katika EasyCrypt hutumika kama ushahidi wa mwisho. Mtu anaweza kufikiria chati inayolinganisha viwango vya uhakikisho:

Chati ya Kufikiri: Kiwango cha Uhakikisho dhidi ya Njia ya Uundaji

  • Kupima kwa Jadi: Imani kubwa kwa kesi zilizopimwa, lakini haijulikani kwa kesi za makali ambazo hazijapimwa (migogoro ya sera, thamani za mipaka). Ufuniko ni mdogo.
  • Ukaguzi wa Msimbo: Imani ya wastani. Inategemea sana ujuzi wa mkaguzi. Inaweza kukosa makosa madogo ya mantiki au maswala ya njia za upande.
  • Uthibitishaji Rasmi (kama ilivyopendekezwa): Uhakikisho wa juu zaidi unaowezekana. Hutoa uthibitisho wa kihisabati wa usahihi kwa ingizo zote zinazowezekana na sifa za usalama zilizowazi. "Chati" ingeonyesha hii kama hatua ya juu zaidi kwenye mhimili wa "Uhakikisho."

Mchango wa karatasi hii ni kuhamisha RPG kutoka katika makundi mawili ya kwanza hadi katika ya tatu.

7. Mfumo wa Uchambuzi: Mfano wa Kesi Usio na Msimbo

Fikiria sera: Urefu=8, hitaji angalau herufi 1 kubwa, nambari 1, herufi 1 maalum. Algorithmu yenye kasoro inaweza:

  1. Nafasi ya 1: Chagua herufi kubwa nasibu.
  2. Nafasi ya 2: Chagua nambari nasibu.
  3. Nafasi ya 3: Chagua herufi maalum nasibu.
  4. Nafasi 4-8: Jaza kwa herufi za nasibu kutoka kwa seti zote.
  5. Panga herufi zote 8 kwa nasibu.

Kasoro: Mpangilio wa kudumu wa awali (U, N, S) kabla ya kupanga kwa nasibu huunda upendeleo. Ingawa kupanga kwa nasibu kunabadilisha nafasi za mwisho, mchakato huanza kutoka kwa usambazaji usio sawa wa hali za kati. Algorithmu iliyothibitishwa kwa rasmi ingejenga nenosiri lote kupitia mchakato mmoja, usio na upendeleo wa kuchukua sampuli kutoka kwa nafasi iliyowekwa vikwazo $\mathcal{P}$, au ingeonyesha kwa uthibitisho kwamba mchakato wake wa hatua nyingi ni sawa na kuchukua sampuli kwa usawa kama huo.

8. Uelewa wa Msingi & Mtazamo wa Mchambuzi

Uelewa wa Msingi: Karatasi hii inabainisha kwa usahihi eneo muhimu la shambulio katika meneja wa nenosiri ambalo mara nyingi hupuuzwa: kuaminika kwa jenereta ya nenosiri yenyewe. Haitoshi kuwa na chumba kizito cha usalama; ikiwa nyenzo za msingi (nenosiri) ni dhaifu au zinabashiriwa kutokana na jenereta yenye makosa, mfumo mzima unashindwa. Hatua ya waandishi ya kutumia njia rasmi—mbinu inayotumika zaidi katika programu za vifaa au ndege—kwa tatizo hili la usalama la watumiaji ni ya kusisimua na muhimu.

Mtiririko wa Mantiki: Hoja ni sahihi: 1) Imani ni kikwazo kwa matumizi ya PM. 2) RPG ni sehemu muhimu ya imani. 3) RPG za sasa zinatekelezwa kwa njia ya ad-hoc bila uhakikisho mkali. 4) Uthibitishaji rasmi hutoa kiwango cha juu zaidi cha uhakikisho. 5) Tunatoa mchoro wa RPG iliyothibitishwa kwa kutumia EasyCrypt. Mantiki hii inaunganisha tatizo linalozingatia mtumiaji (imani) na suluhisho la kiufundi la kina (njia rasmi).

Nguvu & Kasoro:
Nguvu: Mwelekeo kwenye PM za chanzo wazi ni wa vitendo. Uchambuzi wa kulinganisha sera ni wa thamani. Kupendekeza utekelezaji wa kumbukumbu kunafaa zaidi kuliko kukosoa wengine tu; huweka kiwango. Kutumia EasyCrypt kunahusisha kazi hii na mazoea ya uthibitishaji wa kriptografia yaliyokua, sawa na uthibitishaji wa algorithmu kama zile katika "The Security of Cryptographic Primitives" (M. Bellare, P. Rogaway).
Kasoro: Dondoo lililotolewa ni hatua ya kuanzia. Mtihani halisi ni utata wa uthibitisho kamili wa EasyCrypt kwa sera za ulimwengu halisi. Njia hii inadhania RNG kamili; udhaifu hapo hupuuza dhamana zote rasmi. Pia haishughulikii mashambulizi ya njia za upande (muda, kumbukumbu) katika faili ya mwisho ya msimbo uliokusanywa, kikomo kilichobainishwa katika miradi mingine ya uthibitishaji rasmi kama uthibitishaji wa seL4 microkernel.

Uelewa Unaoweza Kutekelezwa:
1. Kwa Watengenezaji wa PM: Unganisha kiini hiki kilichothibitishwa, au kitu kama hicho, kama maktaba. Gharama ya uthibitishaji rasmi ni kubwa mwanzoni lakini hupunguza mzigo wa ukaguzi wa usalama wa muda mrefu na majukumu.
2. Kwa Wakaguzi & Watafiti: Tumia kazi hii kama kiolezo kuchambua PM nyingine. Jedwali la kulinganisha sera ni orodha tayari ya ukaguzi wa usalama.
3. Kwa Vyombo vya Viwango (k.m., NIST, FIDO): Fikiria uthibitishaji rasmi kama sharti la kuhakiki moduli za uundaji wa nenosiri, sawa na jinsi Vigezo vya Kawaida vinavyolazimisha michakato mkali ya uundaji kwa bidhaa za uhakikisho wa juu.
4. Kwa Watumiaji: Omba uwazi. Pendekeza PM zinazochapisha algorithmu zao za RPG na, kwa vyema, ushahidi wao wa uthibitishaji. Karatasi hii inatoa msamiati wa kuomba hilo.

Kimsingi, utafiti huu ni wito wa kuinua viwango vya uhandisi kwa sehemu ya msingi ya usalama. Inabadilisha lengo kutoka "salama kwa matumaini" hadi "sahihi kwa uthibitisho," ambayo ndio kiwango pekee kinachokubalika kwa zana zinazolinda utambulisho wetu wa kidijitali.

9. Matumizi ya Baadaye & Mwelekeo wa Utafiti

Matokeo yanapanuka zaidi ya meneja wa nenosiri:

  • Tokeni za API & Huduma: Huduma za wingu na usanifu wa huduma ndogo mara nyingi huhitaji tokeni zinazoundwa. Jenereta iliyothibitishwa inahakikisha siri hizi ni thabiti kwa kriptografia.
  • Uundaji wa Ufunguo wa Kriptografia: Kanuni zinatumika kwa kuzalisha msimbo wa kurejesha unaosomwa na binadamu au maneno ya siri (kupitia njia kama za diceware) kwa funguo za kriptografia, ambapo upendeleo ni hatari sawa.
  • Ushirikiano na Usalama wa Vifaa: Kazi ya baadaye inaweza kuthibitisha mwingiliano kati ya programu ya RPG na Jenereta za Nambari za Nasibu za Kweli za Vifaa (TRNGs) au Mazingira ya Utekelezaji Yanayoaminika (TEEs).
  • Uchambuzi wa Sera wa Otomatiki: Jenga zana zinazochambua kwa rasmi sera zilizobainishwa na mtumiaji kwa udhaifu (k.m., nafasi ndogo za utafutaji kwa ufanisi licha ya utata unaoonekana) kabla ya uzalishaji hata kufanyika.
  • Uwekaji wa Viwango: Mwelekeo mkubwa zaidi wa baadaye ni kugeuza utekelezaji huu wa kumbukumbu kuwa kiwango kinachotumiwa sana, labda kama maktaba pekee (kama libsodium kwa kriptografia) ambayo programu yoyote inaweza kutumia kwa uzalishaji wa siri uliothibitishwa.

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.03626.
  2. Bellare, M., & Rogaway, P. (2005). Introduction to Modern Cryptography. Sura juu ya Kazi za Uongo na Vibali vya Pseudorandom.
  3. Klein, G., et al. (2009). seL4: Uthibitishaji rasmi wa kiini cha OS. Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles.
  4. Taasisi ya Kitaifa ya Viwango na Teknolojia (NIST). (2017). Mwongozo wa Utambulisho wa Kidijitali (SP 800-63B).
  5. Makubaliano ya Kutambua Vigezo vya Kawaida (CCRA). Vigezo vya Kawaida vya Tathmini ya Usalama wa Teknolojia ya Habari.
  6. Chiasson, S., van Oorschot, P. C., & Biddle, R. (2006). Kuangalia tena matumizi ya nenosiri za picha zinazotegemea kubofya. Proceedings of the 3rd symposium on Usable privacy and security.
  7. EasyCrypt Proof Assistant. Nyaraka Rasmi na Mafunzo. https://easycrypt.info/