Mozilla rr – GDB na “sterydach”?

Ten wpis jest częścią cyklu “Od zera do bughuntera” – listę wszystkich postów znajdziesz tutaj.

Zdarzają się takie dni, kiedy mało co wychodzi, nawet znalezione błędy w oprogramowaniu. Nie zamierzam bawić się w cybercoacha (jak termin się spopularyzuje to znacie mojego maila 😉 ) i pomagać ludziom w kwestiach zmiany myślenia oraz życia ze świadomością istnienia niereprodukowalnych podatności – wolę przedstawić konkretne narzędzia, które pomogą uporać się z tą sytuacją technicznie a nie mentalnie, bo takie rozwiązanie będzie moim zdaniem najlepsze. Martwi mnie świadomość tego, że Mozilla, swoją drogą zasłużenie, jest znana z przeglądarki Firefox – jej zespół bezpieczeństwa dostarcza świetne narzędzia do badania bezpieczeństwa oprogramowania: biblioteka Octo do budowania fuzzerów, fuzzery DOM, fuzzery JS wykorzystywane do testów silnika SpiderMonkey oraz framework do debuggowania rr (Record & Replay). O tym ostatnim w tym poście będzie mowa.

Ale co? Po co? Dlaczego?

Odpowiedź jest bardzo prosta – aby programistom / “bezpiecznikom” żyło się łatwiej. Według moich nieobiektywnych obserwacji niedeterministyczne błędy (trudne do replikacji po stronie “naprawiającej” np. zależne od sytuacji wyścigu lub struktury pamięci) zdarzają się najczęściej wtedy, kiedy całkowicie się ich nie spodziewamy: nowy release, rutynowa poprawka w kodzie lub niestandardowe środowisko wykonania, na którym nie przeprowadzaliśmy testów.

rr na “wysokim poziomie” oparty jest o bardzo prostą koncepcję: zapisanie pełnego przebiegu wykonania do momentu zaistnienia problemu, oczywiście z możliwością odtworzenia i przechodzenia “krok po kroku”. W tym miejscu należy wspomnieć, że rr jest oparte o gdb – działają w nim mechanizmy skryptowania znane z tego, już klasycznego debuggera, wraz z integrację z popularnymi IDE. Narzut wydajnościowy jest zaskakująco niewielki (1.2x) – wynika to z zapisywania tylko stanów w programie, które ze swojej natury są niedeterministyczne, np, pobieranie inputu od użytkownika. Z mojej perspektywy najbardziej interesującą funkcjonalnością jest Chaos Mode, wspierający wyzwalanie problemów z kodem trudnych do powielenia.

Zacznijmy od problemów rr…

Bardzo interesująco to wszystko brzmi, lecz świadomy Czytelnik zdaje sobie sprawę, że musi być jakieś “ale” – i oczywiście będzie miał racje! Z założenia rr działa jednowątkowo, więc niektóre przebiegi będą zapisywane bardzo powoli. Kolejnym wykluczeniem jest poddawanie procesowi debuggowania aplikacji korzystających z mechanizmów współdzielenia pamięci pomiędzy procesami, które nie są procesami potomnymi / rodzicami. To ograniczenie ma duży sens, bo podejrzewam, że zapis bardzo szybko spuchłby do wielkości kilkudziesięciu gigabajtów a “przedarcie” się do interesującego stanu byłoby mocno utrudnione. Niestety dużym minusem jest wysoka niekompatybylność ze środowiskami wirtualnymi: VirtualBox, Hyper-V oraz Xen. Nie wspierają one wirtualizacji PMU (Performance Monitoring Unit), co uniemożliwia działanie rr. WSL (Windows Subsystem for Linux) również nie jest dobrym rozwiązaniem, za to wirtualizatory od VMware, QEMU oraz KVM zadziałają bez problemu.

