ITB Cryptographic Isolator with formal proof of reliability

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.

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 cascade with direct feedback (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 the bits of the plaintext across 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, while in the 168-bit mode C(168, 56) * C(112, 56) is 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 pseudorandom noise in each byte) with a per-pixel key 7-bit cyclic shift, 7-bit channel masking, and noise bit position selection.

Key features of the project:

• 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.
• 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.
• 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.
• 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.
• In combination with fast modern PRFs (AES, BLAKE2/3, Areion), the construction is suitable for secure messaging, file storage, and networking VPN-tunnels (with a group packet queuing overhead of about 15%). To protect against side-channel attacks, the core executes in constant time with full forced cleanup of stack frames and processor registers (GPR, XMM/YMM/ZMM, NEON) after calls.
• For the x86_64 architecture, assembler cores are implemented using BMI2 instructions (PEXT/PDEP), AES-NI, VAES, AVX2, and AVX-512, while for ARM64 (Aarch64) — based on NEON extensions, Crypto Extensions, and SVE2 (with a portable fallback to pure Go). Wrappers for 33 programming languages are prepared over a unified C ABI (libitb3).

Source: opennet.ru