Triton and Symbolic execution on GDB

50 mins talk on HITCON Community 2017

1. Triton and Symbolic execution on GDB 2017/08/26 @ HITCON bananaappletw
2. $whoami • 陳威伯(bananaappletw) • Master of National Chiao Tung University • Organizations: • Software Quality Laboratory • Bamboofox member • Vice president of NCTUCSC • Specialize in: • symbolic execution • binary exploit • Talks: • HITCON CMT 2015
3. Outline • Why symbolic execution? • Symbolic execution? • Triton • SymGDB
4. Why symbolic execution?
5. In the old days • Static analysis • Dynamic analysis
6. Static analysis • objdump • IDA PRO
7. Dynamic analysis • GDB • ltrace • strace
8. Symbolic execution!!!
9. What is symbolic execution? • Symbolic execution is a means of analyzing a program to determine what inputs cause each part of a program to execute • System-level • S2e(https://github.com/dslab-epfl/s2e) • User-level • Angr(http://angr.io/) • Triton(https://triton.quarkslab.com/) • Code-based • klee(http://klee.github.io/)
10. Symbolic execution Z == 12 fail() "OK"
11. Triton • Website: https://triton.quarkslab.com/ • A dynamic binary analysis framework written in C++. • developed by Jonathan Salwan • Python bindings • Triton components: • Symbolic execution engine • Tracer • AST representations • SMT solver Interface
12. Triton Structure
13. Symbolic execution engine • The symbolic engine maintains: • a table of symbolic registers states • a map of symbolic memory states • a global set of all symbolic references Step Register Instruction Set of symbolic expressions init eax = UNSET None ⊥ 1 eax = φ1 mov eax, 0 {φ1=0} 2 eax = φ2 inc eax {φ1=0,φ2=φ1+1} 3 eax = φ3 add eax, 5 {φ1=0,φ2=φ1+1,φ3=φ2+5}
14. Triton Tracer • Tracer provides: • Current opcode executed • State context (register and memory) • Translate the control flow into AST Representations • Pin tracer support
15. AST representations • Triton converts the x86 and the x86-64 instruction set semantics into AST representations • Triton's expressions are on SSA form • Instruction: add rax, rdx • Expression: ref!41 = (bvadd ((_ extract 63 0) ref!40) ((_ extract 63 0) ref!39)) • ref!41 is the new expression of the RAX register • ref!40 is the previous expression of the RAX register • ref!39 is the previous expression of the RDX register
16. AST representations • mov al, 1 • mov cl, 10 • mov dl, 20 • xor cl, dl • add al, cl
17. Static single assignment form(SSA form) • Each variable is assigned exactly once • y := 1 • y := 2 • x := y Turns into • y1 := 1 • y2 := 2 • x1 := y2
18. Why SSA form? y1 := 1 (This assignment is not necessary) y2 := 2 x1 := y2 • When Triton process instructions, it could ignore some unnecessary instructions. • It saves time and memory.
19. Symbolic variables • Make ecx symbolic variable • convertRegisterToSymbolicVariable(REG.ECX) • isRegisterSymbolized(REG.ECX) == True • test ecx, ecx (ZF = ECX & ECX = ECX) • je +7 (isRegisterSymbolized(REG.EIP) == True)(jump to nop if ZF=1) • mov edx, 0x64 • nop
20. SMT solver Interface
21. Example • Defcamp 2015 r100 • Program require to input the password • Password length could up to 255 characters
22. Defcamp 2015 r100
23. Defcamp 2015 r100
24. Defcamp 2015 r100 • Set Architecture • Load segments into triton • Define fake stack ( RBP and RSP ) • Symbolize user input • Start to processing opcodes • Set constraint on specific point of program • Get symbolic expression and solve it
25. Set Architecture
26. Load segments into triton
27. Define fake stack ( RBP and RSP )
28. Symbolize user input
29. Start to processing opcodes
30. Get symbolic expression and solve it
31. Some problems of Triton • The whole procedure is too complicated • High learning cost to use Triton • With support of debugger, many steps could be simplified
32. SymGDB • Repo: https://github.com/SQLab/symgdb • Symbolic execution support for GDB • Combined with: • Triton • GDB Python API • Symbolic environment • symbolize argv
33. Design and Implementation • GDB Python API • Failed method • Successful method • Flow • SymGDB System Structure • Implementation of System Internals • Relationship between SymGDB classes • Supported Commands • Symbolic Execution Process in GDB • Symbolic Environment • symbolic argv • Debug tips
34. GDB Python API • API: https://sourceware.org/gdb/onlinedocs/gdb/Python-API.html • Source python script in .gdbinit • Functionalities: • Register GDB command • Register event handler (ex: breakpoint) • Execute GDB command and get output • Read, write, search memory
35. Register GDB command
36. Register event handler
37. Execute GDB command and get output
38. Read memory
39. Write memory
40. Failed method • At first, I try to use Triton callback to get memory and register values • Register callbacks: • needConcreteMemoryValue • needConcreteRegisterValue • Process the following sequence of code • mov eax, 5 • mov ebx,eax (Trigger needConcreteRegisterValue) • We need to set Triton context of eax
41. Triton callbacks
42. Problems • Values from GDB are out of date • Consider the following sequence of code • mov eax, 5 • We set breakpoint here, and call Triton's processing() • mov ebx,eax (trigger callback to get eax value, eax = 5) • mov eax, 10 • mov ecx, eax (Trigger again, get eax = 5) • Because context state not up to date
43. Tried solutions • Before needed value derived from GDB, check if it is not in the Triton's context yet Not working! Triton will fall into infinite loop
44. Successful method • Copy GDB context into Triton • Load all the segments into Triton context • Symbolic execution won't affect original GDB state • User could restart symbolic execution from breakpoint
45. Flow • Get debugged program state by calling GDB Python API • Get the current program state and yield to triton • Set symbolic variable • Set the target address • Run symbolic execution and get output • Inject back to debugged program state
46. SymGDB System Structure
47. Implementation of System Internals • Three classes in the symGDB • Arch(), GdbUtil(), Symbolic() • Arch() • Provide different pointer size、register name • GdbUtil() • Read write memory、read write register • Get memory mapping of program • Get filename and detect architecture • Get argument list • Symbolic() • Set constraint on pc register • Run symbolic execution
48. Relationship between SymGDB classes
49. Supported Commands Command Option Functionality symbolize argv memory [address][size] Make symbolic target address Set target address triton None Run symbolic execution answer None Print symbolic variables debug symbolic gdb Show debug messages
50. Symbolic Execution Process in GDB • gdb.execute("info registers", to_string=True) to get registers • gdb.selected_inferior().read_memory(address, length) to get memory • setConcreteMemoryAreaValue and setConcreteRegisterValue to set triton state • In each instruction, use isRegisterSymbolized to check if pc register is symbolized or not • Set target address as constraint • Call getModel to get answer • gdb.selected_inferior().write_memory(address, buf, length) to inject back to debugged program state
51. Symbolic Environment: symbolic argv • Using "info proc all" to get stack start address • Examining memory content from stack start address • argc • argv[0] • argv[1] • …… • null • env[0] • env[1] • …… • null argc argument counter(integer) argv[0] program name (pointer) argv[1] program args (pointers) … argv[argc-1] null end of args (integer) env[0] environment variables (pointers) env[1] … env[n] null end of environment (integer)
52. Debug tips • Simplify: https://github.com/JonathanSalwan/Triton/blob/master/src/example s/python/simplification.py
53. Demo • Examples • crackme hash • crackme xor • GDB commands • Combined with Peda
54. crackme hash • Source: https://github.com/illera88/Ponce/blob/master/examples/crackme_h ash.cpp • Program will pass argv[1] to check function • In check function, argv[1] xor with serial(fixed string) • If sum of xored result equals to 0xABCD • print "Win" • else • print "fail"
55. crackme hash
56. crackme hash
57. crackme hash
58. crackme xor • Source: https://github.com/illera88/Ponce/blob/master/examples/crackme_xor.cpp • Program will pass argv[1] to check function • In check function, argv[1] xor with 0x55 • If xored result not equals to serial(fixed string) • return 1 • print "fail" • else • go to next loop • If program go through all the loop • return 0 • print "Win"
59. crackme xor
60. crackme xor
61. crackme xor
62. GDB commands
63. GDB commands
64. Combined with Peda • Same demo video of crackme hash • Using find(peda command) to find argv[1] address • Using symbolize memory argv[1]_address argv[1]_length to symbolic argv[1] memory
65. Combined with Peda
66. Drawbacks • Triton doesn't support GNU c library • Why? • SMT Semantics Supported: https://triton.quarkslab.com/documentation/doxygen/SMT_Semanti cs_Supported_page.html • Triton has to implement system call interface to support GNU c library
67. Triton versus Angr Difference Triton Angr Architecture support x86 amd64 x86 amd64 arm …… GNU c library support No Yes Path selection No Yes
68. References • Wiki: https://en.wikipedia.org/wiki/Symbolic_execution • Triton: https://triton.quarkslab.com/ • GDB Python API: https://sourceware.org/gdb/onlinedocs/gdb/Python-API.html • Peda: https://github.com/longld/peda • Ponce: https://github.com/illera88/Ponce • Angr: http://angr.io/
69. Bamboofox
70. Q & A
71. Thank you