Hacking for all!

https://chacker.pl/

Na koniec musisz wiedzieć, które ścieżki programu są badane przez analizę symboliczną. Klasyczne wykonywanie symboliczne bada wszystkie ścieżki programu, tworząc nowy stan symboliczny w każdej gałęzi. To podejście nie jest skalowalne, ponieważ liczba możliwych ścieżek rośnie wykładniczo wraz z liczbą gałęzi w programie; jest to dobrze znany problem eksplozji ścieżek. W rzeczywistości liczba ścieżek może być nieskończona, jeśli występują nieograniczone pętle lub wywołania rekurencyjne. W przypadku programów nietrywialnych potrzebne jest inne podejście, aby wykonywanie symboliczne było bardziej praktyczne. Alternatywnym podejściem dla SSE jest użycie heurystyki do decydowania, które ścieżki badać. Na przykład, w narzędziu do automatycznego wykrywania błędów, możesz skupić się na analizie pętli indeksujących tablice, ponieważ stosunkowo często zawierają one błędy, takie jak przepełnienia bufora. Inną powszechną heurystyką jest przeszukiwanie w głąb (DFS), które bada jedną kompletną ścieżkę programu przed przejściem do kolejnej ścieżki, przy założeniu, że głęboko zagnieżdżony kod jest prawdopodobnie bardziej „interesujący” niż kod powierzchowny. Przeszukiwanie wszerz (BFS) działa odwrotnie, badając wszystkie ścieżki równolegle, ale zajmuje więcej czasu, aby dotrzeć do głęboko zagnieżdżonego kodu. Wybór heurystyki zależy od celu narzędzia Symbex, a znalezienie odpowiedniej heurystyki może stanowić poważne wyzwanie. Wykonywanie Concolic bada tylko jedną ścieżkę na raz, w oparciu o konkretne dane wejściowe. Można je jednak również połączyć z podejściem heurystycznej eksploracji ścieżek, a nawet z podejściem eksploracji wszystkich ścieżek. W przypadku wykonywania Concolic najłatwiejszym sposobem eksploracji wielu ścieżek jest wielokrotne uruchamianie aplikacji, za każdym razem z nowymi danymi wejściowymi odkrytymi poprzez „odwrócenie” ograniczeń gałęzi w poprzednim przebiegu. Bardziej wyrafinowanym podejściem jest tworzenie migawek stanu programu, tak aby po zakończeniu eksploracji jednej ścieżki można było przywrócić migawkę do wcześniejszego punktu wykonania i stamtąd eksplorować inną ścieżkę. Podsumowując, wykonywanie symboliczne ma wiele parametrów, które można modyfikować, aby zrównoważyć wydajność i ograniczenia analizy. Optymalna konfiguracja będzie zależeć od celów, a różne silniki Symbex dokonują różnych wyborów konfiguracyjnych. Na przykład Triton ( i angr1 to silniki Symbex na poziomie binarnym, które obsługują SSE na poziomie aplikacji i wykonywanie concolic. S2E2 również działa na plikach binarnych, ale wykorzystuje podejście oparte na maszynie wirtualnej w całym systemie, które może stosować Symbex nie tylko do aplikacji, ale także do jądra, bibliotek i sterowników działających na maszynie wirtualnej. Natomiast KLEE3 wykonuje klasyczne SSE online na kodzie bitowym LLVM, a nie bezpośrednio na plikach binarnych, obsługując wiele heurystyk wyszukiwania w celu optymalizacji pokrycia ścieżki. Istnieją nawet silniki Symbex wyższego poziomu, które działają bezpośrednio na kodzie C, Java lub Python. Teraz, gdy znasz już działanie różnych technik Symbex, omówmy kilka typowych optymalizacji, których możesz użyć, aby zwiększyć skalowalność swoich narzędzi Symbex.

https://chacker.pl/

Aby uniknąć eksplozji stanu w pełni symbolicznej pamięci, można zastąpić nieograniczone adresy symboliczne adresami konkretnymi. W przypadku wykonywania konkolicznego silnik Symbex może po prostu użyć rzeczywistego adresu konkretnego. W przypadku statycznego wykonywania symbolicznego silnik będzie musiał użyć heurystyki, aby wybrać odpowiedni adres konkretny. Zaletą tego podejścia jest znaczne zmniejszenie przestrzeni stanów i złożoności ograniczeń, ale wadą jest to, że nie uwzględnia ono w pełni wszystkich możliwych zachowań programu, co może spowodować, że silnik Symbex przeoczy niektóre możliwe wyniki.W praktyce wiele silników Symbex wykorzystuje kombinację tych rozwiązań. Na przykład mogą one symbolicznie modelować dostęp do pamięci, jeśli dostęp jest ograniczony do wystarczająco małego zakresu przez ograniczenia, jednocześnie konkretyzując dostępy nieograniczone.

https://chacker.pl/

Rozwiązania oparte na pamięci w pełni symbolicznej próbują modelować wszystkie możliwe wyniki operacji ładowania lub zapisywania danych w pamięci. Jednym ze sposobów osiągnięcia tego celu jest rozwidlenie stanu na wiele kopii, z których każda odzwierciedla każdy możliwy wynik operacji. Na przykład, załóżmy, że odczytujemy tablicę a przy użyciu indeksu symbolicznego φi, z ograniczeniem, że φi < 5. Podejście rozwidlające stan rozwidlałoby stan na pięć kopii: jedną dla sytuacji, gdy φi = 0 (tak, że odczytane jest a[0]), drugą dla φi = 1 itd. Innym sposobem osiągnięcia tego samego efektu jest użycie ograniczeń z wyrażeniami if-then-else obsługiwanymi przez niektóre solvery ograniczeń. Wyrażenia te są analogiczne do warunków if-then-else używanych w językach programowania. W tym podejściu odczyt tej samej tablicy jest modelowany jako ograniczenie warunkowe, które odpowiada symbolicznemu wyrażeniu a[i], jeśli φi = i. Chociaż w pełni symboliczne rozwiązania pamięciowe dokładnie modelują zachowanie programu, to jednak cierpią na eksplozję stanów lub ekstremalnie skomplikowane ograniczenia, jeśli jakikolwiek dostęp do pamięci korzysta z nieograniczonych adresów. Problemy te są bardziej powszechne w symbeksach binarnych niż w symbeksach źródłowych, ponieważ informacje o ograniczeniach nie są łatwo dostępne w plikach binarnych.

https://chacker.pl/

Kolejnym zagadnieniem jest określenie, które części stanu programu są reprezentowane symbolicznie, a które są konkretne, a także ustalenie sposobu obsługi symbolicznego dostępu do pamięci. Wiele silników wykonawczych SSE i Concolic oferuje możliwość pominięcia stanu symbolicznego dla niektórych rejestrów i lokalizacji pamięci. Śledząc informacje symboliczne tylko dla wybranego stanu, zachowując jednocześnie konkretność pozostałej części stanu, można zmniejszyć rozmiar stanu oraz złożoność ograniczeń ścieżki i wyrażeń symbolicznych. To podejście jest bardziej wydajne pod względem pamięci i szybsze, ponieważ ograniczenia są łatwiejsze do rozwiązania. Kompromisem jest konieczność wyboru, który stan uczynić symbolicznym, a który tylko konkretnym, a ta decyzja nie zawsze jest trywialna. Nieprawidłowy wybór może spowodować, że narzędzie Symbex zgłosi nieoczekiwane wyniki. Innym ważnym aspektem sposobu, w jaki silniki Symbex utrzymują stan symboliczny, jest sposób, w jaki reprezentują one dostęp do pamięci symbolicznej. Podobnie jak inne zmienne, wskaźniki mogą być symboliczne, co oznacza, że ​​ich wartość nie jest konkretna, lecz częściowo nieokreślona. Stwarza to trudny problem, gdy ładowanie lub przechowywanie danych w pamięci korzysta z adresu symbolicznego. Na przykład, jeśli wartość jest zapisywana do tablicy za pomocą indeksu symbolicznego, jak należy aktualizować stan symboliczny? Omówmy kilka sposobów podejścia do tego problemu.

https://chacker.pl/

Kolejną ważną kwestią jest to, czy silnik Symbex wykonuje wiele ścieżek równolegle. Silniki Symbex, które równolegle eksplorują wiele ścieżek programu, nazywane są online, podczas gdy silniki eksplorujące tylko jedną ścieżkę na raz nazywane są offline. Na przykład, klasyczne statyczne wykonywanie symboliczne jest online, ponieważ tworzy nową instancję Symbex w każdej gałęzi i eksploruje oba kierunki równolegle. Natomiast wykonywanie concolic jest zazwyczaj offline, eksplorując tylko jedno konkretne wykonanie na raz. Istnieją jednak implementacje SSE offline i concolic online. Zaletą online Symbex jest to, że nie wymaga wielokrotnego wykonywania tej samej instrukcji. Implementacje offline często analizują ten sam fragment kodu wielokrotnie, co oznacza konieczność uruchomienia całego programu od początku dla każdej ścieżki programu. W tym sensie implementacje symboliczne online są bardziej wydajne, ale równoległe śledzenie wszystkich tych stanów może pochłaniać dużo pamięci, o co nie trzeba się martwić w przypadku wykonywania symbolicznego offline. Implementacje Symbex online starają się zminimalizować narzut pamięci poprzez scalanie identycznych części stanów programu, dzieląc je tylko wtedy, gdy się rozchodzą. Ta optymalizacja jest znana jako kopiowanie przy zapisie, ponieważ kopiuje scalone stany, gdy zapis powoduje ich rozchodzenie się, tworząc nową prywatną kopię stanu dla ścieżki, która generuje zapis.

https://chacker.pl/

Dynamiczne wykonywanie symboliczne (DSE) uruchamia aplikację z konkretnymi danymi wejściowymi i zachowuje stan symboliczny oprócz stanu konkretnego, zamiast całkowicie go zastępować. Innymi słowy, to podejście wykorzystuje stan konkretny do sterowania wykonywaniem, jednocześnie zachowując  stan symboliczny jako metadane, tak jak silniki analizy skażeń przechowują informacje o skażeniach. Z tego powodu dynamiczne wykonywanie symboliczne jest również znane jako wykonywanie concolic, jak w przypadku „konkretnego wykonywania symbolicznego”. W przeciwieństwie do tradycyjnego statycznego wykonywania symbolicznego, które bada wiele ścieżek programu równolegle, wykonywanie concolic uruchamia tylko jedną ścieżkę naraz, określoną przez konkretne dane wejściowe. Aby badać różne ścieżki, wykonywanie concolic „odwraca” ograniczenia ścieżki, a następnie używa solvera ograniczeń do obliczenia konkretnych danych wejściowych, które prowadzą do gałęzi alternatywnej. Następnie można użyć tych konkretnych danych wejściowych do rozpoczęcia nowego wykonania concolic, które bada ścieżkę alternatywną. Wykonywanie Concolic ma wiele zalet. Jest znacznie bardziej skalowalne, ponieważ nie wymaga utrzymywania wielu równoległych stanów wykonywania. Można również rozwiązać problemy SSE z interakcjami zewnętrznymi, po prostu uruchamiając te interakcje konkretnie. Nie prowadzi to do problemów ze spójnością, ponieważ wykonywanie Concolic nie uruchamia różnych ścieżek równolegle. Ponieważ wykonywanie Concolic symbolizuje tylko „interesujące” części stanu programu, takie jak dane wejściowe użytkownika, obliczane przez nie ograniczenia zazwyczaj obejmują mniej zmiennych niż te obliczane przez klasyczne silniki SSE, co sprawia, że ​​ograniczenia są łatwiejsze i znacznie szybsze do rozwiązania. Główną wadą jest to, że pokrycie kodu uzyskane przez wykonywanie Concolic zależy od początkowych konkretnych danych wejściowych. Ponieważ wykonywanie Concolic „odwraca” jednocześnie tylko niewielką liczbę ograniczeń rozgałęzień, dotarcie do interesujących ścieżek może zająć dużo czasu, jeśli są one oddzielone wieloma odwróceniami od ścieżki początkowej. Mniej trywialne jest również symboliczne wykonywanie tylko części programu, choć można to zaimplementować, dynamicznie włączając lub wyłączając silnik symboliczny w czasie wykonywania.

https://chacker.pl/

Alternatywnie, silnik wykonywania symbolicznego może bezpośrednio wykonywać interakcje zewnętrzne. Na przykład, zamiast modelować efekty wywołania systemowego, silnik Symbex może faktycznie wykonać wywołanie systemowe i włączyć konkretną wartość zwracaną oraz efekty uboczne do stanu symbolicznego. Chociaż to podejście jest proste, prowadzi do problemów, gdy wiele ścieżek, które wykonują konkurujące ze sobą interakcje zewnętrzne, jest badanych równolegle. Przykładowo, jeśli wiele ścieżek działa równolegle na tym samym pliku fizycznym, może to prowadzić do problemów ze spójnością, jeśli zmiany będą ze sobą kolidować. Można to obejść, klonując pełny stan systemu dla każdej badanej ścieżki, ale takie rozwiązanie jest niezwykle pamięciochłonne. Co więcej, ponieważ zewnętrzne komponenty oprogramowania nie są w stanie obsłużyć stanu symbolicznego, bezpośrednia interakcja ze środowiskiem oznacza kosztowne wywołanie solvera ograniczeń w celu obliczenia odpowiednich wartości konkretnych, które można przekazać do wywołania systemowego lub bibliotecznego.Ze względu na trudności związane ze statycznym wykonywaniem symbolicznym, nowsze badania skupiają się na alternatywnych implementacjach symbexu w oparciu o analizę dynamiczną.

https://chacker.pl/

Powszechnym podejściem jest modelowanie przez silnik SSE efektów interakcji zewnętrznych, takich jak wywołania systemowe i biblioteczne. Modele te stanowią swego rodzaju „podsumowanie” efektów, jakie wywołanie systemowe lub biblioteczne wywiera na stan symboliczny. (Należy pamiętać, że słowo „model” w tym znaczeniu nie ma nic wspólnego z modelami zwracanymi przez solver ograniczeń).Pod względem wydajności modelowanie efektów jest stosunkowo tanim rozwiązaniem. Jednak stworzenie dokładnych modeli dla wszystkich możliwych interakcji ze środowiskiem – w tym z siecią, systemem plików i innymi procesami – jest monumentalnym zadaniem, które może wymagać stworzenia symulowanego symbolicznego systemu plików, symbolicznego stosu sieciowego itd. Co gorsza, modele muszą zostać przepisane, jeśli chcemy symulować inny system operacyjny lub jądro. Dlatego w praktyce modele są często niekompletne lub niedokładne.

https://chacker.pl/

Podobnie jak większość technik analizy oprogramowania i plików binarnych, wykonywanie symboliczne występuje w wariantach statycznych i dynamicznych, charakteryzujących się różnymi kompromisami w zakresie skalowalności i kompletności. Tradycyjnie wykonywanie symboliczne to technika analizy statycznej, która emuluje część programu, propagując stan symboliczny z każdą emulowaną instrukcją. Ten typ wykonywania symbolicznego jest również znany jako statyczne wykonywanie symboliczne (SSE). Analizuje ono wyczerpująco wszystkie możliwe ścieżki lubwykorzystuje heurystykę, aby zdecydować, które ścieżki należy wybrać. Zaletą SSE jest to, że umożliwia analizowanie programów, które nie mogą zostać uruchomione na danym procesorze. Na przykład można analizować pliki binarne ARM na komputerze x86. Kolejną zaletą jest to, że łatwo jest emulować tylko część pliku binarnego (na przykład tylko jedną funkcję) zamiast całego programu. Wadą jest to, że eksploracja obu kierunków w każdej gałęzi nie zawsze jest możliwa ze względu na problemy ze skalowalnością. Chociaż można użyć heurystyki, aby ograniczyć liczbę eksplorowanych gałęzi, opracowanie skutecznej heurystyki, która wychwyci wszystkie interesujące ścieżki, nie jest łatwe. Co więcej, niektóre elementy działania aplikacji są trudne do poprawnego modelowania za pomocą SSE, szczególnie gdy sterowanie przepływa poza aplikację do komponentów oprogramowania, nad którymi nie ma kontroli silnik wykonywania symbolicznego, takich jak jądro lub biblioteka. Dzieje się tak, gdy program wydaje wywołanie systemowe lub biblioteczne, odbiera sygnał, próbuje odczytać zmienną środowiskową itd. Aby obejść ten problem, można zastosować poniższe rozwiązania, choć każde z nich ma swoje wady.

https://chacker.pl/

Czy implementacja Symbex opiera się na analizie statycznej, czy dynamicznej?

Online a offline

Czy silnik Symbex bada wiele ścieżek równolegle (online), czy nie (offline)?

Stan symboliczny

Które części stanu programu są reprezentowane symbolicznie, a które są konkretne? Jak obsługiwany jest symboliczny dostęp do pamięci?

Pokrycie ścieżki

Które (i ile) ścieżek programu bada analiza symboliczna?

Omówmy każdą z tych decyzji projektowych i ich konsekwencje w zakresie wydajności, ograniczeń i kompletności.