Wyrażenie symboliczne φj, gdzie j ∈ N, odpowiada albo wartości symbolicznej αi, albo pewnej matematycznej kombinacji wyrażeń symbolicznych, takiej jak φ3 = φ1 + φ2. σ będę używać do oznaczenia magazynu wyrażeń symbolicznych, który jest zbiorem wszystkich wyrażeń symbolicznych użytych w wykonaniu symbolicznym. Jak wspomniałem, binarny system symboliczny (symbex) odwzorowuje wszystkie lub niektóre rejestry i lokalizacje pamięci na wyrażenie w σ.
Wykonanie symboliczne działa na wartościach symbolicznych, które reprezentują dowolną możliwą wartość konkretną. Wartości symboliczne będę oznaczać jako αi, gdzie i jest liczbą całkowitą (i ∈ N). Silnik Symbex oblicza dwa różne rodzaje formuł na podstawie tych wartości symbolicznych: zbiór wyrażeń symbolicznych i ograniczenie ścieżki. Ponadto utrzymuje mapowanie zmiennych (lub w przypadku binarnego Symbex, rejestrów i lokalizacji pamięci) na wyrażenia symboliczne. Połączenie ograniczenia ścieżki i wszystkich wyrażeń symbolicznych oraz mapowań nazywam stanem symbolicznym.
Symbex wykonuje (lub emuluje) aplikację z wartościami symbolicznymi, a nie z wartościami konkretnymi używanymi podczas normalnego uruchamiania programu. Oznacza to, że zmienne nie zawierają konkretnych wartości, takich jak 42 czy foobar, jak miałoby to miejsce podczas normalnego wykonywania. Zamiast tego, niektóre lub wszystkie zmienne (lub w kontekście analizy binarnej, rejestry lub komórki pamięci) są reprezentowane przez symbol, który zastępuje dowolną możliwą wartość, jaką zmienna może przyjąć. W trakcie wykonywania, wykonywanie symboliczne oblicza formuły logiczne dla tych symboli. Formuły te reprezentują operacje wykonywane na symbolach podczas wykonywania i opisują granice zakresu wartości, które symbole mogą reprezentować. Jak wyjaśnię, wiele silników Symbex przechowuje symbole i formuły jako metadane oprócz wartości konkretnych, zamiast je zastępować, podobnie jak analiza skażeń śledzi metadane skażeń. Zbiór wartości symbolicznych i formuł przechowywanych przez silnik Symbex nazywa się stanem symbolicznym. Przyjrzyjmy się, jak zorganizowany jest stan symboliczny, a następnie przeanalizujmy konkretny przykład ewolucji stanu w wykonaniu symbolicznym.
Wykonywanie symboliczne, w skrócie symbex, to technika analizy oprogramowania, która wyraża stan programu za pomocą formuł logicznych, na podstawie których można automatycznie wnioskować, aby odpowiedzieć na złożone pytania dotyczące zachowania programu. Na przykład NASA używa wykonywania symbolicznego do generowania przypadków testowych dla kodu o znaczeniu krytycznym, a producenci sprzętu do testowania kodu napisanego w językach opisu sprzętu, takich jak Verilog i VHDL. Wykonywania symbolicznego można również używać do automatycznego zwiększania pokrycia kodu analiz dynamicznych poprzez generowanie nowych danych wejściowych, które prowadzą do niezbadanych ścieżek programu, co jest przydatne w testowaniu oprogramowania i analizie złośliwego oprogramowania. W rozdziale 13 przedstawiono praktyczne przykłady wykorzystania symbex do implementacji pokrycia kodu, implementacji podziału wstecznego, a nawet automatycznego generowania exploitów na luki w zabezpieczeniach! Niestety, chociaż wykonywanie symboliczne jest potężną techniką, należy ją stosować oszczędnie i ostrożnie ze względu na problemy ze skalowalnością. Na przykład, w zależności od rodzaju rozwiązywanego problemu z wykonaniem symbolicznym, złożoność może rosnąć wykładniczo do punktu, w którym obliczeniowe rozwiązanie stanie się całkowicie niewykonalne. Dowiesz się, jak zminimalizować te problemy ze skalowalnością , ale najpierw przyjrzyjmy się podstawom działania wykonania symbolicznego.
Wykonywanie symboliczne śledzi metadane dotyczące stanu programu, podobnie jak analiza skażeń. Jednak w przeciwieństwie do informacji o skażeniach, które pozwalają jedynie wnioskować, że część stanu programu wpływa na inną, wykonywanie symboliczne pozwala wnioskować o tym, jak powstał stan programu i jak osiągnąć różne stany programu. Jak zobaczysz, wykonywanie symboliczne umożliwia wiele zaawansowanych analiz niemożliwych do przeprowadzenia innymi technikami. Rozpocznę ten rozdział od omówienia podstaw wykonywania symbolicznego. Następnie dowiesz się więcej o rozwiązywaniu ograniczeń (w szczególności rozwiązywaniu SMT), które jest fundamentalnym elementem wykonywania symbolicznego. W rozdziale 13 wykorzystasz Triton, bibliotekę wykonywania symbolicznego na poziomie binarnym, do tworzenia praktycznych narzędzi demonstrujących możliwości wykonywania symbolicznego.
Poznałeś/aś wewnętrzną strukturę libdft, popularnej biblioteki open source do analizy danych (DTA). Poznałeś/aś również praktyczne przykłady wykorzystania libdft do wykrywania dwóch typowych ataków: przejęcia kontroli (control hijacking) i eksfiltracji danych. Powinieneś/powinnaś być teraz gotowy/gotowa do tworzenia własnych narzędzi DTA!
Ćwiczenie
Wskazówka: Nie można bezpośrednio podłączyć printf do biblioteki libdft, ponieważ nie jest to wywołanie systemowe. Zamiast tego musisz znaleźć inny sposób, na przykład z hookiem na poziomie instrukcji (ins_set_pre biblioteki libdft), który sprawdza wywołania stykowego modułu PLT printf. Na potrzeby tego ćwiczenia możesz przyjąć założenia upraszczające, takie jak brak pośrednich wywołań printf i stały, zakodowany na stałe adres dla stykowego modułu PLT. Jeśli szukasz praktycznego przykładu podłączania na poziomie instrukcji, sprawdź narzędzie libdft-dta.c dołączone do biblioteki libdft!
Aby zademonstrować zdolność dta-dataleak do wykrywania wycieków danych, zaimplementowałem kolejny prosty serwer o nazwie dataleak-test-xor. Dla uproszczenia, ten serwer dobrowolnie „przecieka” zanieczyszczone pliki do gniazda, ale dta-dataleak może w ten sam sposób wykrywać pliki wyciekające przez exploit. Listing przedstawia odpowiedni kod dla serwera.
Listing : dataleak-test-xor.c
Serwer otwiera gniazdo na porcie localhost 9999 (1) i używa go do odebrania wiadomości (2) zawierającej listę nazw plików. Dzieli tę listę na pojedyncze nazwy plików za pomocą funkcji o nazwie split_filenames, która jest pominięta w zestawieniu (3). Następnie otwiera wszystkie żądane pliki (4) i wybiera losowo dwa z otwartych plików (5). Należy zauważyć, że w realistycznym przypadku użycia dta-dataleak, dostęp do plików byłby uzyskiwany za pomocą exploita, a nie udostępniany dobrowolnie przez serwer. Na potrzeby tego przykładu serwer odczytuje zawartość dwóch losowo wybranych plików wiersz po wierszu (6), łącząc każdą parę wierszy (po jednym wierszu z każdego pliku) za pomocą operacji XOR (7). Połączenie wierszy spowoduje, że dta-dataleak połączy ich kolory skażeń, demonstrując łączenie skażeń na potrzeby tego przykładu. Na koniec, wynik dwóch linii XOR jest przesyłany przez sieć (8), zapewniając „wyciek danych” do wykrycia przez dta-dataleak. Teraz zobaczmy, jak dta-dataleak wykrywa próbę wycieku danych, a konkretnie, jak kolory skażeń są łączone, gdy wyciekające dane zależą od wielu plików. Listing przedstawia wynik uruchomienia programu dataleak-test-xor z zabezpieczeniem dta-dataleak. Powtarzające się fragmenty wyniku zostały skrócone za pomocą „…”.
Listing : Wykrywanie próby eksfiltracji danych za pomocą dta-dataleak
W tym przykładzie serwer dataleak-test-xor jest uruchamiany z funkcją Pin, używając dta-dataleak jako narzędzia Pin w celu ochrony przed wyciekami danych (1). Natychmiast następuje pierwsze wywołanie systemowe odczytu związane z procesem ładowania dataleak-test-xor (2). Ponieważ te bajty są odczytywane z biblioteki współdzielonej, która nie ma przypisanego koloru skażenia, dta-dataleak ignoruje odczyt. Następnie przykład uruchamia sesję netcat, aby połączyć się z serwerem (3) i wysłać mu listę nazw plików do otwarcia (4). Narzędzie dta-dataleak przechwytuje zdarzenia otwarcia dla wszystkich tych plików i przypisuje każdemu z nich kolor skażenia (5). Następnie serwer losowo wybiera dwa pliki, które mają zostać ujawnione. W tym przypadku okazują się to pliki z deskryptorem pliku 8 (6) i 5 (7). W przypadku obu plików, dta-dataleak przechwytuje zdarzenia odczytu i zanieczyszcza odczytane bajty powiązanymi z nimi kolorami zanieczyszczania (odpowiednio 0x08 i 0x01). Następnie dta-dataleak przechwytuje próbę wysłania przez serwer zawartości pliku, która jest teraz łączona za pomocą operacji XOR, przez sieć (8). Sprawdza zanieczyszczanie bajtów, które serwer ma zamiar wysłać (9), zauważa, że są one zanieczyszczone tagiem 0x09 (10), a następnie wyświetla alert i przerywa działanie programu. Tag 0x09 to kombinacja dwóch kolorów zanieczyszczania: 0x01 i 0x08. Z alertu wynika, że kolory te odpowiadają odpowiednio plikom dta-execve.cpp i echo.c. Jak widać, analiza zanieczyszczania ułatwia wykrywanie wycieków informacji i dokładne określenie, które pliki zostały zanieczyszczone. Można również użyć scalonych kolorów zanieczyszczania, aby określić, które źródła zanieczyszczania przyczyniły się do wartości bajtu. Nawet przy użyciu zaledwie ośmiu kolorów skaz istnieją nieskończone możliwości tworzenia potężnych narzędzi DTA!
Na koniec, Listing przedstawia odbiornik skażeń programu dta-dataleak, czyli procedurę obsługi wywołań gniazd, która przechwytuje przesyły sieciowe w celu sprawdzenia ich pod kątem prób eksfiltracji danych. Jest ona podobna do procedury obsługi wywołań gniazd, którą widziałeś w narzędziu dta-execve, z tą różnicą, że sprawdza wysłane bajty pod kątem skażenia zamiast stosować skażenie do odebranych bajtów.
Listing : dta-dataleak.cpp (ciąg dalszy)
Najpierw funkcja pre_socketcall_hook pobiera parametry call (1) i args (2) dla funkcji socketcall. Następnie używa przełącznika w wywołaniu, takiego jak ten, który widziałeś w procedurze obsługi socketcall dla dta-execve, z tą różnicą, że ten nowy przełącznik sprawdza SYS_SEND i SYS_SENDTO (3) zamiast SYS_RECV i SYS_RECVFROM. Jeśli przechwyci zdarzenie send, analizuje argumenty send: deskryptor pliku socket, bufor send i liczbę bajtów do wysłania (4). Po wydrukowaniu kilku danych diagnostycznych kod przechodzi przez wszystkie bajty w buforze send (5) i pobiera status zanieczyszczenia każdego bajtu za pomocą funkcji tagmap_getb (6). Jeśli bajt jest zanieczyszczony, funkcja pre_socketcall_hook wywołuje funkcję alert, aby wyświetlić alert i zatrzymać aplikację (7). To obejmuje cały kod narzędzia dta-dataleak. W następnej sekcji pokażemy, w jaki sposób dta-dataleak wykrywa próbę eksfiltracji danych i w jaki sposób kolory skażeń łączą się, gdy eksfiltracja danych zależy od wielu źródeł skażenia.
Teraz, gdy każdy otwarty plik jest powiązany z kolorem zanieczyszczającym, przyjrzyjmy się funkcji post_read_hook, która zanieczyszcza odczytane z pliku bajty przypisanym do niego kolorem. Listing przedstawia odpowiedni kod.
Listing : dta-dataleak.cpp (ciąg dalszy)
Najpierw funkcja post_read_hook analizuje odpowiednie argumenty i wartość zwracaną z kontekstu wywołania systemowego, aby uzyskać deskryptor pliku, który jest odczytywany (fd) (1), bufor, do którego odczytywane są bajty (buf) (2) oraz liczbę odczytanych bajtów (len) (3). Jeśli len jest mniejsze lub równe zero, żadne bajty nie zostały odczytane, więc funkcja post_read_hook zwraca wynik bez zanieczyszczania czegokolwiek (4). W przeciwnym razie uzyskuje kolor zanieczyszczania fd, odczytując go z fd2color (5). Jeśli fd ma skojarzony kolor zanieczyszczania (6), funkcja post_read_hook używa funkcji tagmap_setn do zanieczyszczania wszystkich odczytanych bajtów tym kolorem (7). Może się również zdarzyć, że fd nie ma skojarzonego koloru (8), co oznacza, że odnosi się do nieinteresującego pliku, takiego jak biblioteka współdzielona. W takim przypadku usuwamy wszelkie zanieczyszczania z adresów nadpisanych przez wywołanie systemowe odczytu (9) za pomocą funkcji tagmap_clrn biblioteki libdft. Usuwa to skażenie z każdego wcześniej zanieczyszczonego bufora, który jest ponownie wykorzystywany do odczytu nieskażonych bajtów.
Listing przedstawia kod dla post_open_hook, procedury obsługi wywołania systemowego open.
Listing : dta-dataleak.cpp (ciąg dalszy)
Przypomnijmy, że celem dta-dataleak jest wykrywanie prób wycieku informacji, które powodują wyciek danych odczytanych z pliku. Aby dta-dataleak mógł określić, który plik jest przedmiotem wycieku, przypisuje on inny kolor każdemu otwartemu plikowi. Celem procedury obsługi otwartego wywołania systemowego, post_open_hook, jest przypisanie koloru skażenia do każdego deskryptora pliku podczas jego otwierania. Filtruje ona również niektóre nieistotne pliki, takie jak biblioteki współdzielone. W rzeczywistym narzędziu DTA prawdopodobnie będziesz chciał zaimplementować więcej filtrów, aby kontrolować, które pliki chronić przed wyciekami informacji. Aby śledzić kolejny dostępny kolor skażenia, post_open_hook używa zmiennej statycznej o nazwie next_color, która jest inicjowana kolorem 0x01 (1). Następnie analizuje kontekst wywołania systemowego (ctx) otwartego wywołania systemowego, które właśnie wystąpiło, aby uzyskać deskryptor pliku fd (2) i nazwę pliku fname (3) właśnie otwartego pliku. Jeśli otwarcie się nie powiedzie (4) lub otwarty plik jest biblioteką współdzieloną, której śledzenie nie jest interesujące (5), post_open_hook zwraca wynik bez przypisywania pliku koloru. Aby ustalić, czy plik jest biblioteką współdzieloną, post_open_hook po prostu sprawdza, czy nazwa pliku zawiera rozszerzenie wskazujące na bibliotekę współdzieloną, takie jak .so. W prawdziwym narzędziu należy zastosować bardziej rygorystyczne kontrole, otwierając podejrzaną bibliotekę współdzieloną i weryfikując, czy zaczyna się ona na przykład od magicznych bajtów ELF (patrz również rozdział 2). Jeśli plik jest na tyle interesujący, aby przypisać mu kolor tainta, post_open_hook rozróżnia dwa przypadki:
Na końcu post_open_hook mapa color2fname jest aktualizowana o nazwę pliku, który został właśnie otwarty (9). W ten sposób, w przypadku wycieku danych, można użyć koloru skażenia wyciekłych danych, aby wyszukać nazwę odpowiadającego pliku, tak jak przed chwilą widzieliśmy w funkcji alert. Jeśli kolor skażenia został ponownie użyty dla wielu plików z jednego z tych powodów, wpis color2fname dla tego koloru będzie listą nazw plików rozdzielonych pionową kreską (|) (10).