Exploit Development (z3-solver)


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
EB889  add     rsp, 8
EB88D  pop     rbx
EB88E  pop     rbp
EB88F  pop     r12
EB891  pop     r13
EB893  retn
EB894  align 8
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

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
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).

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
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’.


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.

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 !



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)

기업문화 엿볼 때, 더팀스