🥇Kryptografický izolátor ITB s formálním důkazem spolehlivosti

Projekt ITB představuje symetrický kryptografický izolátor, navržený k obalení standardních pseudonáhodných funkcí (PRF) a hashových primitiv (AES, BLAKE2/3, Areion a dalších) v propojené kombinatorní a topologické bariéře. Na rozdíl od klasických blokových a proudových šifrovacích módů, architektura ITB se zaměřuje na strukturální izolaci vnitřního primitiva, čímž brání šíření diferenčních a lineárních charakteristik, algebraické linearizace a přímých kódování pro SAT/SMT a MILP řešitele přes hranice bariéry. Kód je napsán v jazyce Go s nízkoúrovňovými optimalizacemi v assembleru pro architektury x86_64 a ARM64 (Aarch64) a je šířen pod licencí Apache 2.0.

Transformace dat v ITB je rozdělena na dvě propojené úrovně (Interlocked Barrier), řízené osmi izolovanými klíčovými seedmi (8-seed isolation) s lokální evolucí klíče prostřednictvím řetězce s přímou vazbou (ChainHash). Na první úrovni bariéra hodnocení (Rank Barrier) provádí klíčovou kombinatorní permutaci každého 48bitového bloku (nebo 168bitového bloku pro 512bitové primitivy), distribuuje bity otevřeného textu do tří nezávislých regionů na základě dvoustupňového nalezení kombinace podle jeho čísla (prostor vyváženého rozdělení C(48, 16) * C(32, 16) činí přibližně 2^70.20, a v 168bitovém režimu C(168, 56) * C(112, 56) – přibližně 2^258.60). Na druhé úrovni pixelová bariéra (Pixel Barrier) mapuje data na mřížku 8-bajtových prvků (8 kanálů po 7 bitech dat a 1 bitu pseudonáhodného šumu v každém bajtu) s pixelovým klíčem 7bitového cyklického posunu, maskováním 7bitových kanálů a výběrem pozice šumového bitu.

Hlavní vlastnosti projektu:

Experimentální ověření izolujících vlastností na zjevně nekryptografických funkcích (stresový test se slabými primitivy). Součástí repozitáře je laboratorní stan, který vkládá obyčejnou hash funkci FNV-1a do bariéry. Díky nelineární kombinatorické rozřazovací technice, dělení bytů na hranicích 7bitových kanálů (GCD(7, 8) = 1) a injekci šumových bitů do každého bajtu je praktické použití nebo konstrukce řešitelného SAT/SMT modelu podle otevřeného a šifrovaného textu blokováno již ve fázi formulace systému rovnic.
Strojově ověřená formální verifikace v jazyce Lean 4. Všechny 12 základních matematických, kombinatorních a bitově vektorových vět konstrukce (spolu s aplikovanou schématem hybridní shody klíčů 3-to-8 ze tří nezávislých KEM kanálů v APPS.md), popsané v dokumentu PROOFS.md, jsou zcela prokázány v Lean 4 bez použití axiomů a vynechaných důkazů.
Vestavěný nástroj pro kryptoanalyzující testování, zahrnující automatizované kontroly: statistické baterie testů, hodnocení algebraického stupně a nelinearity, kontrola izolačních klíčů při filtraci šumu pomocí CCA-orákula a hledání zranitelností pomocí externích solverů.
Dva režimy provozu: standardní autentizovaný režim (AEAD podle schématu MAC-Inside-Encrypt, kde je autentizační kód počítán a šifrován uvnitř kontejneru) a režim plauzibilního popření (Plausible Deniability) na základě bezpodmínečného kódování COBS, přičemž dešifrování libovolným nesprávným klíčem produkuje syntakticky správná data bez indikátoru chyby.
Ve spojení s rychlými moderními PRF (AES, BLAKE2/3, Areion) je konstrukce vhodná pro bezpečnou výměnu zpráv, ukládání souborů a síťové VPN-tunele (při skupinové paketové frontě tvoří režie formátu přibližně 15%). Pro ochranu před útoky přes vedlejší kanály jádra běží v konstantní době (constant-time) s plnou vynucenou čistotou zásobníkových rámců a procesorových registrů (GPR, XMM/YMM/ZMM, NEON) po voláních.
Pro architekturu x86_64 byly realizovány assemblerové jádra s využitím instrukcí BMI2 (PEXT/PDEP), AES-NI, VAES, AVX2 a AVX-512, a pro ARM64 (Aarch64) – na základě rozšíření NEON, Crypto Extensions a SVE2 (s přenositelným vracením na čistý Go). Nad jednotným C ABI (libitb3) byly připraveny vazby pro 33 programovacích jazyků.

Zdroj: opennet.ru