{"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\/es\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Aislador criptogr\u00e1fico ITB con prueba formal de fiabilidad","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Se presenta el proyecto ITB, que desarrolla un aislante criptogr\u00e1fico sim\u00e9trico destinado a envolver funciones de pseudoaleatoriedad est\u00e1ndar (PRF) y primitivas de hash (AES, BLAKE2\/3, Areion y otras) en una barrera combinatoria y topol\u00f3gica intercalada. A diferencia de los modos de cifrado cl\u00e1sicos basados en bloques y flujos, la arquitectura ITB est\u00e1 enfocada en la aislamiento estructural del primitvo interno, impidiendo la propagaci\u00f3n de caracter\u00edsticas diferenciales y lineales, la linealizaci\u00f3n algebraica, as\u00ed como codificaciones directas para solucionadores SAT\/SMT y MILP a trav\u00e9s de los l\u00edmites de la barrera. El c\u00f3digo est\u00e1 escrito en el lenguaje Go con optimizaciones de bajo nivel en ensamblador para arquitecturas x86_64 y ARM64 (Aarch64) y se distribuye bajo la licencia Apache 2.0.<\/p>\n
La transformaci\u00f3n de datos en ITB se divide en dos niveles interconectados (Interlocked Barrier), gestionados por ocho semillas clave aisladas (8-seed isolation) con una evoluci\u00f3n local de la clave a trav\u00e9s de una cadena con conexi\u00f3n directa (ChainHash). En el primer nivel, la barrera de clasificaci\u00f3n (Rank Barrier) realiza una permutaci\u00f3n combinatoria clave de cada bloque de 48 bits (o bloque de 168 bits para primitivos de 512 bits), distribuyendo los bits del texto claro en tres regiones independientes en funci\u00f3n de la combinaci\u00f3n de dos pasos seg\u00fan su n\u00famero (el espacio de particiones equilibradas C(48, 16) * C(32, 16) es aproximadamente 2^70.20, y en modo de 168 bits C(168, 56) * C(112, 56) \u2014 aproximadamente 2^258.60). En el segundo nivel, la barrera de p\u00edxeles (Pixel Barrier) mapea los datos en una cuadr\u00edcula de elementos de 8 bytes (8 canales de 7 bits de datos y 1 bit de ruido pseudoaleatorio en cada byte) con un desplazamiento c\u00edclico clave de 7 bits por p\u00edxel, enmascaramiento de canales de 7 bits y selecci\u00f3n de la posici\u00f3n del bit de ruido.<\/p>\n
Caracter\u00edsticas principales del proyecto:<\/p>\n
\n
Verificaci\u00f3n experimental de las propiedades de aislamiento en funciones claramente no criptogr\u00e1ficas (prueba de estr\u00e9s con primitivas d\u00e9biles). El repositorio incluye un banco de pruebas que inserta una funci\u00f3n hash com\u00fan FNV-1a dentro de la barrera. A trav\u00e9s de la combinaci\u00f3n no lineal de la clasificaci\u00f3n, la divisi\u00f3n de bytes a lo largo de los l\u00edmites de los canales de 7 bits (MCD(7, 8) = 1) y la inyecci\u00f3n de bits de ruido en cada byte, se bloquea el acceso pr\u00e1ctico o la construcci\u00f3n de un modelo SAT\/SMT resolvible en el texto claro y cifrado ya en la etapa de formulaci\u00f3n del sistema de ecuaciones.\n
Verificaci\u00f3n formal comprobada por m\u00e1quina en el lenguaje Lean 4. Todas las 12 teoremas fundamentales matem\u00e1ticos, combinatorios y de vectores de bits de la construcci\u00f3n (as\u00ed como el esquema aplicado de acuerdo h\u00edbrido de claves 3 a 8 de tres canales KEM independientes en APPS.md), descritos en el documento PROOFS.md, est\u00e1n completamente probados en Lean 4 sin el uso de axiomas ni omisiones en las pruebas.\n
Herramienta integrada para pruebas criptogr\u00e1ficas que incluye comprobaciones automatizadas: bater\u00edas de pruebas estad\u00edsticas, evaluaci\u00f3n del grado algebraico y no linealidad, verificaci\u00f3n de la aislamiento de semillas al filtrar posiciones de ruido a trav\u00e9s de un or\u00e1culo CCA y b\u00fasqueda de vulnerabilidades mediante solucionadores externos.\n
Dos modos de operaci\u00f3n: modo autenticado est\u00e1ndar (AEAD seg\u00fan el esquema MAC-Inside-Encrypt, donde la inserci\u00f3n de mensaje se calcula y cifra dentro del contenedor) y modo de negaci\u00f3n plausible basado en codificaci\u00f3n incondicional COBS, donde la descifrado con una clave incorrecta produce datos sint\u00e1cticamente correctos sin indicador de error.\n