The goal here is to find valid IOCTL codes for the HackSysExtremeVulnerableDriver by analyzing only the binary. The control flow varies between the binary and source due to compiler optimizations. This results in a situation where only a few IOCTL codes in the assembly are represented as a constant with the remaining being computed at runtime.
The code in hevd_ioctl.py is a approximation of the control flow of the compiled
IrpDeviceIoCtlHandler function. The effects of the compiler optimization are more pronounced when comparing this code to the original C function. To comply with requirements of the PyExZ3 module, the target function is named after the script's filename, and the
expected_result function is defined. A
@symbolic decorator is added to the
ioctl parameter to treat it symbolically.
The IOCTL codes are automatically discovered by running
λ "C:\Program Files (x86)\Python36-32\python.exe" pyexz3.py hevd_ioctl.py PyExZ3 (Python Exploration with Z3) Exploring hevd_ioctl.hevd_ioctl ... [('ioctl', '0x22201f')] HACKSYS_EVD_IOCTL_ALLOCATE_FAKE_OBJECT [('ioctl', '0x222003')] HACKSYS_EVD_STACKOVERFLOW [('ioctl', '0x222007')] HACKSYS_EVD_IOCTL_STACK_OVERFLOW [('ioctl', '0x22200b')] HACKSYS_EVD_IOCTL_ARBITRARY_OVERWRITE [('ioctl', '0x22200f')] HACKSYS_EVD_IOCTL_POOL_OVERFLOW [('ioctl', '0x222013')] HACKSYS_EVD_IOCTL_ALLOCATE_UAF_OBJECT [('ioctl', '0x222017')] HACKSYS_EVD_IOCTL_USE_UAF_OBJECT [('ioctl', '0x22201b')] HACKSYS_EVD_IOCTL_FREE_UAF_OBJECT [('ioctl', '0x222023')] HACKSYS_EVD_IOCTL_TYPE_CONFUSION [('ioctl', '0x222027')] HACKSYS_EVD_IOCTL_INTEGER_OVERFLOW [('ioctl', '0x22202b')] HACKSYS_EVD_IOCTL_NULL_POINTER_DEREFERENCE [('ioctl', '0x22202f')] HACKSYS_EVD_IOCTL_UNINITIALIZED_STACK_VARIABLE [('ioctl', '0x222033')] HACKSYS_EVD_IOCTL_UNINITIALIZED_HEAP_VARIABLE [('ioctl', '0x222037')] HACKSYS_EVD_IOCTL_DOUBLE_FETCH hevd_ioctl test passed <---
If you'd like to run this on your own, I did the following steps to setup PyExZ3:
- Download and extract the contents of the PyExZ3 zipball to
- Download the Z3 release and extract the binaries in
- Also place the
- Optional: Modify the
PyExZ3\symbolic\explore.pyto return hex values.
There are probably more automated techniques for this use case than re-coding the control-flow logic in Python, but thought I'd share a simple example.