Zuwa Tabbatar da Tsarin Hanyoyin Ƙirƙirar Kalmar Sirri a cikin Manajoji na Kalmar Sirri

1. Gabatarwa

Manajoji na kalmar sirri (PMs) muhimman kayan aiki ne don tsaron dijital na zamani, suna ba masu amfani damar yin amfani da kalmar sirri mai ƙarfi, na musamman ba tare da nauyin tunawa ba. Duk da haka, yawaitar amfani da masu amfani tana hana saboda rashin amincewa da wadannan tsare-tsare. Wannan takarda tana magana ne da wani muhimmin bangare na wannan rashi na amana: tsarin ƙirƙirar kalmar sirri bazuwa (RPG). Muna jayayya cewa tabbatar da tsarin waɗannan hanyoyin ba wasa ne na ilimi kawai ba, amma mataki ne da ya wajaba don gina tsarin sarrafa kalmar sirri da ke da tabbataccen tsaro da amana.

Takardar tana bincika hanyoyin gama gari a cikin shahararrun PMs kamar Google Chrome, Bitwarden, da KeePass, kuma tana ba da shawarar aiwatar da magana da aka tabbatar ta hanyar amfani da tsarin EasyCrypt. Manufar ita ce mu motsa daga tsaro na hasashe zuwa tabbataccen daidaito da kaddarorin tsaro na lissafi.

2. Hanyoyin Ƙirƙirar Kalmar Sirri na Yanzu

Binciken manajoji na kalmar sirri 15 ya bayyana tsarin gama gari da bambance-bambance masu mahimmanci a yadda ake ƙirƙirar kalmar sirri bazuwa, wanda ke shafar tsaro da bin ka'idojin mai amfani kai tsaye.

2.1 Ka'idojin Tsarin Kalmar Sirri

Manajoji na kalmar sirri suna ba masu amfani damar ayyana ka'idojin da kalmar sirri da aka ƙirƙira dole ne su bi. Waɗannan ka'idoji suna sarrafa tsawon lokaci, saitin haruffa (ƙananan haruffa, manyan haruffa, lambobi, haruffa na musamman), da ƙayyadaddun abubuwa kamar mafi ƙarancin/matsakaicin faruwa kowane saiti ko keɓance haruffa masu shakku (misali, 'l', 'I', 'O', '0').

Kwatanta Ka'idoji: Chrome vs. Bitwarden vs. KeePass

Matsakaicin Tsawon Lokaci: Chrome (200), Bitwarden (128), KeePass (30000)
Saitin Haruffa: Duk suna goyan bayan saitin ginshiƙi; KeePass yana ba da saitin faɗaɗa (Maƙallai, Sarari, Ragewa, Ƙarƙashin layi).
Keɓance Haruffa Masu Kama: Duk suna aiwatar da wannan, amma tare da ɗan bambancin jerin haruffa.
Saitin Al'ada/Keɓancewa: KeePass kawai yana ba da damar saitin haruffa da mai amfani ya ayyana don haɗawa ko keɓancewa.

Bambance-bambance a cikin zaɓuɓɓukan ka'idoji yana haifar da yanayi mai rarrabuwa inda "ƙarfin" kalmar sirri da aka ƙirƙira ba a bayyana shi daidai ba a duk faɗin dandamali.

2.2 Ƙirƙirar Kalmar Sirri Bazuwa

Tsarin tsarin yawanci ya ƙunshi: 1) ƙirƙirar haruffa don cika ƙayyadaddun ƙayyadaddun saiti, 2) cika sauran tsawon lokaci daga saitin da aka yarda, da 3) aiwatar da matakin jujjuyawa na ƙarshe. Misali, tsarin Chrome da farko yana gamsar da mafi ƙarancin, sannan yana ɗaukar samfuri daga haɗin saitin da ba a kai ga matsakaicin su ba, kuma a ƙarshe yana jujjuya kirtani. Muhimmin rauni yana cikin yanayin ad-hoc na waɗannan matakan da yuwuwar son zuciya a cikin samfurin bazuwa, wanda ba a taɓa yin bincike a tsari ba.

3. Hanyar Tabbatarwa ta Tsari

Muna ɗaukar hanyar tabbatar da sirri ta tushen wasa a cikin mataimakin tabbatar da EasyCrypt. Hanyar ta ƙunshi:

