{"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\/it\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Isolatore crittografico ITB con prova formale di affidabilit\u00e0","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
\u00c8 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 \u00e8 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.<\/p>\n
La trasformazione dei dati in ITB \u00e8 suddivisa in due livelli interconnessi (Interlocked Barrier), gestiti da otto semi chiave isolati (8-seed isolation) con un'evoluzione locale della chiave attraverso una catena a collegamento diretto (ChainHash). Nel primo livello, la barriera di ranking (Rank Barrier) esegue una permutazione combinatoria chiave di ciascun blocco da 48 bit (o di un blocco da 168 bit per i primitivi da 512 bit), distribuendo i bit del testo in chiaro su tre regioni indipendenti in base alla combinazione a due fasi in base al suo numero (lo spazio delle partizioni bilanciate C(48, 16) * C(32, 16) \u00e8 circa 2^70.20, mentre in modalit\u00e0 a 168 bit C(168, 56) * C(112, 56) \u00e8 circa 2^258.60). Nel secondo livello, la barriera pixel (Pixel Barrier) mappa i dati su una griglia di elementi da 8 byte (8 canali con 7 bit di dati e 1 bit di rumore pseudocasuale in ogni byte) con uno spostamento circolare chiave 7-bit pixel per pixel, mascherando i canali a 7 bit e selezionando la posizione del bit di rumore.<\/p>\n
Caratteristiche principali del progetto:<\/p>\n
\n
Verifica sperimentale delle propriet\u00e0 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 \u00e8 bloccata gi\u00e0 nella fase di formulazione del sistema di equazioni.\n
Verifica formale automatizzata con il linguaggio Lean 4. Tutti i 12 teoremi matematici, combinatori e di vettori di bit di base, nonch\u00e9 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.\n
Strumenti integrati per test di crittoanalisi, compresi controlli automatizzati: batterie di test statistici, valutazione del grado algebrico e della non linearit\u00e0, verifica dell'isolamento delle chiavi durante la filtrazione delle posizioni di rumore tramite l'oracolo CCA e ricerca di vulnerabilit\u00e0 mediante risolutori esterni.\n
Due modalit\u00e0 di funzionamento: modalit\u00e0 standard autenticata (AEAD secondo lo schema MAC-Inside-Encrypt, dove l'inserimento dell'impronta viene calcolato e cifrato all'interno del contenitore) e modalit\u00e0 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.\n