{"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\/de\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"ITB-Kryptographischer Isolator mit formellem Nachweis der Zuverl\u00e4ssigkeit","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Das ITB-Projekt wurde vorgestellt, das einen symmetrischen kryptographischen Isolator entwickelt, der daf\u00fcr ausgelegt ist, standardm\u00e4\u00dfige pseudo-zuf\u00e4llige Funktionen (PRF) und Hash-Primitiven (AES, BLAKE2\/3, Areion und andere) in eine gekoppelte kombinatorische und topologische Barriere zu h\u00fcllen. Im Gegensatz zu klassischen Block- und Stream-Verschl\u00fcsselungsmodi zielt die ITB-Architektur auf die strukturelle Isolation des internen Primitivs ab und verhindert die Ausbreitung von differentiellen und linearen Eigenschaften, algebraischer Linearisation sowie direkter Kodierungen f\u00fcr SAT\/SMT- und MILP-L\u00f6ser durch die Barrieregrenzen. Der Code ist in Go geschrieben und enth\u00e4lt niedrigstufige Optimierungen in Assembler f\u00fcr die Architekturen x86_64 und ARM64 (Aarch64) und wird unter der Apache 2.0-Lizenz verteilt.<\/p>\n
Die Datenumwandlung in ITB ist in zwei verbundene Ebenen (Interlocked Barrier) unterteilt, die von acht isolierten Schl\u00fcssel-Seed-Werten (8-seed isolation) mit lokaler Schl\u00fcsselkaskadierung \u00fcber eine direkte Verbindung (ChainHash) gesteuert werden. Auf der ersten Ebene f\u00fchrt die Rangbarriere (Rank Barrier) eine zentrale kombinatorische Permutation jedes 48-Bit-Blocks (oder 168-Bit-Blocks f\u00fcr 512-Bit-Primitiven) durch, wobei die Bits des Klartexts auf drei unabh\u00e4ngige Regionen verteilt werden, basierend auf einem zweistufigen Kombinationsfindungsverfahren nach seiner Nummer (der Raum der ausgewogenen Partitionen C(48, 16) * C(32, 16) betr\u00e4gt etwa 2^70.20, und im 168-Bit-Modus betr\u00e4gt C(168, 56) * C(112, 56) \u2014 etwa 2^258.60). Auf der zweiten Ebene verarbeitet die Pixelbarriere (Pixel Barrier) die Daten in eine Gitterstruktur aus 8-Byte-Elementen (8 Kan\u00e4le mit 7 Bit Daten und 1 Bit pseudorandomem Rauschen in jedem Byte) mit einem pixelgenauen, schl\u00fcsselgest\u00fctzten 7-Bit-Zyklischen Shift, wobei 7-Bit-Kan\u00e4le maskiert und die Position des Rauschbits ausgew\u00e4hlt wird.<\/p>\n
Die Hauptmerkmale des Projekts:<\/p>\n
\n
Experimentelle \u00dcberpr\u00fcfung der Isoliereigenschaften an eindeutig nicht-kryptographischen Funktionen (Stresstest mit schwachen Primitiven). Das Repository enth\u00e4lt einen Laborstand, der eine gew\u00f6hnliche Hash-Funktion FNV-1a innerhalb der Barriere einf\u00fchrt. Aufgrund der nichtlinearen kombinatorischen Rangordnung, der Aufteilung von Bytes an den Grenzen der 7-Bit-Kan\u00e4le (ggT(7, 8) = 1) und der Einspeisung von Rauschbits in jedes Byte wird der praktische Zugriff oder die Erstellung eines l\u00f6sbaren SAT\/SMT-Modells f\u00fcr den Klartext und den verschl\u00fcsselten Text bereits in der Phase der Formulierung des Gleichungssystems blockiert.\n
Maschinen\u00fcberpr\u00fcfte formale Verifikation in der Sprache Lean 4. Alle 12 grundlegenden mathematischen, kombinatorischen und bitvektor-Theoreme der Konstruktion (sowie das angewandte Hybrid-Schema zum Schl\u00fcssel\u00fcbereinstimmung 3-to-8 aus drei unabh\u00e4ngigen KEM-Kan\u00e4len in APPS.md), die im Dokument PROOFS.md beschrieben sind, wurden vollst\u00e4ndig in Lean 4 ohne Verwendung von Axiomen und Beweis\u00fcbertragungen bewiesen.\n
Eingebautes Werkzeug zur kryptanalytischen Testung, einschlie\u00dflich automatisierter Pr\u00fcfungen: statistische Testbatterien, Bewertung der algebraischen Gradzahl und Nichtlinearit\u00e4t, \u00dcberpr\u00fcfung der Isolation von Seeds durch Rauschspositionsselektion \u00fcber den CCA-Orakel und Auffindung von Schwachstellen durch externe Solver.\n
Zwei Betriebsmodi: Standard-Authentifizierungsmodus (AEAD nach dem MAC-Inside-Encrypt-Schema, wo der Tag innerhalb des Containers berechnet und verschl\u00fcsselt wird) und der Modus der plausiblen Abstreitbarkeit (Plausible Deniability) basierend auf bedingungsloser Kodierung COBS, bei dem die Entschl\u00fcsselung mit einem beliebigen falschen Schl\u00fcssel syntaktisch korrekte Daten ohne Fehlerindikator ausgibt.\n