Bayani: Ayyana tsarin tsarin RPG a tsari da buƙatun tsaro.
Aiwatarwa: Rubuta tsarin a cikin harshen EasyCrypt.
Tabbatarwa: Tabbatar cewa aiwatarwa ta gamsar da bayaninta. Wannan ya haɗa da:
- Daidaiton Aiki: Sakamakon koyaushe yana cika ka'idar mai amfani.
- Tsaro (Bazuwa): Sakamakon ba za a iya bambanta shi da kirtani bazuwa na gaskiya na ka'ida ɗaya ba, idan aka ɗauka mai ƙirƙirar lamba bazuwa mai tsaro (RNG). An ƙirƙira wannan a matsayin wasa mai yuwuwa inda abokin gaba ba zai iya bambanta sakamakon RPG daga bazuwa ba.

Wannan yana canza amana daga bitar code da gwaji zuwa tabbacin lissafi.

4. Shawarar Aiwatar da Magana

Takardar tana ba da shawarar tsarin RPG guda ɗaya, mai sassa wanda aka tsara don tabbatarwa. Muhimman fasalullukansa sun haɗa da:

Ƙaddamar da Ka'ida: Tsarin bayanai na tsari wanda ke wakiltar duk ƙayyadaddun mai amfani.
Ƙirƙirar Mataki Biyu: Matakin tabbataccen gamsarwa don mafi ƙarancin, sannan matakin samfurin daidaitaccen mataki don sauran ramuka.
Jujjuyawar Tabbacce: Matakin jujjuyawa na ƙarshe tare da tabbataccen daidaito.

Aiwatarwa a cikin EasyCrypt yana aiki a matsayin "ma'auni na zinariya" wanda za a iya kwatanta ko ma samo tsarin kasuwanci da shi.

5. Sakamakon Gwaji & Bayanin Ginshiƙi

Yayin da PDF ta mai da hankali kan shawarar tsari, sakamakon gwaji da ake nufi shi ne nasarar tabbatar da aiwatar da magana a cikin EasyCrypt. "Ginshiƙi" na wannan aikin shine tsarin tabbatarwa da kansa.

Zanen Tsarin Tabbatar da Tabbaci

