Provable countermeasures against Hardware Trojans

Poniższa praca omawia problem środków zaradczych wobec sprzętowych koni trojańskich (Hardware Trojan Horse, w skrócie HTH) rozumianych jako złośliwe i permanentne modyfikacje urządzeń obliczeniowych. Skupiamy się na rozwiązaniach, których bezpieczeństwo można formalnie wykazać. Urządzenia obliczeniowe modelujemy jako obwody logiczne i uwzględniamy możliwość mo dyfikacji przez przeciwnika. Zakres tej modyfikacji różni się w zależności od modelu – czasem przeciwnik może zastąpić układ innym, a czasem musi za chować jego pierwotną topologię. W każdym wypadku HTH jest cyfrowy, co oznacza, że może używać tylko oficjalnych kanałów wejścia i wyjścia w komuni kacji ze światem zewnętrznym. Pracę rozpoczynamy od przeglądu istniejących w literaturze środków zaradczych wykorzystujących takie narzędzia kryptogra ficzne, jak Verifiable Computation, Multi-Party Computation oraz Interactive Coding. W pozostałej części pracy prezentujemy nowe metod obrony przez HTH: Very Simple Compilers oraz Efficiently Testable Circuits. Wszystkie metody obrony przed HTH zaprezentowane w pracy (zarówno ist niejące, jak i nowe) składają się z co najmniej jednego z następujących dwóch elementów: (i) kompilatora obwodów, (ii) procedury testującej. Kompilator ob wodów to procedura, która dla danego obwodu F realizującego funkcjonalność F, generuje obwód Fb, który również realizuje F. Fb składa się z części pro dukowanych w sposób niezaufany – mówimy, że są zainfekowane HTH – oraz, czasami, prostego modułu produkowanego w sposób zaufany zwanego modu łem głównym. Procedura testowania działa zwykle w następujący sposób: życie obwodu zostaje podzielone na dwie fazy – laboratoryjną oraz na wolności. Ob wód Fb w fazie laboratoryjnej otrzymuje wejścia (a) z dowolnego zbioru lub (b) losowo wybrane z określonego rozkładu; jego wyjścia są porównywane z warto ściami referencyjnymi. Jeśli się zgadzają (tj. urządzenie przechodzi test labo ratoryjny), rozpoczyna życie na wolności, gdzie otrzymuje wejścia (a) wybrane przez przeciwnika lub (b) z określonego rozkładu. Długości tych faz mierzone są w liczbie wywołań. Jako pierwszy środek zaradczy prezentujemy schemat ochrony przed HTH, który przekształca dowolny obwód F w obwód efektywnie testowalny (Effi ciently Testable Circuit) Fb i jego zbiór testowy T. Zaproponowana przez nas konstrukcja ma przekonujące parametry – bezpieczeństwo może zostać złamane z zaniedbywalnym prawdopodobieństwem, nawet gdy długość fazy na wolności. jest nieograniczona; kompilacja układu zwiększa jego rozmiar w sposób liniowy z czynnikiem mniejszym niż 20; wielkość zbioru testowego jest stała. W do wodzie bezpieczeństwa wykorzystujemy nowe pojęcie utraty informacji (infor mation loss). Wykorzystuje ono podstawową ideę entropii Shannona, ale bez odniesienia do miary prawdopodobieństwa. Wyniki są przedstawione w pracach Mirza Ahad Baig, Suvradip Chakraborty, Stefan Dziembowski, Małgorzata Ga łązka, Tomasz Lizurej i Krzysztof Pietrzak, Efficiently Testable Circuits. ITCS - Innovations in Theoretical Computer Science 2023; Mirza Ahad Baig, Suvra dip Chakraborty, Stefan Dziembowski, Małgorzata Gałązka, Tomasz Lizurej i Krzysztof Pietrzak, Efficiently Testable Circuits Without Conductivity. Theory of Cryptography Conference 2023. Jako drugi środek zaradczy prezentujemy Very Simple Schemes. W tym wy padku skompilowany układ Fb składa się z modułu głównego oraz niezaufanych instancji F. Głównym celem w tym wypadku jest maksymalne uproszczenie modułu głównego urządzenia oraz minimalne zwiększenie wielkości skompilo wanego układu. Prezentujemy konstrukcję, która spełnia osiągalne parametry bezpieczeństwa takich schematów. Ten środek przeciwdziała HTH, które mogą całkowicie zmodyfikować układ; urządzenie na wolności otrzymuje losowe wej ścia. Ten wynik został przedstawiony w pracy Suvradip Chakraborty, Stefan Dziembowski, Małgorzata Gałązka, Tomasz Lizurej, Krzysztof Pietrzak i Mi chelle Yeo, Trojan-resilience without cryptography. Theory of Cryptography Conference 2021.

