{"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\/fr\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Isolateur cryptographique ITB avec une preuve formelle de fiabilit\u00e9","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Le projet ITB a \u00e9t\u00e9 pr\u00e9sent\u00e9, d\u00e9veloppant un isolateur cryptographique sym\u00e9trique, con\u00e7u pour envelopper des fonctions pseudorandom standard (PRF) et des primitives de hachage (AES, BLAKE2\/3, Areion et autres) dans une barri\u00e8re combinatoire et topologique. Contrairement aux modes de chiffrement classiques par blocs et par flux, l'architecture ITB vise une isolation structurelle de la primitive interne, emp\u00eachant la propagation des caract\u00e9ristiques diff\u00e9rentielles et lin\u00e9aires, la lin\u00e9arisation alg\u00e9brique, ainsi que les codages directs pour les solveurs SAT\/SMT et MILP \u00e0 travers les fronti\u00e8res de la barri\u00e8re. Le code est \u00e9crit en Go avec des optimisations de bas niveau en assembleur pour les architectures x86_64 et ARM64 (Aarch64) et est distribu\u00e9 sous la licence Apache 2.0.<\/p>\n
La transformation des donn\u00e9es dans ITB est divis\u00e9e en deux niveaux li\u00e9s (Interlocked Barrier), g\u00e9r\u00e9s par huit cl\u00e9s isol\u00e9es (8-seed isolation) avec une \u00e9volution locale de la cl\u00e9 \u00e0 travers une cha\u00eene en liaison directe (ChainHash). Au premier niveau, la barri\u00e8re de classement (Rank Barrier) ex\u00e9cute une permutation combinatoire cl\u00e9 de chaque bloc de 48 bits (ou bloc de 168 bits pour des primitives de 512 bits), distribuant les bits du texte clair sur trois r\u00e9gions ind\u00e9pendantes en fonction d'une combinaison \u00e0 deux \u00e9tapes selon son num\u00e9ro (l'espace des partitions \u00e9quilibr\u00e9es C(48, 16) * C(32, 16) est d'environ 2^70.20, et en mode 168 bits C(168, 56) * C(112, 56) \u2014 environ 2^258.60). Au deuxi\u00e8me niveau, la barri\u00e8re de pixel (Pixel Barrier) mappe les donn\u00e9es sur une grille d'\u00e9l\u00e9ments de 8 octets (8 canaux avec 7 bits de donn\u00e9es et 1 bit de bruit pseudo-al\u00e9atoire dans chaque octet) avec un d\u00e9calage cyclique de cl\u00e9 de 7 bits par pixel, masquant les canaux de 7 bits et choisissant la position du bit de bruit.<\/p>\n
Les principales caract\u00e9ristiques du projet :<\/p>\n
\n
La v\u00e9rification exp\u00e9rimentale des propri\u00e9t\u00e9s d'isolement sur des fonctions manifestement non cryptographiques (test de stress avec des primitives faibles). Le d\u00e9p\u00f4t comprend un banc d'essai de laboratoire int\u00e9grant une fonction de hachage classique FNV-1a \u00e0 l'int\u00e9rieur de la barri\u00e8re. Gr\u00e2ce \u00e0 une combinaison non lin\u00e9aire de classement, \u00e0 la division des octets aux fronti\u00e8res des canaux de 7 bits (GCD(7, 8) = 1) et \u00e0 l'injection de bits de bruit dans chaque octet, l'utilisation pratique ou la construction d'un mod\u00e8le SAT\/SMT solvable \u00e0 partir du texte clair et chiffr\u00e9 est bloqu\u00e9e d\u00e8s la formulation du syst\u00e8me d'\u00e9quations.\n
V\u00e9rification formelle automatique v\u00e9rifi\u00e9e par machine en Lean 4. Toutes les 12 th\u00e9or\u00e8mes math\u00e9matiques de base, combinatoires et th\u00e9or\u00e8mes des vecteurs de bits de la construction (ainsi que le sch\u00e9ma appliqu\u00e9 d'accord hybride des cl\u00e9s 3-to-8 \u00e0 partir de trois canaux KEM ind\u00e9pendants dans APP.md), d\u00e9crites dans le document PROOFS.md, sont enti\u00e8rement prouv\u00e9es dans Lean 4 sans utiliser d'axiomes ni de lacunes dans les preuves.\n
Outils int\u00e9gr\u00e9s pour les tests cryptanalytiques, comprenant des v\u00e9rifications automatis\u00e9es : batteries de tests statistiques, \u00e9valuation du degr\u00e9 alg\u00e9brique et de la non-lin\u00e9arit\u00e9, v\u00e9rification de l'isolation des graines lors du filtrage des positions de bruit via un oracle CCA et recherche de vuln\u00e9rabilit\u00e9s \u00e0 l'aide de solveurs externes.\n
Deux modes de fonctionnement : mode authentifi\u00e9 standard (AEAD selon le sch\u00e9ma MAC-Inside-Encrypt, o\u00f9 l'insertion d'authentification est calcul\u00e9e et chiffr\u00e9e \u00e0 l'int\u00e9rieur du conteneur) et mode de d\u00e9ni plausible bas\u00e9 sur le codage inconditionnel COBS, dans lequel le d\u00e9chiffrement avec une cl\u00e9 incorrecte retourne des donn\u00e9es syntaxiquement correctes sans indicateur d'erreur.\n