Kwararar Ra'ayi: Ana iya ganin tabbatarwa a matsayin jadawali mai jagora na dogaro na ma'ana.
1. Tushen Nodes (Zato): Tsaron tushen CSPRNG (Mai Ƙirƙirar Lamba Bazuwa Mai Tsaro na Sirri).
2. Tsaka-tsaki Nodes (Lemmas): Kaddarorin ƙananan hanyoyin (misali, "samfurin ba tare da maye gurbin daga saiti yana haifar da zaɓin abu daidai").
3. Node na Ƙarshe (Ka'ida): Babban ka'idar tsaro: Tsarin RPG ba za a iya bambanta shi da mai ƙirƙirar kirtani bazuwa na manufa a ƙarƙashin ka'idar da aka ayyana ba.
Kowane kibiya yana wakiltar matakin tabbatarwa na tsari a cikin EasyCrypt. Cikar wannan jadawali ita ce sakamakon gwaji na farko, yana nuna babu rassan ma'ana da suka ɓace tsakanin zato da da'awar tsaro ta ƙarshe.

6. Cikakkun Bayanai na Fasaha & Tsarin Lissafi

An tsara ainihin kaddarar tsaro a matsayin wasan rashin bambanci. Bari $\mathcal{A}$ ya zama abokin gaba mai lokaci mai yuwuwar polynomial. Bari $\text{RPG}(\text{ka'ida})$ ya zama tsarin mu kuma $\text{RAND}(\text{ka'ida})$ ya zama mai ƙirƙira mai kyau wanda ke fitar da kirtani bazuwa cikakke wanda ke gamsar da ka'ida.

An ayyana wasan $\text{IND}^{\text{RPG}}_{\mathcal{A}}$ kamar haka:
1. Mai kalubalantar ya jefa tsabar kudi $b \xleftarrow{\$} \{0,1\}$.
2. Idan $b=0$, mai kalubalantar ya ba $s \leftarrow \text{RPG}(\text{ka'ida})$ zuwa $\mathcal{A}$.
3. Idan $b=1$, mai kalubalantar ya ba $s \leftarrow \text{RAND}(\text{ka'ida})$ zuwa $\mathcal{A}$.
4. $\mathcal{A}$ ya fitar da zato $b'$.
$\mathcal{A}$ ya ci nasara idan $b' = b$.

An ayyana fa'ida na abokin gaba kamar haka: $$\mathbf{Adv}^{\text{ind}}_{\text{RPG}}(\mathcal{A}) = \left| \Pr[\mathcal{A} \text{ ya ci nasara}] - \frac{1}{2} \right|$$

Manufar tabbatarwa ita ce a nuna cewa wannan fa'idar ba ta da mahimmanci ga duk $\mathcal{A}$ mai inganci, a ƙarƙashin zaton cewa ainihin mai tsinkaya bazuwa ko PRF yana da tsaro. Ana samun wannan ta hanyar jerin tsalle-tsalle na wasa, inda kowane tsalle yana canza ainihin wasan zuwa wanda yake daidai da ma'ana ko wanda bambancin ya tabbata ba shi da mahimmanci.

7. Tsarin Bincike: Misalin Lamari

Yanayi: Bincika fasalin "Keɓance Haruffa Masu Kama" a cikin tsarin Chrome.
Tsarin Tsari: Bari cikakken saitin haruffa ya zama $C$. Rukunin "mai kama" shine $S \subset C$. Saitin da aka yarda shine $A = C \setminus S$.
Yiwuwar Aibi (Ba tare da Tabbatarwa ba): Dole ne tsarin ya tabbatar da samfurin daidai daga $A$. Aiwatarwa marar hankali na iya: 1. Samfurin daga $C$. 2. Idan samfurin yana cikin $S$, ƙi kuma sake ɗaukar samfurin. Wannan yana daidai ne kawai idan samfurin daga $C$ yana daidai kuma an tabbatar da madauki na ƙin yarda zai ƙare. A cikin yanayi mai yanayi ko son zuciya na RNG, wannan na iya fitar da bayanai ko haifar da rashin ƙarewa.
Hanyar Tabbatarwa: Aiwatarwa da aka tabbatar ta tsari zata: 1. Sami sharadi na farko cewa $A$ ba komai bane. 2. Kai tsaye ɗauki samfurin daga rarraba daidai akan $A$ ta amfani da tabbataccen canjin sakamakon RNG. 3. Haɗa da tabbataccen tabbacin inji cewa rarraba sakamakon yana daidai akan $A$ kuma ya kasance mai zaman kansa daga $S$.
Wannan lamarin yana kwatanta yadda tabbatarwa ta tsari ke tilasta sarrafa ɓangarorin gefe (komai $A$) da kuma tabbatar da kaddarar tsaro da ake nufi (daidaito).

8. Ra'ayin Mai Binciken Masana'antu

Mahimmin Fahimta: Masana'antar manajan kalmar sirri an gina ta ne bisa tushen amana da ake nufi, ba tabbataccen tsaro ba. Wannan takarda ta gano daidai cewa mai ƙirƙirar kalmar sirri shine mabuɗin amana mai mahimmanci, amma an yi watsi da shi ta hanyar tsari. Ainihin fahimta ba shine sarkakiyar hanyoyin ba—sau da yawa suna da sauƙi—amma babu tabbataccen garantin lissafi don irin wannan aikin mai mahimmanci na tsaro. Yana kama da gina rumbun banki amma ana amfani da makullin da kayan aikinsa kawai an duba shi ta hanyar duba shi, ba a gwada shi da zane-zanen injiniya ba.

Kwararar Ma'ana: Hujja tana da ban sha'awa: 1) Amana ita ce babbar shingen amfani da PM. 2) RPG shine muhimmin fasali da ke tasiri amana. 3) RPGs na yanzu ana aiwatar da su tare da mafi kyawun ƙoƙarin code, ba ƙirar da aka tabbatar ba. 4) Saboda haka, tabbatar da tsarin RPG wata hanya ce kai tsaye, mai tasiri don ƙara amana. Kwararar daga matsala (rashin amincewar mai amfani) zuwa magani (tabbatarwa) yana bayyana kuma yana da kyakkyawar dalili. Zaɓin EasyCrypt da tabbatarwa na tushen wasa yana da inganci, yana daidaitawa da kafaffen ayyuka a cikin sirri da aka tabbatar kamar aiwatarwa da aka tabbatar a cikin ayyuka kamar HACL*.

Ƙarfi & Aibobi:
Ƙarfi: Takardar tana magance matsala ta gaske, mai matuƙar mahimmanci tare da ingantacciyar hanya. Bayar da aiwatar da magana da aka tabbatar yana da aiki fiye da zargi kawai. Mai da hankali kan shugabannin buɗe tushe (Chrome, Bitwarden, KeePass) yana sa binciken ya zama takamaiman kuma ya dace.
Aibobi: Giwa a cikin daki shine haɗin kai. Tsarin tsari da aka tabbatar ba shi da ma'ana idan tsarin da ke kewaye—UI, ɓoyayyen bayanan kalmar sirri, tsarin cika ta atomatik—yana da rauni. Takardar a ɓoye tana ɗauka cewa "tsaftataccen" tushen sirri, amma yawanci cin zarafi na duniya suna kaiwa ga code na manne, kamar yadda aka gani a cikin raunin ƙari na burauza daban-daban. Bugu da ƙari, ba a tattauna aikin tsarin da aka ba da shawarar da na hasashe ba; tabbatarwa na iya ƙara kaya.

Fahimta Mai Aiki:
1. Ga Masu Sayar da PM: Karɓi ko bincika tare da aiwatar da magana da aka tabbatar. Fara ɗaukar RPG a matsayin na'urar sirri, ba kawai aikin amfani ba. Ku ba da kuɗin ƙoƙarin tabbatarwa na ciki ko bincike da aka mai da hankali kan wannan bangare.
2. Ga Ƙungiyoyin Ma'auni (misali, NIST, FIDO): Ƙirƙira da buga cikakkun bayanai na tsari don ƙirƙirar kalmar sirri. Jagororin na yanzu (misali, NIST SP 800-63B) sun dogara ne akan rubutu; bayanin da za a iya tabbatar da injin zai zama mai canza wasa.
3. Ga Masu Binciken Tsaro: Matsa daga gwajin RPG na akwatin baƙar fata zuwa duba ƙirarsu daidai da ƙirar da aka tabbatar. Jerin abubuwan da aka yi bita daga binciken ka'idar wannan takarda yana ba da farawa.
4. Ga Masu Bincike: Tsawaita wannan aikin zuwa sama don tabbatar da tattara entropy/tsaba na RNG da ƙasa don tabbatar da duk tsarin sarrafa kalmar sirri. Babban manufa ya kamata ya zama manajan kalmar sirri mai tabbatarwa daga ƙarshe zuwa ƙarshe, wanda ayyuka a cikin software na tsarin da aka tabbatar ke nuna shi.

9. Aikace-aikace na Gaba & Hanyoyin Bincike

Tasirin wannan aikin ya wuce manajoji na kalmar sirri:

Shaidar Ba tare da Kalmar Sirri ba: Babbar matsala ta ƙirƙirar da sarrafa alamun sirri (misali, don lambobin baya na WebAuthn) iri ɗaya ne. Hanyoyin ƙirƙira da aka tabbatar za su zama mahimmanci ga waɗannan tsare-tsare.

Shirye-shiryen Na'urar IoT: Yawan turawa na na'urorin IoT sau da yawa yana amfani da tsoffin kalmar sirri da aka ƙirƙira ta hanyar tsari. Mai ƙirƙira da aka tabbatar zai iya kawar da gaba ɗaya nau'in raunin takaddun shaida na asali.

Haɗin kai tare da Tsaron Kayan Aiki: RPGs na gaba za a iya aiwatar da su azaman code da aka tabbatar yana gudana a cikin Yanayin Aikin Amincewa (TEE) ko abu mai tsaro, tare da tabbatattun hujjoji suna faɗaɗa zuwa musanya kayan aiki.

Ka'idoji Masu Daidaitawa: Ana buƙatar bincike cikin hanyoyin da aka tabbatar ta tsari waɗanda za su iya daidaita ka'idoji bisa ga bayanan barazana na ainihin lokaci ko buƙatun takamaiman gidan yanar gizo yayin kiyaye garantin tsaro.

Haɗin Ƙira na Amfani-Tabbatarwa: Kalubale na gaba shine ƙirar ƙira da tabbatar da kaddarorin da suka shafi amfani, kamar ƙwaƙwalwar kalmar sirri (don dalilai na baya) da nau'in rubutu akan madannai daban-daban, tabbatar da cewa waɗannan "taushi" ƙayyadaddun ba su haifar da lahani na tsaro ba.

Hanyar tana nuna zuwa gaba inda muhimman sassan software na tsaro ba kawai buɗe tushe ba ne amma suna zuwa tare da tabbatattun hujjojin injin na ainihin kaddarorinsu, suna ƙara bayyana gaskiya da amana lokaci guda.

10. Nassoshi

Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Zuwa Tabbatar da Tsarin Hanyoyin Ƙirƙirar Kalmar Sirri da ake amfani da su a cikin Manajoji na Kalmar Sirri. arXiv preprint arXiv:2106.03626v2.

Bhargavan, K., et al. (2017). HACL*: ɗakin karatu na sirri na zamani da aka tabbatar. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17).

Grassi, P. A., et al. (2017). Jagororin Asalin Dijital: Tabbatar da gaskiya da Sarrafa Rayuwa (NIST Special Publication 800-63B). Cibiyar Ƙididdiga da Fasaha ta Ƙasa.

Chothia, T., et al. (2016> Gano Lahani a cikin Ƙarin Burauza ta atomatik. IEEE Tsaro & Sirri.

Bellare, M., & Rogaway, P. (2006). Tsaron Ƙirƙirar Lambobi Uku da Tsarin Tabbatar da Wasan Code. Ci gaban Sirri – EUROCRYPT 2006.

Mataimakin Tabbatar da EasyCrypt. (n.d.). An samo daga https://easycrypt.info/