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

Представлен проект ITB, развивающий симметричный криптографический изолятор, предназначенный для обёртывания стандартных псевдослучайных функций (PRF) и хэш-примитивов (AES, BLAKE2/3, Areion и других) в сцепленный комбинаторный и топологический барьер. В отличие от классических блочных и потоковых режимов шифрования, архитектура ITB нацелена на структурную изоляцию внутреннего примитива, препятствуя распространению дифференциальных и линейных характеристик, алгебраической линеаризации, а также прямых кодировок для решателей SAT/SMT и MILP через границы барьера. Код написан на языке Go с низкоуровневыми оптимизациями на ассемблере для архитектур x86_64 и ARM64 (Aarch64) и распространяется под лицензией Apache 2.0.

Преобразование данных в ITB разделено на два сцепленных уровня (Interlocked Barrier), управляемых восемью изолированными ключевыми сидами (8-seed isolation) с локальной эволюцией ключа через каскад с прямой связью (ChainHash). На первом уровне барьер ранжирования (Rank Barrier) выполняет ключевую комбинаторную перестановку каждого 48-битного блока (или 168-битного блока для 512-битных примитивов), распределяя биты открытого текста по трём независимым регионам на основе двушагового нахождения сочетания по его номеру (пространство сбалансированных разбиений C(48, 16) * C(32, 16) составляет около 2^70.20, а в 168-битном режиме C(168, 56) * C(112, 56) — около 2^258.60). На втором уровне пиксельный барьер (Pixel Barrier) отображает данные на сетку 8-байтовых элементов (8 каналов по 7 бит данных и 1 бит псевдослучайного шума в каждом байте) с попиксельным ключевым 7-битным циклическим сдвигом, маскированием 7-битных каналов и выбором позиции шумового бита.

Основные особенности проекта:

• Экспериментальная проверка изолирующих свойств на заведомо некриптографических функциях (стресс-тест со слабыми примитивами). В состав репозитория включён лабораторный стенд, подставляющий внутрь барьера обычную хэш-функцию FNV-1a. За счёт нелинейного комбинадического разранжирования, расщепления байтов по границам 7-битных каналов (НОД(7, 8) = 1) и инъекции шумовых битов в каждый байт практическое обращение или построение решаемой SAT/SMT-модели по открытому и шифрованному тексту блокируется уже на этапе формулирования системы уравнений.
• Машинно-проверенная формальная верификация на языке Lean 4. Все 12 базовых математических, комбинаторных и бит-векторных теорем конструкции (а также прикладная схема гибридного согласования ключей 3-to-8 из трёх независимых KEM-каналов в APPS.md), описанные в документе PROOFS.md, полностью доказаны в Lean 4 без использования аксиом и пропусков доказательств.
• Встроенный инструментарий криптоаналитического тестирования, включающий автоматизированные проверки: статистические батареи тестов, оценку алгебраической степени и нелинейности, проверку изоляции сидов при отсеивании позиций шума через CCA-оракул и поиск уязвимостей при помощи внешних решателей.
• Два режима работы: стандартный аутентифицированный режим (AEAD по схеме MAC-Inside-Encrypt, где имитовставка вычисляется и шифруется внутри контейнера) и режим правдоподобного отрицания (Plausible Deniability) на базе безусловного кодирования COBS, при котором расшифрование произвольным неверным ключом выдаёт синтаксически корректные данные без индикатора ошибки.
• В паре с быстрыми современными PRF (AES, BLAKE2/3, Areion) конструкция пригодна для защищённого обмена сообщениями, хранения файлов и сетевых VPN-туннелей (при групповой пакетной очереди накладные расходы формата составляют около 15%). Для защиты от атак по сторонним каналам ядра выполняются за постоянное время (constant-time) с полной принудительной очисткой стековых фреймов и процессорных регистров (GPR, XMM/YMM/ZMM, NEON) после вызовов.
• Для архитектуры x86_64 реализованы ассемблерные ядра с использованием инструкций BMI2 (PEXT/PDEP), AES-NI, VAES, AVX2 и AVX-512, а для ARM64 (Aarch64) — на базе расширений NEON, Crypto Extensions и SVE2 (с переносимым откатом на чистый Go). Поверх единого C ABI (libitb3) подготовлены обвязки для 33 языков программирования.

Источник: opennet.ru