Loading...
Mfululizo: Mfululizo wa Uthibitishaji Rasmi · Sehemu ya 1 kati ya 3 Hadhira: wanaoanza kabisa. Hakuna maarifa ya hisabati, upangaji programu, au kriptografia yanayodhaniwa. Utakachoondoka nacho: uelewa wazi wa maana ya kuthibitisha programu sahihi, kwa nini hilo ni tofauti kimsingi na kuijaribu, thibitisho linalokaguliwa na mashine ni nini, na mipaka mahususi (na ya uaminifu) ya kile ambacho thibitisho kama hilo linaweza kuahidi.
Programu nyingi huaminiwa kwa sababu zimejaribiwa: tunaziendesha kwa ingizo nyingi na kuzitazama zikifanya kazi. Uthibitishaji rasmi [Formal Verification] unauliza swali la ujasiri zaidi. Je, tunaweza kuthibitisha, kwa uhakika wa kihisabati, kwamba mfumo hufanya unachopaswa kufanya kwa kila ingizo linalowezekana, ikiwemo zile ambazo hakuna mtu aliyewahi kufikiria kujaribu? Makala haya yanajenga wazo hilo kuanzia misingi. Intuisheni kwanza, hakuna alama hadi zitakapostahili.
Hii ni simulizi ya kweli, na ndiyo sababu mfululizo huu upo.
Mnamo 2022, sarafu-fiche inayolenga faragha Zcash ilizindua bwawa jipya la faragha lililoitwa Orchard, likiwawezesha watu kufanya miamala huku kiasi kikiwa kimefichwa. Kwa miaka minne lilifanya kazi bila kasoro na lilipita ukaguzi wa kitaalamu wa kurudiwa. Kisha, mnamo Mei 2026, mtafiti wa usalama aliyefikiri kwa uangalifu kuhusu hisabati ya msingi (kwa msaada wa zana za AI) aligundua sehemu moja isiyowekewa vikwazo vya kutosha katika hisabati ya mfumo. Pengo hilo moja lingeweza kumruhusu mshambulizi kuunda kiasi kisicho na kikomo cha fedha bandia, na kwa sababu kiasi kilifichwa, hakuna ambaye angeona hilo likitokea. Kasoro hiyo ilikuwepo wakati wote.
Haikugunduliwa kwa majaribio. Kila jaribio lilikuwa limepita kwa miaka minne. Iligunduliwa na mtu aliyefikiria kuhusu hisabati. Na timu ilipoirekebisha, haikupachika tu marekebisho na kuendelea. Waliandika thibitisho la kihisabati lililokaguliwa na mashine, lenye zaidi ya nadharia binafsi 2,700, kwamba mbadala huo haungeweza kuwa na aina hiyo ya kasoro kabisa.
Huo ndio uthibitishaji rasmi, na hiki ndicho unachokupatia: si “tulijaribu hali nyingi na zikafanya kazi,” bali “tulithibitisha kuwa inashikilia kwa kila hali.” Kwa mifumo ambamo hali moja iliyokosekana ni janga (fedha, ndege, vifaa vya matibabu, kriptografia), tofauti hiyo ni kila kitu.
Eneo lisiloonekana katika majaribio lilipewa jina miongo kadhaa iliyopita na mwanasayansi wa kompyuta Edsger Dijkstra, na bado ni kweli:
Majaribio yanaweza kuonyesha uwepo wa hitilafu, lakini kamwe si kutokuwepo kwake.
Jaribio linapopita, umejifunza kwamba mfumo hufanya kazi kwa ingizo hilo. Hujajifunza chochote kuhusu ingizo ambazo hukujaribu, na hitilafu hatari karibu daima huwa katika hali ambazo hakuna aliyejaribu.
Fikiria una wajibu wa jengo lenye milango elfu moja, na kazi yako ni kuhakikisha kila mlango umefungwa usiku.
Tofauti iko kati ya kuchukua sampuli ya uhalisia na kuthibitisha sifa ya usanifu. Majaribio huchukua sampuli. Uthibitishaji rasmi huthibitisha. Hilo ndilo wazo zima, na kila kitu kingine ni mitambo ya kulifanya kwa ukali.
Kila uthibitishaji rasmi, haijalishi umeendelea kiasi gani, hujengwa kwa viambato vitatu hasa. Vishike hivi kwa uwazi na yaliyobaki ni maelezo.
| Nguzo | Maana rahisi | Mfano wa jengo |
|---|---|---|
| Ubainishaji | Kauli sahihi ya maana ya “usawa” | “Kila mlango lazima ufunge usiku” |
| Mfumo | Kitu halisi kinachokaguliwa (programu, saketi, itifaki) | Jengo na utaratibu wake wa kufunga |
| Thibitisho | Hoja kali kwamba mfumo daima hutimiza ubainishaji | Uonyeshaji wa kimantiki kwamba kubonyeza “funga” hufunga milango yote |
Na kiambato cha nne, kisicho na kelele, hufanya jambo lote liaminike:
Wasaidizi wa thibitisho ambao unaweza kusikia wakitajwa ni pamoja na Lean, Rocq (zamani Coq), na Isabelle. Kwa hakika, ni injini kali sana za kukagua mantiki. Thibitisho la Zcash katika simulizi letu la mwanzo liliandikwa kwa Lean. Kwa kutambulika, miundo ya kisasa ya AI inazidi kutumiwa kusaidia kuandika thibitisho hizi, huku binadamu wakiziongoza, jambo ambalo limepunguza juhudi zilizokuwa zikichukua miaka hadi wiki. Mashine bado hukagua kila hatua, kwa hiyo uharakishaji huo haupunguzi uhakika wowote.
Neno “thibitisho” linaweza kuonekana kutisha, kwa hiyo tuliondoe fumbo kwa mfano thabiti unaoweza kukaguliwa. Hakuna kriptografia, ni hesabu za shule tu.
Dai: kwa kila nambari nzima n, jumla 0 + 1 + 2 + ... + n ni sawa na n(n+1)/2.
Unaweza kujaribu hili. n = 5 hutoa 0+1+2+3+4+5 = 15, na 5 × 6 / 2 = 15. ✓ Inalingana. Jaribu n = 10: jumla ni 55, na fomula hutoa 10 × 11 / 2 = 55. ✓ (Hivi vinahesabiwa na kuthibitishwa; dai kwa kweli hushikilia kwa kila n kuanzia 0 hadi 999 vinapokaguliwa moja kwa moja.)
Lakini kujaribu thamani, hata elfu moja kati yake, hakufikii “kwa kila nambari nzima.” Zipo zisizo na ukomo. Thibitisho huziba pengo hilo lisilo na ukomo kwa hoja yenye kikomo, kwa kutumia mbinu inayoitwa induction [induction]:
n = 0, jumla ni 0 tu, na fomula hutoa 0 × 1 / 2 = 0. Zinalingana. ✓k. Sasa ongeza nambari inayofuata, k+1. Jumla hadi k+1 ni (sum up to k) + (k+1) = k(k+1)/2 + (k+1). Mstari mmoja wa aljebra hupanga upya hili kuwa (k+1)(k+2)/2, ambayo ni fomula yenyewe hasa huku k+1 ikichukua nafasi ya k. ✓Kwa kuwa hushikilia mwanzoni (0) na kila hatua huipeleka hadi nambari inayofuata, hushikilia kwa nambari nzima zote, milele, katika hoja moja yenye kikomo. Hilo ni thibitisho. Msaidizi wa thibitisho hufanya hoja hii hasa, lakini huhakiki kimitambo kwamba kila hatua, ikiwemo “mstari wa aljebra,” hufuata kwa kweli kutokana na yaliyotangulia.
Kuruka kwa fikra kunakostahili kueleweka: thibitisho hubadilisha “hali zisizo na ukomo” kuwa hoja yenye kikomo, inayoweza kukaguliwa. Huo ndio uwezo wa kipekee ambao majaribio hayana kimuundo.
Uthibitishaji rasmi una nguvu kwa kiasi fulani kutokana na utambuzi unaofafanua ambapo hitilafu hutoka kwanza. Kasoro yoyote katika mfumo wa kukagua kanuni hufuatilia hadi mojawapo ya sehemu tatu:
| Chanzo cha hitilafu | Maana yake | Je, tunaweza kuithibitisha iondoke? |
|---|---|---|
| Ubainishaji | Hisabati au kanuni zenyewe si sahihi (sharti linalokosekana, ufafanuzi mbaya) | Ndiyo, moja kwa moja; hapa ndipo uthibitishaji rasmi hustawi |
| Utekelezaji | Msimbo unashindwa kutekeleza kwa uaminifu ubainishaji sahihi | Kwa sehemu; mara nyingi kushindwa huko huacha ushahidi unaoweza kugundulika |
| Dhana iliyovunjika | Kitu ambacho mfumo mzima hutegemea kinageuka kuwa si kweli | Hapana; dhana ndizo msingi usioweza kupunguzwa |
Uainishaji huu una maana zaidi kuliko unavyoonekana, na Sehemu za 2 na 3 huzingatia hilo. Hitilafu za kina zaidi na hatari zaidi, zile zinazoweza kujificha milele, huwa zinaishi katika ubainishaji: maelezo ya kihisabati ya kile ambacho mfumo unapaswa kufanya. Na ubainishaji ndio hasa ambao thibitisho lililokaguliwa na mashine linaweza kuchunguza moja kwa moja, hali zote kwa wakati mmoja. Hiyo ndiyo sababu juhudi makini za uthibitishaji rasmi hulenga hapo kwanza.
Uthibitishaji rasmi una nguvu, lakini ahadi yake ni mahususi, na kuielewa vibaya huwapotosha watu. Kwa hiyo iseme kwa uangalifu:
Thibitisho huhakikisha kwamba mfumo hutimiza ubainishaji, chini ya dhana zilizotajwa. Hakuna zaidi.
Matokeo manne hufuata, na kila moja ni muhimu:
Mbali na kudhoofisha uthibitishaji rasmi, usahihi huu ndio nguvu yake. Hukwambia hasa unachopata. Kama tutakavyoona katika Sehemu ya 3, timu ya Zcash inayotaja wazi wigo na dhana zake (“tulithibitisha uimara wa ugavi, chini ya dhana hizi zilizopewa majina, na si faragha”) ni mfano wa uaminifu huo.
Ili kuweka hili lisomeke tulirahisisha. Ubainishaji halisi huandikwa katika lugha rasmi sahihi, si sentensi za Kiingereza; kuna mitindo kadhaa ya uthibitishaji rasmi (uthibitishaji shirikishi wa nadharia, ukaguzi wa miundo, mbinu zinazotegemea SMT) inayofaa kwa matatizo tofauti; na kuandika thibitisho hizi bado ni kazi inayohitaji ustadi na juhudi hata kwa msaada wa AI. Pia tuliruka jinsi msaidizi wa thibitisho huwakilisha mantiki ndani yake. Hakuna kati ya haya yanayobadilisha kiini: ubainishaji, mfumo, na thibitisho lililokaguliwa na mashine kwamba vitu hivyo viwili vinakubaliana, chini ya dhana zilizotajwa. Maelezo yatarejea tutakapoyahitaji.
| Istilahi | Maana rahisi kwa Kiingereza |
|---|---|
| Formal verification | Kuthibitisha, kihisabati, kwamba mfumo hutimiza ubainishaji kwa hali zote |
| Specification | Kauli sahihi ya maana ya “tabia sahihi” |
| System | Programu halisi, saketi, au itifaki inayokaguliwa |
| Proof | Mlolongo wenye kikomo wa hatua za kimantiki unaoanzisha dai kwa hali zote |
| Proof assistant / theorem prover | Programu (Lean, Rocq, Isabelle) inayokagua kila hatua ya thibitisho |
| Machine-checked | Imethibitishwa hatua kwa hatua na kompyuta, si kwa kusomwa na binadamu pekee |
| Induction | Mbinu ya uthibitisho: ni kweli mwanzoni, na kila hatua huipeleka hadi inayofuata |
| Assumption | Sharti ambalo thibitisho hutegemea; likiwa si kweli, dhamana huenda isishikilie |
Je, uthibitishaji rasmi unachukua nafasi ya majaribio? Hapana. Hukamilishana. Majaribio hugundua matatizo ya kiutendaji na dhana potofu kwa gharama ndogo; uthibitishaji huondoa aina nzima za hitilafu ambazo majaribio yanaweza yasichukue kamwe kama sampuli.
Ikiwa una nguvu sana, kwa nini kila kitu hakithibitishwi rasmi? Ni ghali na huhitaji ustadi wa wataalamu, ingawa msaada wa AI unapunguza gharama hiyo. Huhifadhiwa kwa mifumo ambamo hitilafu nadra ingekuwa janga, ambako gharama yake hulipa hasa.
Je, mfumo uliothibitishwa rasmi bado unaweza kushindwa? Ndiyo, ikiwa ubainishaji ulikuwa mbaya, ufafanuzi ulielezwa vibaya, dhana haikushikilia, au kushindwa kuko nje ya kilichobainishwa. Thibitisho hufunika tu kile kinachodai kufunika.
Je, thibitisho lililokaguliwa na mashine linaaminika zaidi kuliko la binadamu? Kwa thibitisho kubwa na tata, kwa kawaida ndiyo. Mashine haitapuuza pengo dogo au kukubali kauli isiyo na uthibitisho, ingawa bado huamini ubainishaji na fafanuzi ilizopewa.
Ikiwa AI husaidia kuandika thibitisho, kwa nini uliamini? Kwa sababu msaidizi wa thibitisho hukagua kila hatua kimitambo. AI hupendekeza hatua; mashine huzithibitisha. Hatua isiyo sahihi hukataliwa tu, kwa hiyo AI huharakisha kazi bila kudhoofisha dhamana.
Unathibitisha kwamba programu ya benki “kamwe hairuhusu salio la akaunti kuwa hasi.” Mwaka mmoja baadaye, fedha bado zinapotea. Je, yote mawili yanawezaje kuwa kweli kwa wakati mmoja? (Jibu hapa chini.)
Thibitisho lilihakikisha sifa moja hasa: masalio kamwe hayawi hasi. Fedha zinaweza kupotea kwa njia ambazo sifa hiyo haikushughulikia kamwe, kwa mfano hitilafu inayohamisha fedha hadi akaunti isiyo sahihi (ambayo bado si hasi), au kasoro katika sehemu ya mfumo ambayo haikubainishwa kamwe. Uthibitishaji ulifanya hasa ulichokuwa umeahidi na hakuna zaidi. Hii ni tahadhari ya Sehemu ya 6 ikifanya kazi: thibitisho hufunika ubainishaji, si kila wazo linalowezekana la “usawa.”
Sehemu ya 2 · Hitilafu ya Orchard: tunageukia simulizi halisi la 2026 kwa ukamilifu. Mfumo wa faragha ulificha kiasi kwa kutumia thibitisho za kriptografia, na mstari mmoja usiowekewa vikwazo vya kutosha katika hisabati yake ulimaanisha kuwa thibitisho hizo zingeweza kufanywa ziseme uongo, zikuruhusu kughushi kusikoonekana bila kikomo. Tutaona hasa maana ya “saketi isiyowekewa vikwazo vya kutosha,” kwa nini aina hii ya hitilafu inaweza kujificha milele, na kwa nini imetokea zaidi ya mara moja.
Sehemu ya Mfululizo wa Uthibitishaji Rasmi kwa ZecHub.