Криптографска изолатор 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