Using Symbolic Execution to Recover IOCTLs in HEVD

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 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 (Python Exploration with Z3)
Exploring hevd_ioctl.hevd_ioctl
[('ioctl', '0x22201f')]
[('ioctl', '0x222003')]
[('ioctl', '0x222007')]
[('ioctl', '0x22200b')]
[('ioctl', '0x22200f')]
[('ioctl', '0x222013')]
[('ioctl', '0x222017')]
[('ioctl', '0x22201b')]
[('ioctl', '0x222023')]
[('ioctl', '0x222027')]
[('ioctl', '0x22202b')]
[('ioctl', '0x22202f')]
[('ioctl', '0x222033')]
[('ioctl', '0x222037')]
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\bin\ to PyExZ3\.
  3. Also place the z3 folder (\z3-4.6.0-x86-win\bin\python\z3) in PyExZ3\.
  4. Place in PyExZ3\ and run
  5. Optional: Modify the _recordInputs() method in PyExZ3\symbolic\ 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.