Ukrytym problemem rr jest to, że zapis wykonania jest deterministyczny – każde uruchomienie to te same adresy pamięci, jej struktura oraz zawartość rejestrów. Jest to oczywiste, lecz wiele osób o tym zapomina.

Nie jest niczym rzadkim sytuacja zamieszczona na obrazku powyżej 😉

“Jedziemy” z crashami!

Instalacja jest prosta, odpowiedni pakiet znajduje się w repozytoriach najpopularniejszych linuksowych dystrybucji – aczkolwiek autorzy zalecają korzystanie z samodzielnej kompilacji kodu z gita.  AFAIK paczki w repozytoriach (poza Debianem 😉 ) są całkiem świeże, więc nic się nie stanie jak pójdziemy po najniższej linii oporu.

Problemem do rozwiązania będzie błąd znaleziony przez moje fuzzery w Z3  i niechętnie poddający się ponownemu wyzwoleniu u deweloperów – u mnie wszystko działa (SOA #1), czego świadectwem jest niżej przedstawiony raport ASAN (skrócony, pełna wersja dostępna w zgłoszeniu błędu):


==8629==ERROR: AddressSanitizer: heap-use-after-free on address 0x60b000010d38 at pc 0x0000032e475b bp 0x7ffc5642b990 sp 0x7ffc5642b988
READ of size 8 at 0x60b000010d38 thread T0
#0 0x32e475a in smt::theory_array_full::instantiate_axiom_map_for(int) z3/build/../src/smt/theory_array_full.cpp:69:28
#1 0x32e475a in smt::theory_array_full::assert_delayed_axioms() z3/build/../src/smt/theory_array_full.cpp:733
#2 0x32f77af in smt::theory_array::final_check_eh() z3/build/../src/smt/theory_array.cpp
#3 0x207ffa5 in smt::context::final_check() z3/build/../src/smt/smt_context.cpp:3793:26
#4 0x207b1e5 in smt::context::bounded_search() z3/build/../src/smt/smt_context.cpp:3707:42
#5 0x2077ccf in smt::context::search() z3/build/../src/smt/smt_context.cpp:3533:22
#6 0x2076326 in smt::context::setup_and_check(bool) z3/build/../src/smt/smt_context.cpp:3361:19
#7 0x1bfaf14 in smt_tactic::operator()(ref const&, sref_buffer<goal, 16u>&) z3/build/../src/smt/tactic/smt_tactic.cpp:199:32
#8 0x41aa076 in cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) z3/build/../src/tactic/tactical.cpp
#9 0x41aa076 in cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) z3/build/../src/tactic/tactical.cpp

Błąd jest stosunkowo łatwy do replikacji z wykorzystaniem projektu skompilowanego za pomocą afl-clang-fast (w moim przypadku jest to wrapper na Clang 6.0), “goły” Clang niestety nie umożliwia stworzenia sytuacji w której dochodzi do use-after-free (oczywiście w odbydwu przypadkach mówimy o buildzie z ASANem). Aby poszukać rozwiązania skompilujmy projekty za pomocą wcześniej wymienionych kompilatorów, a następnie nagrajmy ich wykonanie za pomocą rr. Etap kompilacji oczywiście pominę, gdyż nic nie wnosi do rozwiązania problemu.

Zapis przebiegu wykonania zapisywany jest bardzo prosto: wystarczy do tego opcja record wraz ze ścieżką do badanego programu (do nagrania w Chaos Mode dorzucamy przełącznik -h):


kamil@dev ~/D/z/build> rr record ./z3 -smt2 ~/Downloads/z3/build/uaf
rr: Saving execution to trace directory `/home/kamil/.local/share/rr/z3-0'.
WARNING: unknown attribute :
[...]
WARNING: unknown attribute :
sat


kamil@dev ~/D/z/build> rr record ./z3 -smt2 ~/Downloads/z3/build/uaf
rr: Saving execution to trace directory `/home/kamil/.local/share/rr/z3-1'.
WARNING: unknown attribute :
[...]
WARNING: unknown attribute :
=================================================================
==8629==ERROR: AddressSanitizer: heap-use-after-free on address 0x60b000010d38 at pc 0x0000032e475b bp 0x7ffc5642b990 sp 0x7ffc5642b988
READ of size 8 at 0x60b000010d38 thread T0
#0 0x32e475a in smt::theory_array_full::instantiate_axiom_map_for(int) z3/build/../src/smt/theory_array_full.cpp:69:28
#1 0x32e475a in smt::theory_array_full::assert_delayed_axioms() z3/build/../src/smt/theory_array_full.cpp:733
#2 0x32f77af in smt::theory_array::final_check_eh() z3/build/../src/smt/theory_array.cpp
#3 0x207ffa5 in smt::context::final_check() z3/build/../src/smt/smt_context.cpp:3793:26
#4 0x207b1e5 in smt::context::bounded_search() z3/build/../src/smt/smt_context.cpp:3707:42
#5 0x2077ccf in smt::context::search() z3/build/../src/smt/smt_context.cpp:3533:22
#6 0x2076326 in smt::context::setup_and_check(bool) z3/build/../src/smt/smt_context.cpp:3361:19
#7 0x1bfaf14 in smt_tactic::operator()(ref const&, sref_buffer<goal, 16u>&) z3/build/../src/smt/tactic/smt_tactic.cpp:199:32
#8 0x41aa076 in cond_tactical::operator()(ref const&, sref_buffer<goal, 16u>&) z3/build/../src/tactic/tactical.cpp/../src/smt/smt_context.cpp:3533:22
[...]

Warto w tym miejscu wspomnieć, że ASAN nie działa z Chaos Mode. Podczas uruchomienia softu w takiej konfiguracji zostaniemy uraczeni poniższym komunikatem:

==23131==Shadow memory range interleaves with an existing memory mapping. ASan cannot proceed correctly. ABORTING.
==23131==ASan shadow was supposed to be located in the [0x00007fff7000-0x10007fff7fff] range.
==23131==Process memory map follows:
0x000000400000-0x00000624c000 z3/build/z3
0x00000624c000-0x00000624e000
0x00000644c000-0x0000064b1000 z3/build/z3
0x0000064b1000-0x0000065a2000 z3/build/z3
0x0000065a2000-0x0000072a7000
0x000067c62000-0x000067dff000 /lib/x86_64-linux-gnu/libm-2.27.so
0x000067dff000-0x000067ffe000 /lib/x86_64-linux-gnu/libm-2.27.so
0x000067ffe000-0x000067fff000 /lib/x86_64-linux-gnu/libm-2.27.so
0x000067fff000-0x000068000000 /lib/x86_64-linux-gnu/libm-2.27.so
0x000068000000-0x000068200000
0x000070000000-0x000070001000 /usr/local/bin/rr_page_64
0x000070001000-0x000070002000 /tmp/rr-shared-preload_thread_locals-23131-0 (deleted)
0x000070002000-0x000070004000
0x0910772f5000-0x09107731b000 /usr/local/lib/rr/librrpreload.so
[...]
0x7f72b0c07000-0x7f72b0c1b000
0x7ffe87dfd000-0x7ffe87e20000 [stack]
0x7ffe87f3f000-0x7ffe87f41000 [vdso]
0xffffffffff600000-0xffffffffff601000 [vsyscall]
==23131==End of process memory map.

Obsługa debugowania nagranego przebiegu programu wygląda tak samo jak działającego oprogramowania poprzez gdb – obsługiwane są wszystkie funkcjonalności dobrze znane amatorom niskopoziomowego “grzebania”. Za pomocą polecenia b *0x00000000032f77b0 ustawię breakpoint chwilę przed awarią. Jest to adres funkcji wzięty z backtrace’a nagranego za pomocą rr:


#0 0x000000000051397e in __sanitizer::internal__exit(int) ()
#1 0x000000000051b8d3 in __sanitizer::Die() ()
#2 0x00000000004ff725 in __asan::ReportGenericError(unsigned long, unsigned long, unsigned long, unsigned long, bool, unsigned long, unsigned int, bool) ()
#3 0x00000000005003c8 in __asan_report_load8 ()
#4 0x00000000032e475b in smt::theory_array_full::instantiate_axiom_map_for (this=, v=) at ../src/smt/theory_array_full.cpp:69
#5 smt::theory_array_full::assert_delayed_axioms (this=) at ../src/smt/theory_array_full.cpp:733
#6 0x00000000032f77b0 in smt::theory_array::final_check_eh (this=0x616000016b88) at ../src/smt/theory_array.cpp:368
#7 0x000000000207ffa6 in smt::context::final_check (this=) at ../src/smt/smt_context.cpp:3793
#8 0x000000000207b1e6 in smt::context::bounded_search (this=) at ../src/smt/smt_context.cpp:3707
#9 0x0000000002077cd0 in smt::context::search (this=0x62400002c108) at ../src/smt/smt_context.cpp:3533
#10 0x0000000002076327 in smt::context::setup_and_check (this=, reset_cancel=true) at ../src/smt/smt_context.cpp:3361
#11 0x0000000001bfaf15 in smt_tactic::operator() (this=0x618000014c88, in=..., result=...) at ../src/smt/tactic/smt_tactic.cpp:199
#12 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#13 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#14 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#15 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#16 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#17 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#18 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#19 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#20 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#21 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#22 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#23 0x00000000041aa077 in cond_tactical::operator() (this=, in=..., result=...) at ../src/tactic/tactical.cpp:1012
#24 0x000000000418f8b7 in and_then_tactical::operator() (this=0x60400001ba18, in=..., result=...) at ../src/tactic/tactical.cpp:120
#25 0x00000000041721dd in exec (t=..., in=..., result=...) at ../src/tactic/tactic.cpp:143
#26 0x0000000004173a4d in check_sat (t=..., g=..., md=..., labels=..., pr=..., core=..., reason_unknown=...) at ../src/tactic/tactic.cpp:164
#27 0x0000000003d1ef1c in (anonymous namespace)::tactic2solver::check_sat_core (this=, num_assumptions=0, assumptions=)
at ../src/solver/tactic2solver.cpp:163
#28 0x0000000003d7cacb in solver_na2as::check_sat (this=, num_assumptions=, assumptions=) at ../src/solver/solver_na2as.cpp:67
#29 0x0000000003d34f74 in combined_solver::check_sat (this=0x7ffc5642de00, num_assumptions=0, assumptions=0x60e000003770) at ../src/solver/combined_solver.cpp:230
#30 0x00000000037b9453 in cmd_context::check_sat (this=0x7ffc5642f0a0, num_assumptions=, assumptions=)
at ../src/cmd_context/cmd_context.cpp:1521
#31 0x00000000036b99f1 in smt2::parser::parse_check_sat (this=) at ../src/parsers/smt2/smt2parser.cpp:2560
#32 0x00000000036b0dff in smt2::parser::parse_cmd (this=0x7ffc5642e6e0) at ../src/parsers/smt2/smt2parser.cpp:2896
#33 0x00000000036a9d87 in smt2::parser::operator() (this=0x7ffc5642e6e0) at ../src/parsers/smt2/smt2parser.cpp:3070
#34 0x00000000036a6de8 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=..., filename=0x0) at ../src/parsers/smt2/smt2parser.cpp:3119
#35 0x00000000005520d8 in read_smtlib2_commands (file_name=) at ../src/shell/smtlib_frontend.cpp:95
#36 0x0000000000582360 in main (argc=, argv=) at ../src/shell/main.cpp:353

Dokumentacja ASANa podrzuca bardzo interesującą wskazówkę do debuggowania: dobrym zwyczajem jest stawianie breakpointa na funkcji __asan::ReportGenericError(). Jest to funkcja pomocnicza, zbierająca dane do raportu, wykonująca się jako jeden z pierwszych etapów działania ASAN.

W zasadzie taka konfiguracja wysyca nasze potrzeby. Aby umożliwić wykonanie “w przód” można wykorzystać breakpoint przed podatną funkcją, natomiast cała siła rr zawiera się w wykonaniu do “tyłu”, którego punktem początkowym będzie drugi breakpoint. Oszczędza to olbrzymią ilość czasu na single-steppingu i podglądaniu zawartości zmiennych. Poniżej listing “szybkiej ścieżki”:


(rr) b __asan::ReportGenericError
Breakpoint 1 at 0x4ff454
(rr) r
0x00007f0f57bf2093 in _start () from /lib64/ld-linux-x86-64.so.2
The program being debugged has been started already.
Start it from the beginning? (y or n) y
Starting program: z3-1/mmap_hardlink_3_z3
Program stopped.
0x00007f0f57bf2090 in _start () from /lib64/ld-linux-x86-64.so.2
(rr) c
Continuing.
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
WARNING: unknown attribute :
Breakpoint 1, 0x00000000004ff454 in __asan::ReportGenericError(unsigned long, unsigned long, unsigned long, unsigned long, bool, unsigned long, unsigned int, bool) ()
(rr) reverse-step
Single stepping until exit from function _ZN6__asan18ReportGenericErrorEmmmmbmjb,
which has no line number information.
0x00000000005003c3 in __asan_report_load8 ()
(rr) reverse-step
Single stepping until exit from function __asan_report_load8,
which has no line number information.
0x00000000032e4125 in smt::theory_array_full::instantiate_axiom_map_for (this=,v=) at ../src/smt/theory_array_full.cpp:69
69 for (enode* ps : d->m_parent_selects)
(rr) list
64 bool theory_array_full::instantiate_axiom_map_for(theory_var v) {
65 bool result = false;
66 var_data * d = m_var_data[v];
67 var_data_full * d_full = m_var_data_full[v];
68 for (enode* pm : d_full->m_parent_maps)
69 for (enode* ps : d->m_parent_selects)
70 if (instantiate_select_map_axiom(ps, pm))
71 result = true;
72 return result;
73 }
(rr) info register
rax 0xc16000021a7 13288628822439
rbx 0x1 1
rcx 0xd87c 55420
rdx 0x7296e50 120155728
rsi 0x1 1
rdi 0x10 16
rbp 0x65a13e0 0x65a13e0 <__afl_area_ptr>
rsp 0x7ffc5642b9a0 0x7ffc5642b9a0
r8 0xfd 253
r9 0x0 0
r10 0x7f0f57def000 139703875465216
r11 0x32e413b 53363003
r12 0x48 72
r13 0x1 1
r14 0x62500019a398 108095738586008
r15 0x60b000010d38 106309030579512
rip 0x32e4125 0x32e4125 <smt::theory_array_full::assert_delayed_axioms()+1125>
eflags 0x282 [ SF IF ]
cs 0x33 51
ss 0x2b 43
ds 0x0 0
es 0x0 0
fs 0x0 0
gs 0x0 0
fs_base 0x7f0f57dd1340 0x7f0f57dd1340
gs_base 0x0 0x0

Niestety, mimo obiecującego początku dalej nie wiemy co się stało, lecz kierunek “wydaje się” dobry. Zatem podczas wykonania poobserwujmy problematyczny adres w pamięci – dodajmy watche za pomocą poleceń watch / rwatch * 0x60b000010d38. Po chwili badania naszej cierpliwości (i sprawdzania backtrace’a po każdym kroku) jesteśmy w stanie dojść do właściwej istoty problemu – jest nim brak aktualizacji wskaźnika po rozszerzeniu pamięci poprzez realloc(), przez co odnosi się on [wskaźnik] do właśnie zwolniongo miejsca, a iteracja pętli używa zwolnionego adresu wyzwalając ASANa. Niestety nie widać tego w raporcie z tego narzędzia (pogrubiona część listingu – ostatni widoczny element w pierwszym raporcie to metoda smt::theory_array_full::instantiate_select_map_axiom()):


Hardware read watchpoint 3: * 0x60b000011578

Value = 1436728
0x0000000001eec37a in smt::theory_array_full::instantiate_axiom_map_for (this=0x615000006c08, v=20)
at ../src/smt/theory_array_full.cpp:69
69 for (enode* ps : d->m_parent_selects)
(rr) p ps
$4 = (smt::enode *) 0x60d0001962a8
(rr) p d->m_parent_selects
$5 = {<vector<smt::enode*, false, unsigned int>> = {m_data = 0x60b000011560}, }
(rr) c
Continuing.

Hardware read watchpoint 3: * 0x60b000011578

Value = 1436728
0x0000000001eec37a in smt::theory_array_full::instantiate_axiom_map_for (this=0x615000006c08, v=20)
at ../src/smt/theory_array_full.cpp:69
69 for (enode* ps : d->m_parent_selects)
(rr) c
Continuing.

Hardware read watchpoint 3: * 0x60b000011578

Value = 1436728
__memmove_sse2_unaligned_erms () at ../sysdeps/x86_64/multiarch/memmove-vec-unaligned-erms.S:335
335 ../sysdeps/x86_64/multiarch/memmove-vec-unaligned-erms.S: No such file or directory.
(rr) bt
#0 __memmove_sse2_unaligned_erms () at ../sysdeps/x86_64/multiarch/memmove-vec-unaligned-erms.S:335
#1 0x0000000000449dcd in __asan::asan_realloc(void*, unsigned long, __sanitizer::BufferedStackTrace*) ()
#2 0x00000000004fed0a in realloc ()
#3 0x00000000035ab311 in memory::reallocate (p=0x60b000011558, s=160)
at ../src/util/memory_manager.cpp:319
#4 0x00000000012761fd in vector<smt::enode*, false, unsigned int>::expand_vector (this=0x60400002d660)
at ../src/util/vector.h:84
#5 0x0000000001275a7d in vector<smt::enode*, false, unsigned int>::push_back (this=0x60400002d660,
elem=@0x7fff5d46c5a0: 0x60d0001962a8) at ../src/util/vector.h:371
#6 0x0000000001f0348a in smt::theory_array::add_parent_select (this=0x615000006c08, v=20,
s=0x60d0001962a8) at ../src/smt/theory_array.cpp:97
#7 0x0000000001ef4d22 in smt::theory_array_full::add_parent_select (this=0x615000006c08, v=20,
s=0x60d0001962a8) at ../src/smt/theory_array_full.cpp:362
#8 0x0000000001ef58d1 in smt::theory_array_full::relevant_eh (this=0x615000006c08, n=0x607000047fa8)
at ../src/smt/theory_array_full.cpp:396
#9 0x00000000014385b1 in smt::context::relevant_eh (this=0x62400002e108, n=0x607000047fa8)
at ../src/smt/smt_context.cpp:1627
#10 0x000000000141657b in smt::relevancy_propagator_imp::set_relevant (this=0x60f000003018,
n=0x607000047fa8) at ../src/smt/smt_relevancy.cpp:308
#11 0x000000000140fa57 in smt::relevancy_propagator_imp::mark_as_relevant (this=0x60f000003018,
n=0x607000047fa8) at ../src/smt/smt_relevancy.cpp:336
#12 0x000000000140e493 in smt::relevancy_propagator_imp::propagate_relevant_app (this=0x60f000003018,
n=0x60700005e4a8) at ../src/smt/smt_relevancy.cpp:357
#13 0x000000000141058d in smt::relevancy_propagator_imp::propagate (this=0x60f000003018)
at ../src/smt/smt_relevancy.cpp:480
#14 0x000000000129a6ac in smt::context::mark_as_relevant (this=0x62400002e108, n=0x60700005ef28)
at ../src/smt/smt_context.h:1208
#15 0x000000000129a59b in smt::context::mark_as_relevant (this=0x62400002e108, v=146)
at ../src/smt/smt_context.h:1212
#16 0x000000000129a517 in smt::context::mark_as_relevant (this=0x62400002e108, l=…)
at ../src/smt/smt_context.h:1214
#17 0x0000000001ef621b in smt::theory_array_full::try_assign_eq (this=0x615000006c08, v1=0x60700005e3c8,
v2=0x60700005e518) at ../src/smt/theory_array_full.cpp:761
#18 0x0000000001eebf9f in smt::theory_array_full::instantiate_select_map_axiom (this=0x615000006c08,
sl=0x60d0001962a8, mp=0x60d00015f6c8) at ../src/smt/theory_array_full.cpp:483
#19 0x0000000001eec38f in smt::theory_array_full::instantiate_axiom_map_for (this=0x615000006c08, v=20)
at ../src/smt/theory_array_full.cpp:70
#20 0x0000000001ef7084 in smt::theory_array_full::assert_delayed_axioms (this=0x615000006c08)
at ../src/smt/theory_array_full.cpp:733
#21 0x0000000001f0710b in smt::theory_array::final_check_eh (this=0x615000006c08)
at ../src/smt/theory_array.cpp:382
#22 0x000000000145ead6 in smt::context::final_check (this=0x62400002e108)
at ../src/smt/smt_context.cpp:3793
#23 0x0000000001459cb1 in smt::context::bounded_search (this=0x62400002e108)
at ../src/smt/smt_context.cpp:3707
#24 0x0000000001455f92 in smt::context::search (this=0x62400002e108) at ../src/smt/smt_context.cpp:3533
#25 0x00000000014545bd in smt::context::setup_and_check (this=0x62400002e108, reset_cancel=true)
at ../src/smt/smt_context.cpp:3361
#26 0x000000000126349a in smt::kernel::imp::setup_and_check (this=0x62400002e108)
at ../src/smt/smt_kernel.cpp:107
#27 0x000000000126204d in smt::kernel::setup_and_check (this=0x602000000658)
at ../src/smt/smt_kernel.cpp:285
#28 0x00000000011a919f in smt_tactic::operator() (this=0x618000014c88, in=…, result=…)
at ../src/smt/tactic/smt_tactic.cpp:199
#29 0x0000000002676940 in cond_tactical::operator() (this=0x604000021a98, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#30 0x0000000002676940 in cond_tactical::operator() (this=0x604000021ad8, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#31 0x0000000002676940 in cond_tactical::operator() (this=0x604000021b18, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
—Type to continue, or q to quit—
#32 0x0000000002676940 in cond_tactical::operator() (this=0x604000021b58, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#33 0x0000000002676940 in cond_tactical::operator() (this=0x604000021b98, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#34 0x0000000002676940 in cond_tactical::operator() (this=0x604000021bd8, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#35 0x0000000002676940 in cond_tactical::operator() (this=0x604000021c18, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#36 0x0000000002676940 in cond_tactical::operator() (this=0x604000021c58, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#37 0x0000000002676940 in cond_tactical::operator() (this=0x604000021c98, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#38 0x0000000002676940 in cond_tactical::operator() (this=0x604000021cd8, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#39 0x0000000002676940 in cond_tactical::operator() (this=0x604000021d18, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#40 0x0000000002676940 in cond_tactical::operator() (this=0x604000021d58, in=…, result=…)
at ../src/tactic/tactical.cpp:1012
#41 0x0000000002665cf4 in and_then_tactical::operator() (this=0x604000021d98, in=…, result=…)
at ../src/tactic/tactical.cpp:120
#42 0x000000000267327d in unary_tactical::operator() (this=0x604000021dd8, in=…, result=…)
at ../src/tactic/tactical.cpp:750
#43 0x0000000002659d28 in exec (t=…, in=…, result=…) at ../src/tactic/tactic.cpp:143
#44 0x000000000265a6ff in check_sat (t=…, g=…, md=…, labels=…, pr=…, core=…) at ../src/tactic/tactic.cpp:164
#45 0x000000000241a921 in (anonymous namespace)::tactic2solver::check_sat_core (this=0x60e000003308,
num_assumptions=0, assumptions=0x0) at ../src/solver/tactic2solver.cpp:163
#46 0x0000000002446c94 in solver_na2as::check_sat (this=0x60e000003308, num_assumptions=0,
assumptions=0x60e000003850) at ../src/solver/solver_na2as.cpp:67
#47 0x0000000002420b1c in combined_solver::check_sat (this=0x60700000b078, num_assumptions=0,
assumptions=0x60e000003850) at ../src/solver/combined_solver.cpp:263
#48 0x000000000212e1fe in cmd_context::check_sat (this=0x7fff5d475ae0, num_assumptions=0,
assumptions=0x60e000003850) at ../src/cmd_context/cmd_context.cpp:1521
#49 0x00000000020d2c80 in smt2::parser::parse_check_sat (this=0x7fff5d4750c0)
at ../src/parsers/smt2/smt2parser.cpp:2560
#50 0x00000000020d0126 in smt2::parser::parse_cmd (this=0x7fff5d4750c0)
at ../src/parsers/smt2/smt2parser.cpp:2896
#51 0x00000000020ca7d5 in smt2::parser::operator() (this=0x7fff5d4750c0)
at ../src/parsers/smt2/smt2parser.cpp:3070
#52 0x00000000020c97b9 in parse_smt2_commands (ctx=…, is=…, interactive=false, ps=…, filename=0x0)
at ../src/parsers/smt2/smt2parser.cpp:3119
#53 0x000000000055a90b in read_smtlib2_commands (file_name=0x7fff5d4772f4 “uaf”)
at ../src/shell/smtlib_frontend.cpp:95
#54 0x00000000005922cb in main (argc=3, argv=0x7fff5d476508) at ../src/shell/main.cpp:353

