Recovering HEVD IOCTLs with Symbolic Execution

The goal here is to find valid IOCTL codes for the HackSys Extreme Vulnerable Driver (HEVD) 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 pyexz3.py hevd_ioctl.py:

λ "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 <---

Click here to download the source code.

If you’d like to run this on your own, I did the following steps to setup PyExZ3:

  1. Download and extract the contents of the PyExZ3 zipball to PyExZ3\.
  2. Download the Z3 release and extract the binaries in z3-4.6.0-x86-win.zip\z3-4.6.0-x86-win\bin\ to PyExZ3\.
  3. Also place the z3 folder (z3-4.6.0-x86-win.zip\z3-4.6.0-x86-win\bin\python\z3) in PyExZ3\.
  4. Place hevd_ioctl.py in PyExZ3\ and run pyexz3.py hevd_ioctl.py.
  5. Optional: Modify the _recordInputs() method in PyExZ3\symbolic\explore.py to 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.

Open to thoughts and feedback as always! Thank you to Thomas Ball (PyExZ3) and Ashfaq Ansari (HEVD) for their contributions.