{"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\/no\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Kryptografisk isolator ITB med formell bevis p\u00e5 p\u00e5litelighet","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
ITB-prosjektet har utviklet en symmetrisk kryptografisk isolator, designet for \u00e5 innkapsle standard pseudotilfeldige funksjoner (PRF) og hash-primitiver (AES, BLAKE2\/3, Areion og andre) i en sammenkoblet kombinatorisk og topologisk barriere. I motsetning til klassiske blokk- og str\u00f8m-krypteringsmodi, har ITB-arkitekturen som m\u00e5l \u00e5 strukturelt isolere den interne primitiv, og forhindre spredning av differensielle og line\u00e6re karakteristikker, algebraisk linearisering, og direkte koding for SAT\/SMT- og MILP-l\u00f8sere gjennom barrierens grenser. Koden er skrevet i Go med lavniv\u00e5optimaliseringer p\u00e5 assembler for x86_64 og ARM64 (Aarch64) arkitekturer, og distribueres under Apache 2.0-lisensen.<\/p>\n
Datakonvertering i ITB er delt inn i to sammenkoblede niv\u00e5er (Interlocked Barrier), styrt av \u00e5tte isolerte n\u00f8kkelsider (8-seed isolation) med lokal n\u00f8kkelutvikling gjennom en kaskade med direkte tilkobling (ChainHash). P\u00e5 f\u00f8rste niv\u00e5 utf\u00f8rer rangeringsbarrieren (Rank Barrier) en n\u00f8kkelkombinasjonspermutasjon av hver 48-bit blokk (eller 168-bit blokk for 512-bit primitive), og distribuerer bitene av klartekst over tre uavhengige regioner basert p\u00e5 en to-trinns kombinasjonsfunksjon basert p\u00e5 nummeret dens (rommet for balanserte oppdelinger C(48, 16) * C(32, 16) er omtrent 2^70.20, og i 168-bit-modus C(168, 56) * C(112, 56) er - omtrent 2^258.60). P\u00e5 andre niv\u00e5 viser pikselbarrieren (Pixel Barrier) dataene p\u00e5 et grid av 8-byte elementer (8 kanaler med 7 bit data og 1 bit pseudorandom st\u00f8y i hver byte) med en per-piksel n\u00f8kkel 7-bit sirkul\u00e6r forskyvning, masking av 7-bit kanaler og valg av st\u00f8ybitposisjon.<\/p>\n
Hovedtrekkene ved prosjektet:<\/p>\n
\n
Eksperimentell verifisering av isolasjonsegenskaper p\u00e5 forh\u00e5ndsdefinerte ikke-kryptografiske funksjoner (stresstest med svake primitiver). Repositoriet inkluderer en laboratoriebank som setter en vanlig hash-funksjon FNV-1a inn i barrieren. Gjennom ikke-line\u00e6r kombinatorisk rangering, byte-splitting p\u00e5 grensene for 7-bits kanaler (GCD(7, 8) = 1) og injisjon av st\u00f8ybiter i hver byte blokkerer praktisk bruk eller konstruksjon av en l\u00f8selig SAT\/SMT-modell basert p\u00e5 klar- og kryptert tekst allerede p\u00e5 formuleringsstadiet av systemet med likninger.\n
Maskinvalidering av formell verifikasjon i Lean 4. Alle de 12 grunnleggende matematiske, kombinatoriske og bitvektor-teoremer av konstruksjonen (samt den praktiske ordningen med hybrid n\u00f8kkeleniggj\u00f8ring 3-to-8 fra tre uavhengige KEM-kanaler i APPS.md), beskrevet i dokumentet PROOFS.md, er fullstendig bevist i Lean 4 uten bruk av aksiomer og mangler i bevisene.\n
Innebygd verkt\u00f8y for kryptanalytisk testing, inkludert automatiserte sjekker: statistiske testbatterier, vurdering av algebraisk grad og ikke-linearitet, sjekk av isolasjon av fr\u00f8 ved sortering av st\u00f8yposisjoner gjennom CCA-orakel og s\u00e5rbarhetss\u00f8king ved hjelp av eksterne l\u00f8sningsmidler.\n
To driftsmoduser: standard autentisert modus (AEAD basert p\u00e5 MAC-Inside-Encrypt, hvor integriteten beregnes og krypteres inne i containeren) og modus for plausibel benektelse (Plausible Deniability) basert p\u00e5 ubetinget koding COBS, der dekryptering med en vilk\u00e5rlig feil n\u00f8kkel gir syntaktisk korrekte data uten feilmelding.\n