inputs. Symbol is similar to mathematical variables, and is NOT fixed values. In symbolic execution, execution environment such as registers, stack, memory, and files are symbolized. What is symbolic execution? Concept of Forward Symbolic Execution (FSE) (FSE is a method often adopted to implement symbolic execution) void testme(int a, int b) { int c = 0; if (a * b == 6) { c = 1; if (a == 1) c = 3; } assert(a * b * c == 6); } a ✕ b = 6 ∧ c ≠ 0 a ✕ b ≠ 6 ∧ c = 0 Φ a ✕ b = 6 ∧ a = 1 ∧ c = 1 a ✕ b = 6 ∧ a ≠ 1 ∧ c = 1 ✔ Assertion pass ✔ Assertion pass ✔ Assertion fail … path constraint
good solutions mitigates weakness of symbolic execution? Black box that fulfills her wish ? Exploit Code Something Good Symbolic Execution ((o( ∀ )o)) What... what is it?
notes Pointer can be overwritten by buffer over flow bug Deploys shellcode to known address to make things simple About demo application to be exploited Futaba% ./notes ---- [menu] ---- n: new note u: update note s: show notes q: quit input command: n ==== [note #0] ==== title: Futaki Futaba content: I’m a high school student. ---- [menu] ---- ... snipped ... input command: s note #0:Futaki Futaba I’m a high school student. typedef struct { char* content; char title[16]; } note; note notes[8]; void update_note(unsigned int note_id) { ... snipped ... _printf(“title: "); _fgets(notes[note_id].title, 1024, stdin); } Buffer overflow bug section Definition of notes struct Pointer can be overwritten BOF
Tracer: can symbolically execute paths follows given input • libc: can symbolically fast execute libc Futaba <| Which symbolic execution engine should I use? | Triton angr KLEE S2E Published in 2015 2016 2008 2011 Usability Medium Easy Easy Medium Hard User Script Python Python command line, C/C++ Lua, C++ Tracer Available Not Works N/A N/A libc Fully Symbolically Executed Replaced with Symbolic Procedure 1) Engine is written in C++ Python C++ C++ Essential requirements when crash occurs in libc Comparison of symbolic execution engine Crashable execution path is known 1) libc can be symbolically executed, but slow
a crash input? mov byte ptr [rbp], al Invalid Memory Access Native execution Symbolic Execution following traced path • Path constraint • Memory access constraint mov byte ptr [symvar_rbp], symvar_al Theorem on arbitrary memory overwrite: Be able to write value a on memory address A when executing this instruction ⇔constraint symvar_rbp == A, symvar_al == a is satisfiable • Crash Generate crash input Arbitrary Memory Overwrite PC Hijack Trigger shellcode Tracer executes according input of . Outputs instructions trace. NOTE: Described in AFL verification phase Crash input from AFL
a crash input? GOT (Global Offset Table) holds libc function address. Using GOT Overwrite, libc function address are overwritten with X (*A = X). fputs() fputs@libc() Index Real Addr fputs fputs@libc GOT lookup call func fputs() X() Index Real Addr fputs X GOT (Overwritten) lookup call func This time, there is a function to invoke shell and this address is known. Let X be shellcode address. (In case of GOT Overwrite) Generate crash input Arbitrary Memory Overwrite PC Hijack Trigger shellcode
it is fixed by her (my) pull request*. Triton can handle signals caused by Tracers, but Tracer ignores SIGBUS and terminates Triton. Fixed to handle SIGBUS in Tracer z3** throws (exception z3::exception) when constraint is wrong. Triton passes on this exception and exits with no messages. Fixed to catch this exception (thanks Jonathan for helping! Run-time error of Triton * This pullreq #695 is merged to dev-v0.6 branch. dev-v0.6 was merged with master branch in Jun 29, 2018. ** z3 is a constraint solver. Triton leverages z3 in back-end.
exploit generation with the following approach. 1. Generate input causes crash using fuzzing 2. Execute the path may triggers crash symbolically 3. Solve constraints and generate exploit code Futaba&Aoi’s (my) AEG is available on GitHub: https://github.com/macaron-et/wasabi-aeg Apply this tool to other vulnerable application. Find exploitable crash using fuzzing. (Sadly, pwn binaries of CTF may have meaningless DoS vulnerabilities) Conclusion: Automated Exploit Generation Try it!