PyExZ3 Example with HackSysExtremeVulnerableDriver
TL;DR: Using symbolic execution to recover driver IOCTL codes that are computed at runtime.
The goal here is to find valid IOCTL codes for the HackSysExtremeVulnerableDriver by analyzing 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 `ex