Miesiąc: czerwiec 2026

https://chacker.pl/

Pierwszą rzeczą, którą zauważysz na Listingu 13-2, jest to, że zawiera on plik ../inc/loader.h (1), ponieważ backward_slicing korzysta z modułu ładującego pliki binarne opracowanego w rozdziale 4. Zawiera on również pliki triton_util.h i isasm_util.h, które udostępniają funkcje narzędziowe, które wkrótce opiszę. Na koniec znajdują się dwa pliki nagłówkowe specyficzne dla Tritona, oba z rozszerzeniem .hpp: triton/api.hpp zawiera główne API Tritona w C++, a triton/x86Specifications.hpp zawiera definicje specyficzne dla architektury x86, takie jak definicje rejestrów. Oprócz dołączenia tych plików nagłówkowych, należy połączyć je z opcją -ltriton, aby korzystać z trybu emulacji symbolicznej Tritona. Funkcja główna rozpoczyna się od załadowania analizowanego pliku binarnego za pomocą funkcji load_binary modułu ładującego pliki binarne. Następnie konfiguruje Tritona do architektury pliku binarnego za pomocą funkcji o nazwie et_triton_arch (2), zdefiniowanej w pliku backward_slicing.cc, którą omówię szczegółowo w sekcji 13.3.4. Wywołuje również funkcję api.enableMode Tritona, aby włączyć tryb ALIGNED_MEMORY Tritona, gdzie api jest obiektem typu triton::API, który jest główną klasą Tritona udostępniającą API C++. Należy pamiętać, że dostęp do pamięci symbolicznej może znacznie zwiększyć rozmiar i złożoność stanu symbolicznego, ponieważ silnik Symbex musi modelować wszystkie możliwe wyniki dostępu do pamięci. Tryb ALIGNED_MEMORY Tritona to optymalizacja, która zmniejsza eksplozję pamięci symbolicznej, zakładając, że pamięć ładuje i przechowuje adresy pamięci wyrównane z dostępem. Można bezpiecznie włączyć tę optymalizację, jeśli wiadomo, że dostęp do pamięci jest wyrównany lub jeśli dokładne adresy pamięci nie mają znaczenia dla analizy.

https://chacker.pl/

Ten pierwszy przykład implementuje wsteczne cięcie w trybie emulacji symbolicznej Tritona. Ten przykład jest uogólnioną wersją przykładu dołączonego do Tritona, który można znaleźć w pliku ~/triton/pin-2.14-71313-gcc.4.4.7-linux/source/tools/Triton/src/examples/python/backward_slicing.py. Oryginalne narzędzie Triton korzysta z API Pythona, ale tutaj wykorzystam API Tritona w językach C/C++. Przykład narzędzia Triton napisanego w Pythonie znajduje się w rozdziale 13.5. Przypomnijmy, że wsteczne cięcie to technika analizy binarnej, która informuje, w pewnym momencie wykonywania, które poprzednie instrukcje przyczyniły się do wartości danego rejestru lub adresu pamięci. Na przykład, załóżmy, że chcesz obliczyć wycinek wsteczny pod adresem 0x404b1e względem rcx we fragmencie kodu z /bin/ls pokazanym na Listingu .

Listing : Fragment deasemblacji z /bin/ls

Wycinek wsteczny składa się ze wszystkich instrukcji, które wpływają na wartość rcx pod adresem 0x404b1e(1). Zatem wycinek powinien zawierać instrukcje pokazane na poniższym listingu. Zobaczmy teraz, jak automatycznie obliczać wycinki wsteczne, takie jak ten, za pomocą Tritona. Najpierw nauczysz się budować narzędzie do wycinków wstecznych, a następnie użyjesz go do wycięcia fragmentu kodu pokazanego na Listingu 13-1, uzyskując ten sam wynik, co ręczny wycinek, który właśnie widziałeś. Ponieważ Triton wyraża wyrażenia symboliczne jako AST, które odwołują się do siebie nawzajem, łatwo jest obliczyć wycinek wsteczny dla danego wyrażenia. Listing przedstawia pierwszą część implementacji narzędzia do wycinków wstecznych. Jak zwykle, pominąłem w tym listingu standardowe pliki nagłówkowe C/C++.

Listing: backward_slicing.cc

