Isolatore crittografico ITB con prova formale di affidabilità

È stato presentato il progetto ITB, che sviluppa un isolatore crittografico simmetrico progettato per avvolgere funzioni pseudo-casuali standard (PRF) e primitive hash (AES, BLAKE2/3, Areion e altre) in una barriera combinatoria e topologica intrecciata. A differenza dei classici modi di crittografia a blocchi e a flusso, l'architettura ITB mira a un'isolamento strutturale della primitiva interna, ostacolando la diffusione delle caratteristiche differenziali e lineari, la linearizzazione algebrica e le codifiche dirette per i risolutori SAT/SMT e MILP attraverso i confini della barriera. Il codice è scritto in Go con ottimizzazioni a basso livello in assembly per le architetture x86_64 e ARM64 (Aarch64) e viene distribuito sotto licenza Apache 2.0.

La trasformazione dei dati in ITB è divisa in due livelli interconnessi (Interlocked Barrier), gestiti da otto semi chiave isolati (8-seed isolation) con evoluzione locale della chiave attraverso una cascata a connessione diretta (ChainHash). Al primo livello, la barriera di ranking (Rank Barrier) esegue una permutazione combinatoria della chiave di ciascun blocco a 48 bit (o blocco a 168 bit per le primitive a 512 bit), distribuendo i bit del testo in chiaro su tre regioni indipendenti in base a una ricerca combinatoria a due fasi in base al suo numero (lo spazio delle partizioni bilanciate C(48, 16) * C(32, 16) è di circa 2^70.20, mentre nel modo a 168 bit C(168, 56) * C(112, 56) è di circa 2^258.60). Al secondo livello, la barriera dei pixel (Pixel Barrier) mappa i dati su una griglia di elementi a 8 byte (8 canali con 7 bit di dati e 1 bit di rumore pseudo-casuale in ciascun byte) con uno spostamento ciclico di chiave a 7 bit pixel per pixel, mascheramento dei canali a 7 bit e scelta della posizione del bit di rumore.

Caratteristiche principali del progetto:

• Verifica sperimentale delle proprietà isolanti su funzioni notoriamente non crittografiche (stress test con primitive deboli). Il repository include una piastra di laboratorio che inserisce all'interno della barriera una comune funzione hash FNV-1a. Grazie alla combinazione non lineare della classificazione, alla scissione dei byte lungo i confini dei canali a 7 bit (GCD(7, 8) = 1) e all'iniezione di bit di rumore in ciascun byte, l'accesso pratico o la costruzione di un modello SAT/SMT risolvibile su testo in chiaro e cifrato è bloccata già nella fase di formulazione del sistema di equazioni.
• Verifica formale automatizzata con il linguaggio Lean 4. Tutti i 12 teoremi matematici, combinatori e di vettori di bit di base, nonché lo schema applicativo di accordo ibrido delle chiavi 3-to-8 da tre canali KEM indipendenti in APPS.md, sono stati completamente dimostrati in Lean 4 senza l'uso di assiomi e omissioni nelle dimostrazioni.
• Strumenti integrati per test di crittoanalisi, compresi controlli automatizzati: batterie di test statistici, valutazione del grado algebrico e della non linearità, verifica dell'isolamento delle chiavi durante la filtrazione delle posizioni di rumore tramite l'oracolo CCA e ricerca di vulnerabilità mediante risolutori esterni.
• Due modalità di funzionamento: modalità standard autenticata (AEAD secondo lo schema MAC-Inside-Encrypt, dove l'inserimento dell'impronta viene calcolato e cifrato all'interno del contenitore) e modalità di negazione plausibile (Plausible Deniability) basata sulla codifica incondizionata COBS, in cui la decrittazione con una chiave errata restituisce dati sintatticamente corretti senza indicatori di errore.
• In combinazione con PRF moderne e veloci (AES, BLAKE2/3, Areion), la costruzione è adatta per scambio di messaggi sicuri, archiviazione di file e tunnel di rete (con un sovraccarico del formato che ammonta a circa il 15% per la coda di pacchetti di gruppo). Per proteggere dagli attacchi attraverso canali laterali, il nucleo viene eseguito in tempo costante (constant-time) con completa pulizia forzata dei frame dello stack e dei registri del processore (GPR, XMM/YMM/ZMM, NEON) dopo le chiamate. VPNPer l'architettura x86_64 sono stati realizzati nucleri assembler utilizzando le istruzioni BMI2 (PEXT/PDEP), AES-NI, VAES, AVX2 e AVX-512, mentre per ARM64 (Aarch64) è stata utilizzata la base delle estensioni NEON, delle Crypto Extensions e di SVE2 (con ripristino portabile su Go puro). Sono stati preparati wrapper per 33 lingue di programmazione sopra un'unica C ABI (libitb3).
• È stato presentato il progetto ITB, che sviluppa un isolante crittografico simmetrico, concepito per avvolgere funzioni pseudocasuali standard (PRF) e primitive hash (AES, BLAKE2/3, Areion e altre) in modo concatenato.

Fonte: opennet.ru