ITB-kryptografisk isolator med formellt bevis på tillförlitlighet

Projektet ITB presenterar en symmetrisk kryptografisk isolator som är avsedd för inpackning av standardpseudo-slumptalsfunktioner (PRF) och hash-primitiv (AES, BLAKE2/3, Areion och andra) i en sammansatt kombinatorisk och topologisk barriär. Till skillnad från klassiska block- och strömcipher, syftar ITBs arkitektur till strukturell isolering av den interna primitiva, vilket förhindrar spridning av differentierings- och linjära egenskaper, algebraisk linjärisering, samt direkta kodningar för SAT/SMT- och MILP-lösare genom barriärens gränser. Koden är skriven i Go med lågnivåoptimeringar i assembler för x86_64 och ARM64 (Aarch64) och distribueras under Apache 2.0-licensen.

Datakonvertering i ITB är uppdelad i två sammanlänkade nivåer (Interlocked Barrier), hanterade av åtta isolerade nyckel-seeds (8-seed isolation) med lokal nyckelevolution genom en kedja med direkt koppling (ChainHash). På den första nivån utför rankingbarriären (Rank Barrier) nyckelkombinatoriska permutationer av varje 48-bits block (eller 168-bits block för 512-bits primitiv), vilket distribuerar klartextens bitar över tre oberoende regioner baserat på den tvåstegs kombinationens nummer (rymd av balanserade partitioner C(48, 16) * C(32, 16) är cirka 2^70.20, och i 168-bits läge C(168, 56) * C(112, 56) är cirka 2^258.60). På den andra nivån kartlägger pixelbarriären (Pixel Barrier) data till ett rutnät av 8-byte element (8 kanaler med 7 bitar data och 1 bit pseudorandomt brus i varje byte) med per-pixel nyckel 7-bits cyklisk förskjutning, maskering av 7-bits kanaler och urval av brusbitens position.

Huvudfunktioner i projektet:

• Experimentell kontroll av isoleringsegenskaper på avsiktligt icke-kryptografiska funktioner (stress-test med svaga primitiv). I repositoryn ingår en laboratoriestation som införlivar en vanlig hash-funktion, FNV-1a, inuti barriären. Genom icke-linjära kombinatoriska rangordningar, uppdelning av bytes vid gränsen av 7-bits kanaler (GCD(7, 8) = 1) och injektion av brus-bitar i varje byte blockeras praktisk användning eller konstruktion av lösbara SAT/SMT-modeller för klar- och krypterad text redan i formuleringsteget av ekvationssystemet.
• Maskinvaliderad formell verifiering på Lean 4-språket. Alla 12 grundläggande matematiska, kombinatoriska och bitvektorteoremen i konstruktionen (liksom den tillämpade schemat för hybridnyckelöverenskommelse 3-to-8 från tre oberoende KEM-kanaler i APPS.md), beskrivna i dokumentet PROOFS.md, är fullständigt bevisade i Lean 4 utan användning av axiom och överskridanden av bevis.
• Inbyggda verktyg för kryptanalytisk testning, inklusive automatiserade verifieringar: statistiska testbatterier, bedömning av algebraisk grad och icke-linjäritet, kontroll av isolering av frön vid filtrering av bruspositioner genom CCA-orakel och sårbarhetssökning med externa lösare.
• Två driftslägen: standard autentiserat läge (AEAD enligt MAC-Inside-Encrypt schemat, där autentisering beräknas och krypteras inuti containern) och läge för plausibel förnekan (Plausible Deniability) baserat på villkorslös kodning COBS, där dekryptering med en godtycklig felaktig nyckel ger syntaktiskt korrekta data utan felindikator.
• I kombination med snabba moderna PRF (AES, BLAKE2/3, Areion) är konstruktionen lämplig för säker meddelandeutbyte, fillagring och nätverks VPN- tunnlar (med gruppert paketkö så uppgår overheaden för formatet till cirka 15%). För att skydda mot attacker genom sidokanaler utförs kärnan på konstant tid (constant-time) med fullständig tvingande rensning av stackramar och processorregister (GPR, XMM/YMM/ZMM, NEON) efter anrop.
• För x86_64-arkitekturen har assemblerkärnor implementerats med instruktioner BMI2 (PEXT/PDEP), AES-NI, VAES, AVX2 och AVX-512, och för ARM64 (Aarch64) baserat på NEON, Crypto Extensions och SVE2 (med portabel backtracking till ren Go). Ovanför enhetlig C ABI (libitb3) har omslag för 33 programmeringsspråk förberetts.

Källa: opennet.ru