Aby użyć narzędzia, należy podać mu nazwę pliku binarnego do analizy, symboliczny plik konfiguracyjny, adres punktu wejścia, od którego ma rozpocząć się analiza, adres, od którego ma zostać obliczony wycinek, oraz rejestr, względem którego ma zostać obliczony wycinek – wszystko za pomocą argumentów wiersza poleceń. Za chwilę wyjaśnię cel symbolicznego pliku konfiguracyjnego. Należy zauważyć, że w tym przypadku adres punktu wejścia to po prostu adres pierwszej instrukcji, którą narzędzie do wycinania będzie emulować; nie musi być taki sam jak punkt wejścia pliku binarnego. Na przykład, aby wyciąć przykładowy kod z Listingu 1, należy użyć 0x404b00 jako adresu punktu wejścia, aby analiza emulowała wszystkie instrukcje pokazane na listingu aż do adresu wycinka. Wyjściem backward_slicing jest lista instrukcji asemblera, które znajdują się w wycinku. Przyjrzyjmy się teraz dokładniej, jak backward_slicing  generuje wycinek programu, zaczynając od bardziej szczegółowego omówienia niezbędnych elementów include i funkcji main.

https://chacker.pl/

Możesz zauważyć, że pełne AST zawierają wiele redundancji: za każdym razem, gdy AST zależy od poprzedniego, cały poprzedni AST staje się poddrzewem w nowym. Duże i złożone programy mają wiele zależności między operacjami, więc poprzedni schemat powoduje niepotrzebne obciążenie pamięci. Dlatego Triton reprezentuje AST w bardziej zwarty sposób . W tym schemacie każdy AST ma nazwę, taką jak ref!1, ref!2 itd., do której można się odwołać z innego AST. W ten sposób, zamiast kopiować cały poprzedni AST, można po prostu odwołać się do niego, umieszczając węzeł referencyjny w nowym AST. Na przykład, prawa strona rysunku 13-1 pokazuje, jak całe lewe poddrzewo w AST eax po instrukcji and eax,0x1 można zastąpić pojedynczym węzłem referencyjnym, który odwołuje się do poprzedniego AST, kompresując 15 węzłów do zaledwie jednego. Triton oferuje funkcję API o nazwie unrollAst, która pozwala na rozwinięcie AST z referencjami do pełnego AST, co umożliwia jego ręczną inspekcję, manipulację lub przekazanie do Z3. Teraz, gdy znasz już podstawy działania Tritona, nauczmy się, jak korzystać z unrollAst i innych funkcji Tritona w praktyce, przyglądając się kilku przykładom.

https://chacker.pl/

Rysunek zakłada, że ​​eax i cl są początkowo mapowane na nieograniczone wyrażenia symboliczne odpowiadające odpowiednio 32-bitowej wartości symbolicznej α1 i 8-bitowej wartości symbolicznej α2. Na przykład, można zauważyć, że stan początkowy dla eax (1) to zbiór AST zakorzeniony w węźle bv (wektor bitowy), z dwoma węzłami potomnymi zawierającymi wartości α1 i 32. Odpowiada to nieograniczonemu 32-bitowemu wektorowi bitowemu Z3, jak w (declare-const alpha1 (_ BitVec 32)). Instrukcja shr eax,cl to logiczne przesunięcie w prawo, które używa eax i cl jako operandów i zapisuje wynik w eax. Zatem po tej instrukcji (2) pełne AST dla eax ma węzeł bvlshr (logiczne przesunięcie w prawo) jako swój korzeń, z drzewami potomnymi reprezentującymi oryginalne AST dla eax i cl. Należy zauważyć, że prawe drzewo potomne, reprezentujące zawartość cl, ma swój korzeń w operacji konkata, która poprzedza wartość cl 24 bitami zerowymi. Jest to konieczne, ponieważ cl ma tylko 8 bitów szerokości, ale należy je rozszerzyć do 32 bitów (tyle samo co eax), ponieważ format SMT-LIB 2.0 używany przez Z3 wymaga, aby oba operandy bvlshr miały tę samą szerokość bitową. Po instrukcji xor eax,0x1 (3) AST dla eax staje się węzłem bvxor z poprzednim AST eax jako lewym poddrzewem i stałym wektorem bitowym zawierającym wartość 1 jako prawym poddrzewem. Podobnie, eax,0x1 (4) skutkuje AST zakorzenionym w węźle bvand, ponownie z poprzednim AST eax jako lewym poddrzewem i stałym wektorem bitowym jako prawym.

https://chacker.pl/

Zarówno w trybie emulacji, jak i w trybie konkolicznym, Triton utrzymuje globalny zestaw wyrażeń symbolicznych, mapowanie rejestrów i adresów pamięci na te wyrażenia symboliczne oraz listę ograniczeń ścieżki, podobnie jak na rysunku 12-1 z rozdziału 12. Triton reprezentuje wyrażenia symboliczne i ograniczenia jako abstrakcyjne drzewa składniowe (AST), z jednym AST na każde wyrażenie lub ograniczenie. AST to struktura danych w postaci drzewa, która przedstawia relacje składniowe między operacjami a operandami. Węzły AST zawierają operacjei operandy w języku SMT systemu Z3. Na przykład rysunek 13-1 pokazuje, jak AST dla rejestru eax ewoluuje w następującej sekwencji trzech instrukcji:

