Hello, it’s Hackability, a Security Researcher at SOOHO.
In this article, I’ll describe how to analyze bugs and how to make exploits of well-known SMT (Satisfiability Modulo Theories) Solver named z3-solver.
Finding Bugs
I’ve found a bug from the z3-solver python package by an accident. (misuse of internal API function)
initial crash log
I’ve searching this issue in z3 github and I realized that this issue (exactly same) is opened last year. However, the author of z3 commented that this kind of type confusion has no effect and this is because misuse of internal APIs. And he closed this issue.
Type Confusion of Z3_inc_ref version <= 4.7.1 · Issue #1639 · Z3Prover/z3 While working with Z3, I found that missing parsing value before call Z3_inc_ref which lead to memory corruption or…github.com
I had no plans to do in this weekend, but I think I found what to do in this weekend. Did I found any of fun? yeah! a lot!
Analyzing bugs and Development exploits
I made my own custom python script fuzzer in last year and with that fuzzer, I can see lots of segmentation fault logs.
However, even the logs can reproduce segmentation fault, not all the logs are not be exploitable. I need to find a log that controls the program execution flow by tainted registers by my input. So, I digging deeper and found a log that taint useful registers and the registers can control the execution program flow.
A PoC from the python script fuzzer
When I debugged the fuzzer log, I can see the segmentation fault by accessing invalid memory. (mov rdx, QWORD PTR [rax-0x18])
Segmentation fault by the PoC script
The reason that I’m picking up this log because there is an indirect call (jmp rax) gadget is exist after crashing point. So, if I can execute the crashed instruction by modifying input, this control flow may meet the jmp rax (rax is tainted) and we can control the execution flow where we want to.
Now, I’ll analyze the reasons why the crash is happened (segmentation fault) and how we can bypass the crash that through to the indirect call in step-by-step.
The modified PoC is look like this,
modified PoC
In the first argument, I put the byte sequence because general python string is multi-bytes which is not compact my input. The second and third argument are same as the fuzzer log. And you can see the input function for debugging purpose. Because of this trick, the z3 library is loaded in virtual memory when z3 is imported. So, after importing the z3 (this means libz3 is loaded in virtual memory) and attaching the process, we can put a break point (bp) in z3 library and debug it.
When we attached the execution of modified PoC python script, the memory mapping of z3 library looks like this,
0x7f480e578000 r-xp libz3.so 0x7f480f884000 ---p libz3.so 0x7f480fa83000 rw-p libz3.so
We can point out that the address 0x7f480e578000 is the code base address of libz3.so because the memory execution authority has executable authority. What we want to trace is the function api::context::set_error_code (crash location). The offset of this function is 0xeb870 from libz3.so code base address so that we should put a break point to the code base address + offset of the function. (0x7f480e663870= 0x7f480e578000+0xeb870)
FYI, most of recent linux kernels enable ASLR (Address Space Layout Randomization) by default. So, when you re-execute the poc script, the code base of libz3 is changed. The solution is to re-calculate code base address every execution time or you can modify sysctl option to disable ASLR. The offset of function from the code base address is always same.
sudo sysctl -a ; to see all sysctls
sudo sysctl -w kernel.randomize_va_space=0 ; 0 - disable ASLR ; 1 - half ASLR ; 2 - full ASLR <- default
When we put a bp and send enter key interrupt to python script, the debugger breaks the execution at the bp and wait our input.
api::context::set_error_code entry point
It looks like perfectly landed where we want to analyze. Before we going further, check the registers which are tainted by our input. It looks rdi, [r10], r12 and r14 registers are tainted by our input. And after few more steps rdx register is also tainted by tainted register, so that we can control the rdx, too.
EB870 push r13 EB872 push r12 EB874 push rbp EB875 mov ebp, esi EB877 push rbx EB878 mov rbx, rdi EB87B sub rsp, 8 EB87F test esi, esi EB881 mov [rbx+518h], esi EB887 jnz short loc_EB898
loc_EB889: EB889 add rsp, 8 EB88D pop rbx EB88E pop rbp EB88F pop r12 EB891 pop r13 EB893 retn EB894 align 8 EB898
loc_EB898: EB898 mov rax, [rdi+528h]
At the address 0xEB887, it compares [rbx + 0x518] and rsi. If they are not same, the control flow branched to 0xeb989. If they are same, there is a return in the end of branched basic block, so we need to make [rbx + 0x518] is same as rsi.
Condition 1: [rbx + 0x518] != rsi
loc_EB898: EB898 mov rax, [rdi+528h] EB89F mov r12, rdx EB8A2 lea r13, [rdi+528h] EB8A9 xor ecx, ecx EB8AB xor esi, esi EB8AD mov rdi, r13 EB8B0 mov rdx, [rax-18h] EB8B4 call __ZNSs9_M_mutateEmmm EB8B9 test r12, r12 EB8BC jz short loc_EB8D4 EB8BE mov rdi, r12 EB8C1 call _strlen EB8C6 mov rsi, r12 EB8C9 mov rdx, rax EB8CC mov rdi, r13 EB8CF call __ZNSs6assignEPKcm
loc_EB8D4: EB8D4 mov rax, [rbx+520h]
When we check the next block (from 0xEB898), it assigns [rdi + 0x528] to rax. At this point, rdi is tainted value so that rax is also tainted value. And then r13 has similar situaltion as rax, but there is small different situation between rax and r13. In the rax case, we can controlled the value of rax. In the r13 case we can’t control the value of r13 register. We only control pointed value by r13 (then r13 must be valid memory address). Btw r13 is still useful tainted value in this case.
We can reach to address 0xEB8D4 through some calls (0xEB8B4, 0xEB8CF).
loc_EB8D4: EB8D4 mov rax, [rbx+520h] EB8DB test rax, rax EB8DE jz short loc_EB889 EB8E0 lea rdx, g_z3_log EB8E7 cmp qword ptr [rdx], 0 EB8EB jz short loc_EB8F7 EB8ED lea rdx, g_z3_log_enabled EB8F4 mov byte ptr [rdx], 1
loc_EB8F7: EB8F7 add rsp, 8 EB8FB mov rdi, rbx EB8FE mov esi, ebp EB900 pop rbx EB901 pop rbp EB902 pop r12 EB904 pop r13 EB906 jmp rax
We can see the indirect call (jmp rax). It looks like we almost there! The final conditional branch is at 0xEB8DE. If we not met the condition (not branched to 0xEB889), we can reach to the indirect call.
Condition 2: test rax, rax (rax != 0)
First, it assigns [rbx + 0x520] to rax. At this point, rbx points our controlled value. However, we just put ‘A’ * 0x100 as first argument in our poc code. So we don’t know what value will be in offset 0x520 of our input. If we didn’t control [rbx + 0x520], the conditional branch (test rax, rax; jz 0xEB889) would be taken which is not our expectation.
So, we need to modify the poc code. We need to put ‘A’*0x520 and ‘B’*8 as the first argument. We expect that when we met 0xEB8D4 instruction (mov rax, [rbx+0x520]), the rax should have ‘BBBBBBBB’.
modified_poc_02.py
an another crash point
What the … There is an another segmentation fault. The rip is not reached to 0xEB8D4. The reason of segmentation is obvious that the rax has weird value and it tries to access with that. (mov rdx, QWORD PTR [rax-0x18])
We need to figure it out where the value of rax is from.
loc_EB898: EB898 mov rax, [rdi+528h] EB89F mov r12, rdx EB8A2 lea r13, [rdi+528h] EB8A9 xor ecx, ecx EB8AB xor esi, esi EB8AD mov rdi, r13 EB8B0 mov rdx, [rax-18h]
Ahh.. It looks they assign [rdi + 0x528] to rax (at this point, rdi points to our controlled value).
rax is assigned
We only put 0x528 bytes as first argument so that we don’t know what value is in offset 0x528. We need to put 8 bytes more in the first arugment. The important thing is that as you can see the crashed instruction, they de-reference of the value. This means that the added 8 bytes should be valid memory address and (8 bytes — 0x18) is also valid address
Condition 3: mov rdx, [rax-0x18] (rax-0x18 is valid memory address)
We’ve faced an another condition here that we need to find valid address that the address minus 0x18 is valid address AND THE ADDRESS IS SHOULD STATIC.
may you already know that we can handle this issue with using other python functions or OOB bug to leak the dynamically changed addresses, but here, I don’t want to use any of them and I want to make this exploit as easy as possible
The static address means that the address is not changed every execution time.
“Hmm. Wait. You said the address is changed every execution time by ASLR. How can we get the static address in execution time?”
Yes, but only dynamic linked libraries’ base addresses are changed in every execution. The code base address of main program (in this case python3.6) is not affected by ASLR. The code base address is affected by how the program binary is compiled. When I checked the python binary, PIE (Position Independent Executable) is disabled, so executed program code base, data and bss sections are always static not changed every execution time.
The bss location is 0x9b4000 which is static address.
Memory dump of BSS section
There are lots of valid address in bss section. I just put address + 0x100 (roughly). I put +0x100 roughly but you should check that 8 byte data should be a valid address.
adding the static address which in bss section
After executing the modified poc script, we can see the debugger is stopped at jmp rax that the rax has ‘BBBBBBBB’ what we expected.
jmp 0x4242424242424242 lol
Now, we can jump anywhere we want to. Generally, we want to pwn the shell, right? so we need to call system or exec kind system functions. In the python binary, the system function is already exposed in plt section so we can use this address.
.plt:41F4E0 ; int system(const char *command) .plt:41F4E0 _system proc near .plt:41F4E0 jmp cs:off_9B4348 .plt:41F4E0 _system endp
Now, we think that when we jump to system, how to put the first argument of the system call. The first argument is passed via rdi but rdi is already tainted by our payload at this point.
The final poc is like this
final exploit code
The result is like this
Pwn the shell !
Yeah!
Conclusion
In this article, I’ve described how to analyze and how to pwn the shell from the z3-solver type confusion bug.
I’ve found that many python packages which interface with C library didn’t check proper type or size of user input. This is because its hard to check and python sandbox policy is not strong enough.
If you are not familiar with exploit development, I recommend to start with python because way easier than other application and these processes (finding, analyzing and weaponizing) are similar to other applications.
You can support me to clap if you fun to read this article. This is huge motivation for me to keep writing articles
If you have any questions of this article, feel free to leave comments or contact me (hackability@sooho.io)
가입하기
