{"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\/nl\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"ITB Cryptografische Isolator met formeel bewijs van betrouwbaarheid","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Het ITB-project is gepresenteerd, dat een symmetrische cryptografische isolator ontwikkelt, ontworpen voor het verpakken van standaard pseudo-willekeurige functies (PRF) en hash-primitive data (AES, BLAKE2\/3, Areion en anderen) in een gekoppelde combinatorische en topologische barri\u00e8re. In tegenstelling tot klassieke blok- en stroomversleuteling, richt de ITB-architectuur zich op structurele isolatie van de interne primitief, waardoor de verspreiding van differenti\u00eble en lineaire kenmerken, algebra\u00efsche linearisatie, evenals directe coderingen voor SAT\/SMT- en MILP-oplossers door de grenzen van de barri\u00e8re wordt voorkomen. De code is geschreven in de programmeertaal Go, met laag-niveau optimalisaties in assembly voor de architecturen x86_64 en ARM64 (Aarch64) en wordt verspreid onder de Apache 2.0-licentie.<\/p>\n
Gegevensconversie in ITB is verdeeld in twee onderling verbonden niveaus (Interlocked Barrier), beheerd door acht ge\u00efsoleerde belangrijke zaden (8-seed isolation) met lokale sleutelontwikkeling via een ketting met directe koppeling (ChainHash). Op het eerste niveau voert de rangbarri\u00e8re (Rank Barrier) een sleutelcombinatoire permutatie uit van elk 48-bits blok (of 168-bits blok voor 512-bits primitieven), waarbij de bits van de platte tekst worden verdeeld over drie onafhankelijke regio's op basis van de tweestapscombinatoriek volgens zijn nummer (de ruimte van gebalanceerde verdelingen C(48, 16) * C(32, 16) is ongeveer 2^70.20, en in de 168-bits modus C(168, 56) * C(112, 56) \u2014 ongeveer 2^258.60). Op het tweede niveau projecteert de pixelbarri\u00e8re (Pixel Barrier) de gegevens op een raster van 8-byte elementen (8 kanalen met 7 bits gegevens en 1 bit pseudowillekeurige ruis in elke byte) met een pixelgewijze sleutel 7-bits cyclische verschuiving, maskering van 7-bits kanalen en selectie van de positie van het ruisbit.<\/p>\n
Belangrijkste kenmerken van het project:<\/p>\n
\n
Experimentele verificatie van isolerende eigenschappen op van tevoren niet-cryptografische functies (stress-test met zwakke primitieven). De repository omvat een laboratoriumopstelling die een reguliere hash-functie FNV-1a binnen de barri\u00e8re invoert. Door middel van niet-lineaire combinatorische rangschikking, het splitsen van bytes langs de grenzen van 7-bits kanalen (grootste gemene deler (7, 8) = 1) en het injecteren van ruisbits in elke byte, wordt praktische toegang of de opbouw van een oplosbare SAT\/SMT-model op open en versleutelde tekst al geblokkeerd in het stadium van het formuleren van het systeem van vergelijkingen.\n
Formele verificatie, gecontroleerd door machines, in de Lean 4-taal. Alle 12 basiswiskundige, combinatorische en bitvectorstellingen van de constructie (inclusief de toegepaste hybride sleuteloverdracht van 3 naar 8 uit drie onafhankelijke KEM-kanalen in APPS.md), beschreven in het document PROOFS.md, zijn volledig bewezen in Lean 4 zonder het gebruik van axioma's en bewijsleemten.\n
Ingebouwde instrumenten voor cryptografische testen, waaronder geautomatiseerde controles: statistische testbatterijen, beoordeling van algebra\u00efsche graad en niet-lineariteit, verificatie van de isolatie van zaden bij het filteren van ruisposities via de CCA-orakel en het zoeken naar kwetsbaarheden met externe oplosser.\n
Twee werkmodi: standaard geauthenticeerde modus (AEAD volgens het MAC-Inside-Encrypt-schema, waarbij de tag wordt berekend en binnen de container wordt versleuteld) en de modus van plausibele ontkenning (Plausible Deniability) op basis van onvoorwaardelijke codering COBS, waarbij het ontsleutelen met een willekeurige onjuiste sleutel syntactisch correcte gegevens oplevert zonder foutindicator.\n