shr eax,cl

xor eax,0x1

and eax,0x1

Dla każdej instrukcji rysunek przedstawia dwa zbiory AST obok siebie: pełne AST po lewej stronie i AST z odniesieniami po prawej stronie. Najpierw omówimy lewą stronę rysunku, a następnie wyjaśnię zbiory AST z odniesieniami.

https://chacker.pl/

Zacznijmy od dokładniejszego omówienia głównych funkcji Tritona. Triton to darmowa, otwartoźródłowa biblioteka do analizy plików binarnych, znana przede wszystkim ze swojego silnika wykonywania symboli. Oferuje interfejsy API dla języków C/C++ i Python, a obecnie obsługuje zestawy instrukcji x86 i x64. Tritona można pobrać i znaleźć dokumentację pod adresem https://triton.quarkslab.com. Zainstalowałem Tritona w wersji 0.6 (kompilacja 1364) na maszynie wirtualnej w katalogu ~/triton. Triton, podobnie jak libdft, jest narzędziem eksperymentalnym (obecnie nie ma w pełni dojrzałych silników Symbex na poziomie binarnym). Oznacza to, że mogą wystąpić błędy, które można zgłaszać pod adresem https://github.com/JonathanSalwan/Triton/. Triton wymaga również specjalnego, ręcznie napisanego modułu obsługi dla każdego typu instrukcji, informującego silnik Symbex o wpływie instrukcji na stan symboliczny. W rezultacie możesz napotkać nieprawidłowe wyniki lub błędy, jeśli analizowany program używa instrukcji nieobsługiwanych przez Tritona. Użyję Tritona do praktycznych przykładów symbexów, ponieważ jest łatwy w użyciu, stosunkowo dobrze udokumentowany i napisany w C++, co daje mu przewagę wydajnościową nad silnikami napisanymi w językach takich jak Python. Co więcej, tryb concolic Tritona jest oparty na Intel Pin, z którym już jesteś zaznajomiony. Triton obsługuje dwa tryby: tryb emulacji symboli i tryb wykonywania concolic, które odpowiadają statycznej (SSE) i dynamicznej (DSE) filozofii symbexów. W obu trybach Triton pozwala na konkretyzację części stanu w celu zmniejszenia złożoności wyrażeń symbolicznych. Przypomnijmy, że SSE tak naprawdę nie uruchamia programu, ale go emuluje, podczas gdy wykonywanie concolic uruchamia program i śledzi stan symboliczny jako metadane. W rezultacie tryb emulacji symbolicznej jest wolniejszy niż tryb konkoliczny, ponieważ musi emulować wpływ każdej instrukcji zarówno na stan symboliczny, jak i konkretny, podczas gdy tryb konkoliczny uzyskuje stan konkretny „za darmo”. Tryb wykonywania konkolicznego opiera się na Intel Pin i musi uruchamiać analizowany program od samego początku. Natomiast w emulacji symbolicznej można łatwo emulować tylko część programu, na przykład pojedynczą funkcję, a nie cały program. Tu przedstawiono praktyczne przykłady zarówno trybu emulacji symbolicznej, jak i trybu konkolicznego. Triton to przede wszystkim silnik symbex offline, w tym sensie, że eksploruje tylko jedną ścieżkę na raz. Posiada jednak również mechanizm migawek, który pozwala na konkoliczne eksplorowanie wielu ścieżek bez konieczności ponownego rozpoczynania pracy za każdym razem. Ponadto zawiera on silnik analizy skażeń o dużej ziarnistości z jednym kolorem. Chociaż w tym rozdziale te funkcje nie będą Ci potrzebne, możesz dowiedzieć się o nich więcej z dokumentacji online i przykładów Tritona. Nowsze wersje Tritona pozwalają również na podłączenie innej platformy instrumentacji binarnej zamiast Pin i innego, wybranego przez Ciebie solvera ograniczeń. Po prostu użyję ustawień domyślnych, czyli Pin i Z3.

https://chacker.pl/

