{"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\/en\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"ITB Cryptographic Isolator with formal proof of reliability","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
The ITB project has been introduced, developing a symmetric cryptographic isolator designed to encapsulate standard pseudorandom functions (PRF) and hash primitives (AES, BLAKE2\/3, Areion, among others) in a linked combinatorial and topological barrier. Unlike classical block and stream cipher modes, the ITB architecture aims for structural isolation of the internal primitive, preventing the propagation of differential and linear characteristics, algebraic linearization, and direct encodings for SAT\/SMT and MILP solvers across the barrier boundaries. The code is written in Go with low-level optimizations in assembly for x86_64 and ARM64 (Aarch64) architectures and is distributed under the Apache 2.0 license.<\/p>\n
Data transformation in ITB is divided into two interlocked levels (Interlocked Barrier), managed by eight isolated key seeds (8-seed isolation) with local key evolution through a direct link cascade (ChainHash). At the first level, the rank barrier (Rank Barrier) performs a key combinatorial permutation of each 48-bit block (or 168-bit block for 512-bit primitives), distributing bits of the plaintext into three independent regions based on a two-step combination finding by its number (the space of balanced partitions C(48, 16) * C(32, 16) is about 2^70.20, and in the 168-bit mode C(168, 56) * C(112, 56) \u2014 about 2^258.60). At the second level, the pixel barrier (Pixel Barrier) maps the data onto a grid of 8-byte elements (8 channels of 7 bits of data and 1 bit of pseudo-random noise in each byte) with a per-pixel key 7-bit cyclic shift, masking 7-bit channels, and selecting the position of the noise bit.<\/p>\n
Key features of the project:<\/p>\n
\n
Experimental validation of isolating properties on deliberately non-cryptographic functions (stress test with weak primitives). The repository includes a laboratory setup that substitutes a regular hash function FNV-1a inside the barrier. Through nonlinear combinatorial ranking, byte splitting across 7-bit channel boundaries (GCD(7, 8) = 1), and injecting noise bits into each byte, practical addressing or constructing a solvable SAT\/SMT model based on the plaintext and encrypted text is blocked already at the stage of formulating the system of equations.\n
Machine-verified formal verification in Lean 4. All 12 fundamental mathematical, combinatorial, and bit-vector theorems of the construction (as well as the applied scheme for hybrid key agreement 3-to-8 from three independent KEM channels in APPS.md), are fully proven in Lean 4 without using axioms or skipping proofs.\n
Built-in tools for cryptographic testing, including automated checks: statistical test batteries, assessment of algebraic degree and non-linearity, isolation check of seeds while filtering noise positions through a CCA oracle, and vulnerability search using external solvers.\n
Two operating modes: standard authenticated mode (AEAD using the MAC-Inside-Encrypt scheme, where the MAC is computed and encrypted within the container) and plausible deniability mode based on unconditional coding COBS, where decrypting with any incorrect key outputs syntactically correct data without an error indicator.\n