QueryX: Symbolic Query on Decompiled Code for Finding Bugs in COTS Binaries

### Overview In this presentation, Iyoung Sang Kang from Georgia Tech introduces QueryX, an extensible static checking tool that supports symbolic queries directly on decompiled code to discover vulnerabilities in commercial off-the-shelf (COTS) binaries. The research, conducted during Kang's PhD alongside colleagues Insu Yun and Taesoo Kim, tackles the scalability and accuracy trade-offs inherent in binary static analysis.

While extensible static analysis tools like CodeQL and Joern allow human analysts to write source-level queries, feeding decompiled code into them results in high false positive rates and missed bugs because source analyzers are unaware of underlying binary specifics (e.g., memory layout and data sections). Conversely, binary tools like angr and BAP rely on low-level binary intermediate representations (IR), which lack high-level abstractions like types and control flow, making queries complex and tedious to write. QueryX bridges this gap by enabling analysts to write high-level, analyst-friendly symbolic queries on decompiled code while remaining binary-aware.

### Key Topics - **Limitations of Source and Binary Checkers**: Source-code query engines fed with decompiled code fail due to binary-unaware semantics like memory layouts and missing data sections. Binary IR tools (like angr) force analysts to deal with low-level details, resulting in verbose query code. - **Decompiler Neutral Representation (DNR)**: QueryX introduces a new intermediate representation, DNR, to retain high-level decompiled code structures while injecting critical binary details, such as stack memory layouts and binary-embedded data sections. - **Analyst-Friendly Symbolic Queries**: QueryX allows queries to be written using JavaScript syntax against decompiled code ASTs. Analysts can register execution callbacks on specific function calls (e.g., `malloc`, `memcpy`) to inspect symbolic states. - **Real-World Bug Hunting in Windows Kernel**: Applying QueryX to the Windows kernel uncovered multiple zero-day vulnerabilities, including integer overflows that lead to heap buffer overflows.

### Technical Details QueryX operates across four primary modules: 1. **Decompiler Module**: Takes target binaries and generates decompiled code (using Hex-Rays). 2. **Lifter Module**: Translates the decompiled code into DNR by calculating stack memory layouts, lifting stack variable accesses, and resolving global variable reads using a dedicated program data section that holds initial binary values and permissions. 3. **Query Interpreter**: Executes analyst queries written in JavaScript syntax, mapping query logic to decompiled AST nodes without forcing analysts to write queries against DNR directly. 4. **Analyzer Module**: Runs symbolic execution from function entry points, traversing AST nodes and firing registered callbacks (such as `collect_alloc` and `check_memcpy`). Callbacks read AST node values from the symbolic state and query the Z3 solver under current path constraints to detect issues like heap overflows.

In an evaluation comparing query complexity for a Windows kernel heap overflow caused by a 2-byte integer overflow, angr required 267 lines of code, whereas QueryX required only 33 lines due to its access to high-level decompiled type information. QueryX also outperformed Joern and CodeQL on a benchmark dataset by achieving higher true positives with fewer false positives.

### Takeaways QueryX demonstrates that combining the high-level readability of decompiled code with binary-aware memory modeling yields practical, concise, and highly effective bug-finding queries. Applied to the Windows kernel across four query types, QueryX uncovered 15 new vulnerabilities (including 10 CVEs and 7 heap overflows), earning $180,000 in bug bounties. Future work noted during the Q&A includes further evaluating semantic equivalence between decompiled code and native binary code.