Zapoznałeś się z zasadami wykonywania symbolicznego. Teraz zbudujmy prawdziwe narzędzia Symbex za pomocą Tritona, popularnego silnika wykonywania symbolicznego o otwartym kodzie źródłowym. Ten rozdział pokazuje, jak zbudować narzędzie do cięcia wstecznego, zwiększyć pokrycie kodu i automatycznie wykorzystać lukę w zabezpieczeniach za pomocą Tritona. Istnieje kilka silników wykonywania symbolicznego, a tylko nieliczne z nich mogą działać na programach binarnych. Najbardziej znane silniki Symbex na poziomie binarnym to Triton, angr,1 i S2E.2 KLEE to kolejny dobrze znany silnik Symbex, który działa na kodzie bitowym LLVM zamiast na kodzie binarnym. Wykorzystam Tritona, ponieważ łatwo integruje się z Intel Pin i jest nieco szybszy dzięki swojemu backendowi C++. Inne znane silniki Symbex to KLEE i S2E, które działają na kodzie bitowym LLVM zamiast na kodzie binarnym.

https://chacker.pl/

Rozwiążmy nieprzejrzysty predykat za pomocą Z3, aby zobaczyć, jak w praktyce wykorzystać operacje na wektorach bitowych. Przejrzyste predykaty to warunki rozgałęzienia, które zawsze zwracają wartość prawda lub fałsz, co nie jest oczywiste dla inżyniera wstecznego. Są one używane jako zaciemnianie kodu, aby utrudnić inżynierowi wstecznemu zrozumienie kodu, na przykład poprzez wstawianie martwego kodu, który w praktyce nigdy nie jest osiągany. W niektórych przypadkach można użyć solvera ograniczeń, takiego jak Z3, aby udowodnić, że rozgałęzienie jest nieprzejrzyście prawdziwe lub fałszywe. Rozważmy na przykład nieprzejrzyście fałszywe rozgałęzienie, które wykorzystuje fakt, że ∀x ∈ Z,2 | (x + x2). Innymi słowy, dla dowolnej liczby całkowitej x, wynikiem x + x2 jest zero modulo dwa. Można tego użyć do skonstruowania rozgałęzienia if((x + x*x) % 2 != 0), które nigdy nie zostanie podjęte, niezależnie od wartości x, co nie jest od razu oczywiste. Następnie możesz wstawić mylący, fałszywy kod w „zajętą” ścieżkę gałęzi, aby wprowadzić w błąd inżynierów wstecznych. Listing  pokazuje, jak zamodelować tę gałąź w Z3 i udowodnić, że nigdy nie można jej zająć.

Listing : Rozwiązywanie nieprzejrzystego predykatu w Z3

Najpierw deklarujesz 64-bitowy wektor bitowy o nazwie x (1), który ma być używany w warunku rozgałęzienia. Następnie potwierdzasz sam warunek rozgałęzienia (2), a na koniec sprawdzasz jego spełnialność za pomocą polecenia check-sat (3). Ponieważ polecenie check-sat zwraca wartość unsat, wiesz, że warunek rozgałęzienia nigdy nie może być prawdziwy, więc możesz bezpiecznie zignorować kod wewnątrz rozgałęzienia podczas inżynierii wstecznej. Jak widać, ręczne modelowanie i dowodzenie nawet tak prostego, nieprzejrzystego predykatu jest żmudne. Jednak dzięki wykonaniu symbolicznemu można automatycznie rozwiązywać tego typu problemy.

Podsumowanie

Poznałeś zasady wykonywania symbolicznego i rozwiązywania ograniczeń. Wykonywanie symboliczne to potężna, ale nieskalowalna technika, którą należy stosować ostrożnie. Z tego powodu istnieje kilka sposobów optymalizacji narzędzi Symbex, z których większość opiera się na minimalizacji ilości analizowanego kodu i obciążenia modułu rozwiązywania ograniczeń. W rozdziale 13 dowiesz się, jak używać Symbex w praktyce, tworząc praktyczne narzędzia Symbex za pomocą Tritona.

https://chacker.pl/