The thesis addresses the problem of countermeasures against Hardware Tro jan Horses (HTHs), understood as adversarial and permanent modifications of computational devices. We focus on solutions that can be formally proven to be secure. We model a computational device as a logical circuit and incorpo rate the possibility of malicious modification. The scope of such modification varies – sometimes, the adversary can replace the circuit with another one, and sometimes, the adversary needs to preserve the original topology. In any case, the HTH is digital, by which we mean that it can use only official input/output channels to communicate. We start with a short survey of prior solutions based on cryptographic primitives such as Verifiable Computation, Multi-Party Com putation, and Interactive Coding. Then, we proceed to the main technical part of this thesis, i.e., we propose and investigate in-depth novel countermeasures: Very Simple Circuit Compilers and Efficiently Testable Circuits. All of the protection schemes against HTHs (both already existing in the literature and the ones presented in this thesis) consist of at least one of the following two parts: (i) circuit compiler and (ii) testing procedure. Circuit compiler is a procedure which, for a given circuit F which realizes functionality F, outputs another circuit Fb, which also realizes F. Fb consists of parts the adversary can modify – we say that they are HTH-infected – and, sometimes, a simple trustfully manufactured part called a master module. Most of the testing procedures work in the following way: the lifecycle of the circuit Fb is divided into two phases – lab phase and wild phase. Circuit Fb during the lab phase is given inputs (a) from an arbitrary set or (b) randomly chosen with a particular distribution; its outputs are compared to reference values. If they agree (i.e., the device passes the lab), it is released into the wild, where Fb is given inputs (a) chosen by the adversary or (b) from a particular distribution. The lengths of these phases are measured in the number of invocations. As the first result, we propose a protection scheme against HTHs which can permanently tamper with Fb. This scheme transforms every F into Efficiently Testable Circuit Fb and its test set T. The construction achieves convincing pa rameters: security is granted with overwhelming or equal 1 probability for the unbounded length of the wild phase; the overhead in the size of the compiled circuit is linear with a factor less than 20; the size of the test set is constant (or linear in the security parameter for more advanced setting). We use a new notion of information loss in the security proof. It inherits a basic idea from Shannon’s entropy but without relation to the probability measure. The re sults are presented in papers Mirza Ahad Baig, Suvradip Chakraborty, Stefan Dziembowski, Małgorzata Gałązka, Tomasz Lizurej, and Krzysztof Pietrzak, Efficiently Testable Circuits. ITCS - Innovations in Theoretical Computer Sci ence 2023; Mirza Ahad Baig, Suvradip Chakraborty, Stefan Dziembowski, Mał- gorzata Gałązka, Tomasz Lizurej, and Krzysztof Pietrzak, Efficiently Testable Circuits Without Conductivity. Theory of Cryptography Conference 2023. The second original result is a notion of Very Simple Schemes. Here, the compiled circuit Fb consists of a master module and some untrusted instanti ations of F. This approach has two main objectives: simplifying the device’s master module and minimal overhead in the size of the compiled circuit. We show a construction that meets such schemes’ achievable security parameters. This countermeasure thwarts HTHs, which can completely modify the circuit; we do not allow the adversary to influence the input the circuit receives in the wild. This result was presented in Suvradip Chakraborty, Stefan Dziembowski, Małgorzata Gałązka, Tomasz Lizurej, Krzysztof Pietrzak, and Michelle Yeo, Trojan-resilience without cryptography. Theory of Cryptography Conference 2021.