Kryptografisk isolator ITB med formell bevis på pålitelighet

ITB-prosjektet har utviklet en symmetrisk kryptografisk isolator, designet for å 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øm-krypteringsmodi, har ITB-arkitekturen som mål å strukturelt isolere den interne primitiv, og forhindre spredning av differensielle og lineære karakteristikker, algebraisk linearisering, og direkte koding for SAT/SMT- og MILP-løsere gjennom barrierens grenser. Koden er skrevet i Go med lavnivåoptimaliseringer på assembler for x86_64 og ARM64 (Aarch64) arkitekturer, og distribueres under Apache 2.0-lisensen.

Datakonvertering i ITB er delt opp i to sammenkoblede nivåer (Interlocked Barrier), styrt av åtte isolerte nøkkelfrø (8-seed isolation) med lokal utvikling av nøkkelen gjennom en kjede med direkte tilkobling (ChainHash). På det første nivået utfører rangbarrieren (Rank Barrier) en nøkkel kombinatorisk omstokking av hver 48-bits blokk (eller 168-bits blokk for 512-bits primativer), og fordeler bits av klartekst over tre uavhengige regioner basert på en to-trinns kombinasjonsfunn metode (rommet for balanserte partisjoner C(48, 16) * C(32, 16) er omtrent 2^70.20, og i 168-bits modus er C(168, 56) * C(112, 56) omtrent 2^258.60). På det andre nivået avbilder pikselbarrieren (Pixel Barrier) dataene til et nett av 8-bytes elementer (8 kanaler med 7 bits data og 1 bit pseudotilfeldig støy i hver byte) med piksel-nøkkels 7-bits sirkulær forskyvning, maskering av 7-bits kanaler og valg av posisjon for støybit.

Hovedtrekkene ved prosjektet:

• Eksperimentell verifisering av isolasjonsegenskaper på forhåndsdefinerte 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ær kombinatorisk rangering, byte-splitting på grensene for 7-bits kanaler (GCD(7, 8) = 1) og injisjon av støybiter i hver byte blokkerer praktisk bruk eller konstruksjon av en løselig SAT/SMT-modell basert på klar- og kryptert tekst allerede på formuleringsstadiet av systemet med likninger.
• 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økkeleniggjøring 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.
• Innebygd verktøy for kryptanalytisk testing, inkludert automatiserte sjekker: statistiske testbatterier, vurdering av algebraisk grad og ikke-linearitet, sjekk av isolasjon av frø ved sortering av støyposisjoner gjennom CCA-orakel og sårbarhetssøking ved hjelp av eksterne løsningsmidler.
• To driftsmoduser: standard autentisert modus (AEAD basert på MAC-Inside-Encrypt, hvor integriteten beregnes og krypteres inne i containeren) og modus for plausibel benektelse (Plausible Deniability) basert på ubetinget koding COBS, der dekryptering med en vilkårlig feil nøkkel gir syntaktisk korrekte data uten feilmelding.
• I kombinasjon med raske, moderne PRF (AES, BLAKE2/3, Areion) er konstruksjonen egnet for sikker meldingsutveksling, filoppbevaring og nettverks VPN-tunneler (ved gruppepakke-kø, utgjør formatkostnadene omtrent 15%). For å beskytte mot angrep via eksterne kanaler, kjøres kjernen i konstant tid (constant-time) med full tvungen rengjøring av stakkrammer og prosessorregistre (GPR, XMM/YMM/ZMM, NEON) etter kall.
• For x86_64-arkitekturen er det implementert assembler-kjerner som bruker BMI2-instruksjoner (PEXT/PDEP), AES-NI, VAES, AVX2 og AVX-512, mens for ARM64 (Aarch64) er det basert på NEON-utvidelser, Crypto Extensions og SVE2 (med portabel tilbakerulling til ren Go). Det er forberedt innpakninger for 33 programmeringsspråk på en enhetlig C ABI (libitb3).

Kilde: opennet.ru