Do tej pory wszystkie przykłady wykorzystywały typ danych Int o dowolnej precyzji z Z3. Jeśli użyjesz typów danych o dowolnej precyzji do modelowania pliku binarnego, wynik może nie odzwierciedlać rzeczywistości, ponieważ pliki binarne operują na liczbach całkowitych o stałej szerokości, które oferują jedynie ograniczoną precyzję. Dlatego Z3 oferuje również wektory bitowe, które są liczbami całkowitymi o stałej szerokości, idealnie nadającymi się do użycia w obliczeniach symbolicznych. Do manipulowania wektorami bitowymi używa się dedykowanych operatorów, takich jak bvadd, bvsub i bvmul, zamiast zwykłych operatorów liczb całkowitych, takich jak +, − i ×. Tabela 1 przedstawia przegląd najczęściej używanych operatorów wektorów bitowych. Zobaczysz ich wiele, jeśli przyjrzysz się ograniczeniom i wyrażeniom symbolicznym, które silniki Symbex, takie jak Triton, przekazują do solvera ograniczeń. Co więcej, znajomość tych operatorów przydaje się podczas tworzenia własnych narzędzi symbex. Omówmy, jak w praktyce używać operatorów wymienionych w tabeli 1. Z3 pozwala na tworzenie wektorów bitowych o dowolnej szerokości bitowej. Istnieje kilka sposobów, aby to osiągnąć, jak widać w pierwszej części tabeli 1 (1). Po pierwsze, można utworzyć 4-bitową stałą wektora bitowego zawierającą bity 1101, używając notacji #b1101. Podobnie, notacja #xda tworzy 8-bitowy wektor bitowy zawierający wartość 0xda. Jak widać, w przypadku stałych binarnych lub szesnastkowych Z3 automatycznie wnioskuje o minimalnym rozmiarze, jaki musi mieć wektor bitowy. Aby zadeklarować stałe dziesiętne, należy jawnie określić zarówno wartość wektora bitowego, jak i jego szerokość. Na przykład notacja (_ bv10 32) tworzy 32-bitowy wektor bitowy zawierający wartość 10. Można również deklarować stałe wektory bitowe o nieokreślonej wartości, używając notacji (declare-const x (_ BitVec 32)), gdzie x jest nazwą stałej, a 32 jest jej szerokością bitową.

Z3 obsługuje również arytmetyczne operatory wektorów bitowych, aby odzwierciedlać wszystkie operacje prymitywne obsługiwane w językach takich jak C/C++ i zestawach instrukcji takich jak x86 (2). Na przykład polecenie Z3 (assert (= y (bvadd x #x10))) potwierdza, że ​​wektor bitowy y musi być równy wektorowi bitowemu x + 0x10. Dla wielu operacji Z3 obejmuje zarówno warianty ze znakiem, jak i bez znaku. Na przykład, (bvsdiv x y) wykonuje dzielenie ze znakiem x/y, podczas gdy (bvudiv x y) wykonuje dzielenie bez znaku. Należy również zauważyć, że Z3 wymaga, aby oba operandy w arytmetycznej operacji wektorowej miały tę samą szerokość bitową. W kolumnie „Przykład” w Tabeli 12-1 wymieniłem przykłady wszystkich typowych operacji wektorowych bitowych Z3. Średniki oznaczają komentarze pokazujące odpowiednik w C/C++ lub wynik arytmetyczny operacji Z3. Oprócz operatorów arytmetycznych, Z3 implementuje również popularne operatory bitowe, takie jak OR (odpowiednik | z języka C), AND (&), XOR (ˆ) i NOT (~) (3). Implementuje również porównania, takie jak = do sprawdzania równości między wektorami bitowymi, bvult do wykonywania porównania „mniejszego niż” bez znaku itd. (4). Obsługiwane porównania są bardzo podobne do tych obsługiwanych przez skoki warunkowe x86 i są szczególnie przydatne w połączeniu z operatorem ite z Z3. Na przykład, (ite (bvsge x y) 22 44) zwraca 22, jeśli x >= y, lub 44 w przeciwnym razie. Można również łączyć dwa wektory bitowe lub wyodrębniać ich część (5). Jest to przydatne, gdy trzeba wyrównać rozmiar dwóch wektorów bitowych, aby umożliwić wykonanie określonej operacji lub gdy interesuje nas tylko część wektora bitowego. Teraz, gdy znasz już operatory bitowe Z3, przyjrzyjmy się praktycznemu przykładowi wykorzystującemu te operatory.

https://chacker.pl/

Z3 może również upraszczać wyrażenia, jak pokazano na Listingu.

Listing: Upraszczanie formuły za pomocą Z3

W tym przykładzie deklarowane są dwie liczby całkowite o nazwach x i y (1), a następnie wywoływane jest polecenie „uprość” w Z3, aby uprościć formułę: 3x + 2y + 5 + x + y (2). Z3 upraszcza ją do 5 + 4x + 3y. Należy zauważyć, że w tym przykładzie wykorzystałem możliwość Z3 do przyjęcia więcej niż dwóch operandów dla operatora „+” i dodania ich wszystkich w jednym kroku. W prostych przykładach, takich jak ten, polecenie „uprość” w Z3 działa dobrze, ale może nie działać tak dobrze w bardziej złożonych przypadkach. Uproszczenie w Z3 ma na celu przede wszystkim usprawnienie programów, takich jak silniki Symbex, które automatycznie przetwarzają formuły, a nie poprawę czytelności dla użytkownika.