Debugowanie i reprodukcja tego błędu byłaby o wiele prostsza, gdyby tylko ASAN zechciał wyświetlić pełen log, aczkolwiek przez to nie byłoby pomysłu na tego posta 🙂

Podsumowanie i krótki algorytm postępowania dla niedeterministycznych błędów

Mimo olbrzymich zasług w obszarach naprawiania i wykrywania błędów typu memory corruption, ASAN nie jest idealny i czasami zachodzi konieczność weryfikacji znalezionych błędów o wysokiej trudności reprodukcji za pomocą rr, które bardzo fajnie działa z wykorzystaniem “hacków” od twórców AddressSanitizera. Debugowanie z możliwością poruszania się w obydwu kierunkach jest dla mnie świetne i znacząco usprawnia efektywność tropienia “trudnych” podatności.

Dla wszystkich osób, które chcą zachować pierwotny kolor włosów, zostawiam proces rozwiązywania problemów za pomocą rr (lub po prostu TLDR):

  1. Kompilacja projektu z ASANem,
  2. Nagranie wykonania za pomocą rr (bez Chaos Mode),
  3. Wyzwolenie błędu poprzez rr replay oraz zapisanie problematycznych adresów,
  4. Watche (zapis i odczyt) na w/w adresy,
  5. Breakpoint na metodzie __asan::ReportGenericError(),
  6. Reverse-Step według potrzeb,
  7. Sprawdzanie backtrace’a do momentu dokopania sie do ostatniego zapisu lub odczytu obszaru pamięci,
  8. Profit? Niekoniecznie i nie zawsze! 😉

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.