Криптографический изолятор ITB с формальным доказательством надёжности - QubStore

Криптографический изолятор ITB с формальным доказательством надёжности

Проект ITB предлагает необычный подход к криптографии: стандартные хэши и шифры (AES, BLAKE2/3, Areion) оборачиваются в двухуровневый комбинаторно-топологический барьер, который должен отсекать дифференциальный и линейный криптоанализ ещё до того, как атакующий построит рабочую модель.

Код написан на Go, а критические участки ускорены ассемблером под x86_64 и ARM64 (Aarch64); распространяется под Apache 2.0. Внутри — два сцепленных уровня (Interlocked Barrier) и восемь независимых ключевых сидов с локальной эволюцией ключа по схеме ChainHash с прямой связью. Первый уровень — Rank Barrier — переставляет каждый 48-битный блок (в 512-битных примитивах — 168-битный) через двухшаговое обратное ранжирование combinadic unrank, разбрасывая биты открытого текста по трём регионам. Число сбалансированных разбиений C(48, 16) * C(32, 16) ≈ 2^70.20, а в 168-битном режиме C(168, 56) * C(112, 56) ≈ 2^258.60. Второй уровень — Pixel Barrier — раскладывает данные по сетке 8-байтовых ячеек: восемь каналов по 7 бит данных плюс бит псевдослучайного шума в каждом байте, с попиксельным 7-битным циклическим сдвигом, маскированием каналов и выбором позиции шумового бита.

Отдельно стоит лабораторный стенд: внутрь барьера подставляют заведомо слабую FNV-1a, и связка всё равно сопротивляется. Работает за счёт нелинейного combinadic unrank, расщепления байтов по границам 7-битных каналов (НОД(7, 8) = 1) и шумовых битов в каждом байте — построить решаемую SAT/SMT-модель по паре открытый/шифрованный текст не выходит уже на этапе формулировки уравнений.

Надёжность подтверждена формально: 12 базовых математических, комбинаторных и бит-векторных теорем из PROOFS.md, а также схема гибридного согласования ключей 3-to-8 из трёх независимых KEM-каналов (развёрнута в 230 теорем и лемм, см. APPS.md) доказаны в Lean 4 — без аксиом и пропусков. В репозитории есть и инструменты криптоаналитического тестирования: статистические батареи, оценка алгебраической степени и нелинейности, проверка изоляции сидов через CCA-оракул с отсеиванием шумовых позиций, поиск уязвимостей внешними решателями.

Предусмотрены два режима и фиксированный wire format: штатный аутентифицированный AEAD по схеме MAC-Inside-Encrypt (имитовставка считается и шифруется внутри контейнера) и режим правдоподобного отрицания на безусловном кодировании COBS — неверный ключ выдаёт произвольные данные без сигнала ошибки. С быстрыми PRF конструкция годится для защищённых мессенджеров, хранения файлов и VPN-туннелей; при групповой пакетной очереди накладные расходы формата — около 15%. Ядра работают за постоянное время, после вызовов стековые фреймы и регистры (GPR, XMM/YMM/ZMM, NEON) принудительно очищаются. Под x86_64 задействованы BMI2 (PEXT/PDEP), AES-NI, VAES, AVX2 и AVX-512, под Aarch64 — NEON, Crypto Extensions и SVE2 с переносимым откатом на чистый Go. Поверх единого C ABI (libitb3) подготовлены обвязки для 33 языков программирования.

Ссылка на основную публикацию