Isolador criptográfico ITB com prova formal de confiabilidade

Foi apresentado o projeto ITB, que desenvolve um isolador criptográfico simétrico destinado a encapsular funções pseudoaleatórias padrão (PRF) e primitivas de hash (AES, BLAKE2/3, Areion e outras) em uma barreira combinatória e topológica interligada. Ao contrário dos modos clássicos de cifragem em bloco e fluxo, a arquitetura ITB tem como alvo a isolação estrutural da primitiva interna, impedindo a propagação de características diferenciais e lineares, linearização algébrica, bem como codificações diretas para solucionadores SAT/SMT e MILP através das fronteiras da barreira. O código é escrito em Go com otimizações de baixo nível em assembly para as arquiteturas x86_64 e ARM64 (Aarch64) e é distribuído sob a licença Apache 2.0.

A transformação de dados no ITB é dividida em dois níveis interligados (Interlocked Barrier), geridos por oito sementes isoladas (8-seed isolation) com evolução de chave local através de uma cadeia com ligação direta (ChainHash). No primeiro nível, a barreira de ranqueamento (Rank Barrier) executa uma permutação combinatória chave de cada bloco de 48 bits (ou bloco de 168 bits para primitivas de 512 bits), distribuindo os bits do texto claro em três regiões independentes com base na combinação de dois passos, de acordo com seu número (o espaço de divisões equilibradas C(48, 16) * C(32, 16) é cerca de 2^70.20, e no modo de 168 bits C(168, 56) * C(112, 56) é cerca de 2^258.60). No segundo nível, a barreira de pixel (Pixel Barrier) mapeia os dados em uma grade de elementos de 8 bytes (8 canais com 7 bits de dados e 1 bit de ruído pseudoaleatório em cada byte) com um deslocamento cíclico de 7 bits da chave por pixel, mascaramento de canais de 7 bits e escolha de posição do bit de ruído.

Principais características do projeto:

• Verificação experimental das propriedades isolantes em funções deliberadamente não criptográficas (teste de estresse com primitivas fracas). O repositório inclui um banco de testes que insere uma função hash comum FNV-1a dentro da barreira. Graças à combinação não linear de ranqueamento, divisão de bytes nas fronteiras dos canais de 7 bits (GCD(7, 8) = 1) e injeção de bits de ruído em cada byte, o uso prático ou a construção de um modelo SAT/SMT resolvível a partir do texto claro e criptografado é bloqueado já na etapa de formulação do sistema de equações.
• Verificação formal validada por máquina na linguagem Lean 4. Todos os 12 teoremas fundamentais de matemática, combinatória e vetores de bits da construção (bem como o esquema aplicado de consenso híbrido de chaves 3-para-8 de três canais KEM independentes em APPS.md), descritos no documento PROOFS.md, são completamente comprovados no Lean 4 sem o uso de axiomas ou lacunas nas provas.
• Um conjunto de ferramentas de teste criptoanalítico integrado, que inclui verificações automatizadas: baterias de testes estatísticos, avaliação do grau algébrico e não linearidade, verificação da separação de sementes ao filtrar posições de ruído através do oráculo CCA e busca por vulnerabilidades com a ajuda de solucionadores externos.
• Dois modos de operação: modo autenticado padrão (AEAD baseado na esquema MAC-Inside-Encrypt, onde a inserção de mensagem é calculada e criptografada dentro do contêiner) e modo de negação plausível (Plausible Deniability) baseado na codificação incondicional COBS, onde a descriptografia com uma chave incorreta gera dados sintaticamente corretos sem indicador de erro.
• Em conjunto com PRFs modernas e rápidas (AES, BLAKE2/3, Areion), a construção é adequada para troca de mensagens segura, armazenamento de arquivos e redes VPN-túneis (com o custo de formato em fila de pacotes agrupados de cerca de 15%). Para proteção contra ataques de canais laterais, os núcleos são executados em tempo constante (constant-time) com limpeza forçada completa dos quadros da pilha e registros de processador (GPR, XMM/YMM/ZMM, NEON) após chamadas.
• Para a arquitetura x86_64, núcleos em assembleia são implementados utilizando instruções BMI2 (PEXT/PDEP), AES-NI, VAES, AVX2 e AVX-512, e para ARM64 (Aarch64) - com base nas extensões NEON, Crypto Extensions e SVE2 (com retrocesso portátil para Go puro). Sobre uma única C ABI (libitb3), foram criados bindings para 33 linguagens de programação.

Fonte: opennet.ru