{"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\/da\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"ITB kryptografisk isolator med formelt bevis for p\u00e5lidelighed","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Projektet ITB pr\u00e6senterer en symmetrisk kryptografisk isolator, der er designet til at indkapsle standard pseudotilf\u00e6ldige funktioner (PRF) og hash-primitiver (AES, BLAKE2\/3, Areion og andre) i en sammenkoblet kombinatorisk og topologisk barriere. I mods\u00e6tning til klassiske blok- og str\u00f8m-krypteringsmetoder sigter ITB-arkitekturen mod strukturel isolation af den interne primitive, hvilket forhindrer spredning af differentielle og line\u00e6re egenskaber, algebraisk linearisering samt direkte kodninger for SAT\/SMT og MILP-l\u00f8sere gennem barrierens gr\u00e6nser. Koden er skrevet i Go-sprog med lavniveauoptimeringer i assembler til x86_64 og ARM64 (Aarch64) arkitekturer og distribueres under Apache 2.0-licensen.<\/p>\n
Datakonvertering i ITB er opdelt i to sammenkoblede niveauer (Interlocked Barrier), styret af otte isolerede n\u00f8gle-s\u00e6d (8-seed isolation) med lokal n\u00f8gle-evolution gennem en k\u00e6de med direkte forbindelse (ChainHash). P\u00e5 det f\u00f8rste niveau udf\u00f8rer rangbarrikaden (Rank Barrier) en n\u00f8glekombinatorisk permutasjon af hver 48-bit blok (eller 168-bit blok for 512-bit primitive), hvor bittene fra klartekst fordeles i tre uafh\u00e6ngige regioner baseret p\u00e5 en to-trins kombination i henhold til sit nummer (rummet af balancerede partitioner C(48, 16) * C(32, 16) udg\u00f8r omkring 2^70.20, og i 168-bit modulet C(168, 56) * C(112, 56) \u2014 omkring 2^258.60). P\u00e5 det andet niveau kortl\u00e6gger pixelbarrieren (Pixel Barrier) data til et gitter af 8-byte elementer (8 kanaler med 7 bit data og 1 bit pseudorandom st\u00f8j i hver byte) med et pixel-for-pixel n\u00f8gle 7-bit cyklisk forskydning, maskerering af 7-bit kanaler og valg af st\u00f8jbit position.<\/p>\n
Hovedtr\u00e6k ved projektet:<\/p>\n
\n
Eksperimentel verificering af isoleringsegenskaber p\u00e5 \u00e5benlyst ikke-kryptografiske funktioner (stresstest med svage primitiv). Repositoryet inkluderer et laboratoriestand, der inds\u00e6tter en almindelig hash-funktion FNV-1a inde i barrieren. Gjennom ikke-line\u00e6r kombinatorisk rangering, opdeling af bytes over gr\u00e6nserne for 7-bit kanaler (GCD(7, 8) = 1) og injektion af st\u00f8jbits i hver byte blokeres praktisk anvendelse eller opbygning af en l\u00f8selig SAT\/SMT-model for klartekst og krypteret tekst allerede p\u00e5 formuleringsstadiet af ligningssystemet.\n
Maskinvalidering i Lean 4. Alle 12 grundl\u00e6ggende matematiske, kombinatoriske og bitvektor-teoremer i konstruktionen (samt den anvendte skema for hybrid n\u00f8gleaftale 3-to-8 fra tre uafh\u00e6ngige KEM-kanaler i APPS.md), beskrevet i dokumentet PROOFS.md, er fuldt bevist i Lean 4 uden brug af aksiomer og manglende beviser.\n
Indbygget v\u00e6rkt\u00f8j til kryptanalytisk testning, der inkluderer automatiserede kontroller: statistiske batterier af tests, vurdering af algebraisk grad og non-linearity, kontrol af frakobling af seeds ved sortering af st\u00f8jpositioner gennem CCA-orakel og identifikation af s\u00e5rbarheder ved hj\u00e6lp af eksterne l\u00f8sningsmidler.\n
To driftsformer: standard autentificeret tilstand (AEAD baseret p\u00e5 MAC-Inside-Encrypt, hvor imitatsionsinds\u00e6ttelsen beregnes og krypteres inde i containeren) og plausibel ben\u00e6gtelsesmode (Plausible Deniability) baseret p\u00e5 ubetinget kodning COBS, hvor dekryptering med en godtyldig forkert n\u00f8gle giver syntaktisk korrekte data uden fejlindikator.\n