{"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\/sv\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"ITB-kryptografisk isolator med formellt bevis p\u00e5 tillf\u00f6rlitlighet","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Projektet ITB presenterar en symmetrisk kryptografisk isolator som \u00e4r avsedd f\u00f6r inpackning av standardpseudo-slumptalsfunktioner (PRF) och hash-primitiv (AES, BLAKE2\/3, Areion och andra) i en sammansatt kombinatorisk och topologisk barri\u00e4r. Till skillnad fr\u00e5n klassiska block- och str\u00f6mcipher, syftar ITBs arkitektur till strukturell isolering av den interna primitiva, vilket f\u00f6rhindrar spridning av differentierings- och linj\u00e4ra egenskaper, algebraisk linj\u00e4risering, samt direkta kodningar f\u00f6r SAT\/SMT- och MILP-l\u00f6sare genom barri\u00e4rens gr\u00e4nser. Koden \u00e4r skriven i Go med l\u00e5gniv\u00e5optimeringar i assembler f\u00f6r x86_64 och ARM64 (Aarch64) och distribueras under Apache 2.0-licensen.<\/p>\n
Datakonvertering i ITB \u00e4r indelad i tv\u00e5 sammankopplade niv\u00e5er (Interlocked Barrier) som styrs av \u00e5tta isolerade nyckelfr\u00f6n (8-seed isolation) med lokal nyckelutveckling genom en kedja med direkt koppling (ChainHash). P\u00e5 den f\u00f6rsta niv\u00e5n utf\u00f6r rangordningsbarri\u00e4ren (Rank Barrier) en nyckelkombinatorisk permutering av varje 48-bitars block (eller 168-bitars block f\u00f6r 512-bitars primitiva), vilket f\u00f6rdelar bitarna av klartext \u00f6ver tre oberoende omr\u00e5den baserat p\u00e5 en tv\u00e5stegs kombinatorik f\u00f6r dess nummer (det balanserade partitioneringsrummet C(48, 16) * C(32, 16) \u00e4r ungef\u00e4r 2^70.20, och i 168-bitars l\u00e4get C(168, 56) * C(112, 56) \u2014 ungef\u00e4r 2^258.60). P\u00e5 den andra niv\u00e5n avbildar pixelbarri\u00e4ren (Pixel Barrier) data till ett rutn\u00e4t av 8-byte element (8 kanaler med 7 bitar data och 1 bit pseudorandom brus i varje byte) med pixelvis nyckelbaserad 7-bitars cyklisk skiftning, maskering av 7-bitars kanaler och val av brusbitsposition.<\/p>\n
Huvudfunktioner i projektet:<\/p>\n
\n
Experimentell kontroll av isoleringsegenskaper p\u00e5 avsiktligt icke-kryptografiska funktioner (stress-test med svaga primitiv). I repositoryn ing\u00e5r en laboratoriestation som inf\u00f6rlivar en vanlig hash-funktion, FNV-1a, inuti barri\u00e4ren. Genom icke-linj\u00e4ra kombinatoriska rangordningar, uppdelning av bytes vid gr\u00e4nsen av 7-bits kanaler (GCD(7, 8) = 1) och injektion av brus-bitar i varje byte blockeras praktisk anv\u00e4ndning eller konstruktion av l\u00f6sbara SAT\/SMT-modeller f\u00f6r klar- och krypterad text redan i formuleringsteget av ekvationssystemet.\n
Maskinvaliderad formell verifiering p\u00e5 Lean 4-spr\u00e5ket. Alla 12 grundl\u00e4ggande matematiska, kombinatoriska och bitvektorteoremen i konstruktionen (liksom den till\u00e4mpade schemat f\u00f6r hybridnyckel\u00f6verenskommelse 3-to-8 fr\u00e5n tre oberoende KEM-kanaler i APPS.md), beskrivna i dokumentet PROOFS.md, \u00e4r fullst\u00e4ndigt bevisade i Lean 4 utan anv\u00e4ndning av axiom och \u00f6verskridanden av bevis.\n
Inbyggda verktyg f\u00f6r kryptanalytisk testning, inklusive automatiserade verifieringar: statistiska testbatterier, bed\u00f6mning av algebraisk grad och icke-linj\u00e4ritet, kontroll av isolering av fr\u00f6n vid filtrering av bruspositioner genom CCA-orakel och s\u00e5rbarhetss\u00f6kning med externa l\u00f6sare.\n
Tv\u00e5 driftsl\u00e4gen: standard autentiserat l\u00e4ge (AEAD enligt MAC-Inside-Encrypt schemat, d\u00e4r autentisering ber\u00e4knas och krypteras inuti containern) och l\u00e4ge f\u00f6r plausibel f\u00f6rnekan (Plausible Deniability) baserat p\u00e5 villkorsl\u00f6s kodning COBS, d\u00e4r dekryptering med en godtycklig felaktig nyckel ger syntaktiskt korrekta data utan felindikator.\n