{"id":184113,"date":"2026-11-03T23:41:02","date_gmt":"2026-11-03T21:41:02","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/kriptograficheskij-izolyator-itb-s-formalnym-dokazatelstvom-nadyozhnosti"},"modified":"2026-11-03T23:41:07","modified_gmt":"2026-11-03T21:41:07","slug":"itb-cryptographic-isolator-with-formally-proven-reliability","status":"publish","type":"post","link":"https:\/\/prohoster.info\/pt\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Isolador criptogr\u00e1fico ITB com prova formal de confiabilidade","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Foi apresentado o projeto ITB, que desenvolve um isolador criptogr\u00e1fico sim\u00e9trico destinado a encapsular fun\u00e7\u00f5es pseudoaleat\u00f3rias padr\u00e3o (PRF) e primitivas de hash (AES, BLAKE2\/3, Areion e outras) em uma barreira combinat\u00f3ria e topol\u00f3gica interligada. Ao contr\u00e1rio dos modos cl\u00e1ssicos de cifragem em bloco e fluxo, a arquitetura ITB tem como alvo a isola\u00e7\u00e3o estrutural da primitiva interna, impedindo a propaga\u00e7\u00e3o de caracter\u00edsticas diferenciais e lineares, lineariza\u00e7\u00e3o alg\u00e9brica, bem como codifica\u00e7\u00f5es diretas para solucionadores SAT\/SMT e MILP atrav\u00e9s das fronteiras da barreira. O c\u00f3digo \u00e9 escrito em Go com otimiza\u00e7\u00f5es de baixo n\u00edvel em assembly para as arquiteturas x86_64 e ARM64 (Aarch64) e \u00e9 distribu\u00eddo sob a licen\u00e7a Apache 2.0.<\/p>\n
A convers\u00e3o de dados em ITB \u00e9 dividida em dois n\u00edveis interligados (Interlocked Barrier), geridos por oito sementes de chave isoladas (isolamento de 8-seed) com a evolu\u00e7\u00e3o local da chave atrav\u00e9s de um cascata com conex\u00e3o direta (ChainHash). No primeiro n\u00edvel, a barreira de classifica\u00e7\u00e3o (Rank Barrier) realiza uma permuta\u00e7\u00e3o combinat\u00f3ria chave de cada bloco de 48 bits (ou bloco de 168 bits para primitivos de 512 bits), distribuindo os bits do texto claro em tr\u00eas regi\u00f5es independentes com base na combina\u00e7\u00e3o de dois est\u00e1gios pelo seu n\u00famero (o espa\u00e7o das parti\u00e7\u00f5es balanceadas C(48, 16) * C(32, 16) \u00e9 aproximadamente 2^70.20, enquanto no modo de 168 bits C(168, 56) * C(112, 56) \u2014 \u00e9 cerca de 2^258.60). No segundo n\u00edvel, a barreira de pixel (Pixel Barrier) mapeia os dados para uma grade de elementos de 8 bytes (8 canais com 7 bits de dados e 1 bit de ru\u00eddo pseudoaleat\u00f3rio em cada byte) com um deslocamento c\u00edclico de chave de 7 bits por pixel, mascaramento de canais de 7 bits e sele\u00e7\u00e3o de posi\u00e7\u00e3o do bit de ru\u00eddo.<\/p>\n
Principais caracter\u00edsticas do projeto:<\/p>\n
\n
Verifica\u00e7\u00e3o experimental das propriedades isolantes em fun\u00e7\u00f5es deliberadamente n\u00e3o criptogr\u00e1ficas (teste de estresse com primitivas fracas). O reposit\u00f3rio inclui um banco de testes que insere uma fun\u00e7\u00e3o hash comum FNV-1a dentro da barreira. Gra\u00e7as \u00e0 combina\u00e7\u00e3o n\u00e3o linear de ranqueamento, divis\u00e3o de bytes nas fronteiras dos canais de 7 bits (GCD(7, 8) = 1) e inje\u00e7\u00e3o de bits de ru\u00eddo em cada byte, o uso pr\u00e1tico ou a constru\u00e7\u00e3o de um modelo SAT\/SMT resolv\u00edvel a partir do texto claro e criptografado \u00e9 bloqueado j\u00e1 na etapa de formula\u00e7\u00e3o do sistema de equa\u00e7\u00f5es.\n
Verifica\u00e7\u00e3o formal validada por m\u00e1quina na linguagem Lean 4. Todos os 12 teoremas fundamentais de matem\u00e1tica, combinat\u00f3ria e vetores de bits da constru\u00e7\u00e3o (bem como o esquema aplicado de consenso h\u00edbrido de chaves 3-para-8 de tr\u00eas canais KEM independentes em APPS.md), descritos no documento PROOFS.md, s\u00e3o completamente comprovados no Lean 4 sem o uso de axiomas ou lacunas nas provas.\n
Um conjunto de ferramentas de teste criptoanal\u00edtico integrado, que inclui verifica\u00e7\u00f5es automatizadas: baterias de testes estat\u00edsticos, avalia\u00e7\u00e3o do grau alg\u00e9brico e n\u00e3o linearidade, verifica\u00e7\u00e3o da separa\u00e7\u00e3o de sementes ao filtrar posi\u00e7\u00f5es de ru\u00eddo atrav\u00e9s do or\u00e1culo CCA e busca por vulnerabilidades com a ajuda de solucionadores externos.\n
Dois modos de opera\u00e7\u00e3o: modo autenticado padr\u00e3o (AEAD baseado na esquema MAC-Inside-Encrypt, onde a inser\u00e7\u00e3o de mensagem \u00e9 calculada e criptografada dentro do cont\u00eainer) e modo de nega\u00e7\u00e3o plaus\u00edvel (Plausible Deniability) baseado na codifica\u00e7\u00e3o incondicional COBS, onde a descriptografia com uma chave incorreta gera dados sintaticamente corretos sem indicador de erro.\n