{"id":184113,"date":"2026-11-03T23:41:02","date_gmt":"2026-11-03T21:41:02","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/kriptograficheskij-izolyator-itb-s-formalnym-dokazatelstvom-nadyozhnosti"},"modified":"2026-11-03T23:41:07","modified_gmt":"2026-11-03T21:41:07","slug":"itb-cryptographic-isolator-with-formally-proven-reliability","status":"publish","type":"post","link":"https:\/\/prohoster.info\/sq\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Kryptografik izoluese ITB me prov\u00eb formale t\u00eb besueshm\u00ebris\u00eb","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Projekti ITB \u00ebsht\u00eb prezantuar, duke zhvilluar nj\u00eb izoluese simetrike kriptografike, e cila \u00ebsht\u00eb menduar p\u00ebr t\u00eb mb\u00ebshtjell\u00eb funksionet standarde pseudoprasuese (PRF) dhe primitivat hash (AES, BLAKE2\/3, Areion dhe t\u00eb tjer\u00eb) n\u00eb nj\u00eb barrier\u00eb t\u00eb kombinuar dhe topologjike. Ndryshe nga m\u00ebnyrat klasike t\u00eb enkriptimit t\u00eb bllokave dhe rrjedh\u00ebs, arkitektura ITB \u00ebsht\u00eb fokusuar n\u00eb izolimin struktural t\u00eb primitivit t\u00eb brendsh\u00ebm, duke e penguar p\u00ebrhapjen e karakteristikave diferenciale dhe linjare, linjizimin algebrik, si dhe kodifikimet direkte p\u00ebr zgjidh\u00ebsit SAT\/SMT dhe MILP p\u00ebrmes kufijve t\u00eb barrier\u00ebs. Kodi \u00ebsht\u00eb shkruar n\u00eb gjuh\u00ebn Go me optimizime t\u00eb nivelit t\u00eb ul\u00ebt n\u00eb assembler p\u00ebr arkitat x86_64 dhe ARM64 (Aarch64) dhe shp\u00ebrndahet n\u00ebn licenc\u00ebn Apache 2.0.<\/p>\n
Transformimi i t\u00eb dh\u00ebnave n\u00eb ITB \u00ebsht\u00eb i ndar\u00eb n\u00eb dy nivele t\u00eb lidhura (Interlocked Barrier), t\u00eb menaxhuara nga tet\u00eb \u00e7el\u00ebsa t\u00eb izoluara (8-seed isolation) me evolucionin lokal t\u00eb \u00e7el\u00ebsit p\u00ebrmes nj\u00eb zinxhiri me lidhje t\u00eb drejtp\u00ebrdrejt\u00eb (ChainHash). N\u00eb nivelin e par\u00eb, bari i renditjes (Rank Barrier) kryen nj\u00eb permutacion ky\u00e7 kombinuese t\u00eb \u00e7do blloku 48-bit (ose bllokut 168-bit p\u00ebr primitiv\u00ebt 512-bit), duke shp\u00ebrndar\u00eb bit\u00ebt e tekstit t\u00eb hapur n\u00eb tri rajone t\u00eb pavarura mbi baza t\u00eb dyshkall\u00ebshit t\u00eb gjetjes s\u00eb kombinimit sipas numrit t\u00eb tij (hap\u00ebsira e ndarjeve t\u00eb balancuara C(48, 16) * C(32, 16) \u00ebsht\u00eb rreth 2^70.20, nd\u00ebrsa n\u00eb modin 168-bit C(168, 56) * C(112, 56) \u2014 rreth 2^258.60). N\u00eb nivelin e dyt\u00eb, bari pixel (Pixel Barrier) shfaq t\u00eb dh\u00ebnat n\u00eb nj\u00eb rrjet t\u00eb elementeve 8-bajt\u00eb (8 kanale me 7 bit t\u00eb dh\u00ebnash dhe 1 bit zhurmash pseudo-rast\u00ebsore n\u00eb secil\u00ebn byte) me nj\u00eb ciklik t\u00eb shtyr\u00eb android p\u00ebr \u00e7el\u00ebsin 7-bit, maskimin e kanaleve 7-bit dhe zgjedhjen e pozicionit t\u00eb bitit t\u00eb zhurm\u00ebs.<\/p>\n
Karakteristikat kryesore t\u00eb projektit:<\/p>\n
\n
Verifikimi eksperimental i pronave izoluese mbi funksione q\u00eb nuk jan\u00eb kriptografike (stestim me primitivat e dob\u00ebt). N\u00eb p\u00ebrb\u00ebrje t\u00eb repositorit \u00ebsht\u00eb p\u00ebrfshir\u00eb nj\u00eb stend laboratorike, e cila vendos brenda barrier\u00ebs nj\u00eb funksion hash t\u00eb zakonsh\u00ebm FNV-1a. N\u00ebp\u00ebrmjet p\u00ebrzierjes jo-lineare kombinatoriale, ndarjes s\u00eb bajt\u00ebve n\u00eb kufijt\u00eb e kanaleve 7-bit (GCD(7, 8) = 1) dhe injektimit t\u00eb bit\u00ebve t\u00eb zhurm\u00ebs n\u00eb \u00e7do bajt, qasja praktike ose nd\u00ebrtimi i nj\u00eb modeli zgjidhen SAT\/SMT p\u00ebr tekstin e hapur dhe t\u00eb enkriptuar bllokohet tashm\u00eb n\u00eb faz\u00ebn e formulimit t\u00eb sistemit t\u00eb barazimeve.\n
Verifikimi formal i kontrolluar nga makina n\u00eb gjuh\u00ebn Lean 4. T\u00eb gjitha 12 teoremat baz\u00eb matematikore, kombinatorike dhe t\u00eb vektor\u00ebve bita, konstrukti (si dhe skema praktike e konfirmimit hibrid t\u00eb \u00e7el\u00ebsave 3-8 nga tre kanale KEM t\u00eb pavarura n\u00eb APPS.md), t\u00eb p\u00ebrshkruara n\u00eb dokumentin PROOFS.md, jan\u00eb provuar plot\u00ebsisht n\u00eb Lean 4 pa p\u00ebrdorimin e aksioneve dhe duke l\u00ebn\u00eb jasht\u00eb prova.\n
Instrumenti i nd\u00ebrtuar p\u00ebr provimin kriptoanalitik, duke p\u00ebrfshir\u00eb kontrollime automatike: bateri testesh statistikore, vler\u00ebsim t\u00eb grad\u00ebs algebrike dhe nonlinearitetit, kontrollimin e izolimit t\u00eb farave kur filtrohen pozitat e zhurm\u00ebs p\u00ebrmes CCA-orakulli dhe k\u00ebrkimin e dob\u00ebsive p\u00ebrmes zgjidh\u00ebsve t\u00eb jasht\u00ebm.\n
Dy modulet e pun\u00ebs: moda standarde e autentifikimit (AEAD sipas skem\u00ebs MAC-Inside-Encrypt, ku imtimimi llogaritet dhe enkriptohet brenda kontejnerit) dhe moda e mohimit t\u00eb besuesh\u00ebm (Plausible Deniability) mbi baz\u00ebn e kodifikimit t\u00eb pavendosur COBS, ku dekriptimi me nj\u00eb \u00e7el\u00ebs t\u00eb gabuar nxjerr t\u00eb dh\u00ebna sintaksisht t\u00eb sakta pa tregues gabimi.\n