{"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\/pl\/blog\/news\/itb-cryptographic-isolator-with-formally-proven-reliability","title":{"rendered":"Izolator kryptograficzny ITB z formalnym dowodem niezawodno\u015bci","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Przedstawiono projekt ITB, rozwijaj\u0105cy symetryczny izolator kryptograficzny, zaprojektowany do opakowywania standardowych pseudolosowych funkcji (PRF) oraz funkcji skr\u00f3tu (AES, BLAKE2\/3, Areion i innych) w sprz\u0119\u017con\u0105 barier\u0119 kombinatoryczn\u0105 i topologiczn\u0105. W przeciwie\u0144stwie do klasycznych tryb\u00f3w szyfrowania blokowego i strumieniowego, architektura ITB koncentruje si\u0119 na strukturalnej izolacji wewn\u0119trznego prymitywu, zapobiegaj\u0105c rozprzestrzenieniu w\u0142a\u015bciwo\u015bci r\u00f3\u017cnicowych i liniowych, algebrycznej liniaryzacji oraz bezpo\u015brednim kodowaniom dla rozwi\u0105zuj\u0105cych SAT\/SMT i MILP przez granice bariery. Kod jest napisany w j\u0119zyku Go z niskopoziomowymi optymalizacjami w asemblerze dla architektur x86_64 i ARM64 (Aarch64) i jest rozpowszechniany na mocy licencji Apache 2.0.<\/p>\n
Transformacja danych w ITB zosta\u0142a podzielona na dwa po\u0142\u0105czone poziomy (Interlocked Barrier), zarz\u0105dzane przez osiem izolowanych kluczy nasion (8-seed isolation) z lokaln\u0105 ewolucj\u0105 klucza przez kaskad\u0119 z bezpo\u015brednim po\u0142\u0105czeniem (ChainHash). Na pierwszym poziomie bariera rankingu (Rank Barrier) wykonuje kluczow\u0105 kombinacyjn\u0105 permutacj\u0119 ka\u017cdego 48-bitowego bloku (lub 168-bitowego bloku dla 512-bitowych prymityw\u00f3w), rozdzielaj\u0105c bity tekstu jawnego na trzy niezale\u017cne obszary w oparciu o dwustopniowe znajdowanie kombinacji wed\u0142ug jego numeru (przestrze\u0144 zr\u00f3wnowa\u017conych podzia\u0142\u00f3w C(48, 16) * C(32, 16) wynosi oko\u0142o 2^70.20, a w trybie 168-bitowym C(168, 56) * C(112, 56) \u2014 oko\u0142o 2^258.60). Na drugim poziomie bariera pikselowa (Pixel Barrier) odwzorowuje dane na siatk\u0119 8-bajtowych element\u00f3w (8 kana\u0142\u00f3w po 7 bit\u00f3w danych i 1 bit pseudolosowego szumu w ka\u017cdym bajcie) z pikselowym kluczem 7-bitowego cyklicznego przesuni\u0119cia, maskowaniem 7-bitowych kana\u0142\u00f3w i wyborem pozycji bitu szumowego.<\/p>\n
G\u0142\u00f3wne cechy projektu:<\/p>\n
\n
Eksperymentalne sprawdzenie w\u0142a\u015bciwo\u015bci izolacyjnych na jawnie niekryptograficznych funkcjach (test obci\u0105\u017ceniowy z s\u0142abymi prymitywami). W sk\u0142ad repozytorium wchodzi laboratoryjna platforma, w kt\u00f3rej wewn\u0105trz bariery wstawiana jest zwyk\u0142a funkcja skr\u00f3tu FNV-1a. Dzi\u0119ki nieliniowemu kombinacyjnemu rozrzutowi, podzia\u0142owi bajt\u00f3w na granicach 7-bitowych kana\u0142\u00f3w (NWD(7, 8) = 1) oraz wstrzykiwaniu bit\u00f3w szumowych do ka\u017cdego bajtu, praktyczne odwrotne lub budowanie rozwi\u0105zywalnego modelu SAT\/SMT na podstawie tekstu jawnego i zaszyfrowanego jest blokowane ju\u017c na etapie formu\u0142owania systemu r\u00f3wna\u0144.\n
Automatycznie weryfikowana formalna weryfikacja w j\u0119zyku Lean 4. Wszystkie 12 podstawowych twierdze\u0144 matematycznych, kombinatorycznych i bitowych konstrukcji (a tak\u017ce aplikacyjny schemat hybrydowego uzgadniania kluczy 3-do-8 z trzech niezale\u017cnych kana\u0142\u00f3w KEM w APPS.md), opisane w dokumencie PROOFS.md, zosta\u0142y w pe\u0142ni udowodnione w Lean 4 bez u\u017cycia aksjomat\u00f3w i pomini\u0119\u0107 dowod\u00f3w.\n
Wbudowane narz\u0119dzie migaj\u0105cy testy kryptograficzne, w tym zautomatyzowane kontrole: statystyczne serie test\u00f3w, ocen\u0119 stopnia algebraicznego i nieliniowo\u015bci, kontrol\u0119 izolacji nasion przy odrzucaniu pozycji szum\u00f3w przez orakl CCA oraz poszukiwanie luk bezpiecze\u0144stwa za pomoc\u0105 zewn\u0119trznych rozwi\u0105za\u0144.\n
Dwa tryby pracy: standardowy uwierzytelniony tryb (AEAD wed\u0142ug schematu MAC-Inside-Encrypt, gdzie wstawka uwierzytelania jest obliczana i szyfrowana wewn\u0105trz kontenera) oraz tryb wiarygodnego zaprzeczenia (Plausible Deniability) oparty na bezwarunkowym kodowaniu COBS, w kt\u00f3rym odszyfrowanie dowolnym nieprawid\u0142owym kluczem daje syntaktycznie poprawne dane bez wska\u017anika b\u0142\u0119du.\n