Publications

In this paper, we present Prosecutor, a new fault localization technique that combines Bayesian reasoning with counterfactual execution analysis to effectively identify faults at the statement level.

We introduce SemQL, a query language that enhances traditional program analysis tool CodeQL with an oracle invocation construct, which allows the analyzer to call external oracles like LLMs to handle tasks requiring semantic reasoning beyond syntax. While existing program analysis tools excel at analyzing code structure, they struggle with analyses requiring semantic/subjective judgments, e.g., detecting string literals in code which expose sensitive information. SemQL bridges this gap by allowing queries to combine structural analysis with LLM-based judgments. We also propose an efficient query evaluation method that reduces the cost of using the LLM, and demonstrate the system usefulness on real-world code analysis problems.

Besides failure-triggering statements, failing tests often execute portions of code unrelated to the underlying defect, introducing noise and misleading information that hinder effective fault diagnosis. Test case minimization is therefore a critical step in the debugging process. We propose a slicing-based approach to address this problem. Our technique employs a novel data-flow analysis that leverages coding conventions to efficiently approximate the behavior of callee procedures without requiring access to their implementations. This enables us to initially derive a compact version of the test. If the minimized test fails to pass the verification step and trigger the original failure, a more conservative slicing approach is adopted on demand.

WebAssembly (Wasm) is a binary format designed for executing performance-critical code in web browsers. A key objective of Wasm is to facilitate the integration of legacy codebases and libraries into web applications without requiring developers to rewrite them in JavaScript from scratch. In practice, however, this objective is constrained by limitations in currently available WebAssembly compilers. In this paper, we investigate (1) the challenges that arise when cross-compiling high-level language codebases to WebAssembly, and (2) the extent to which WebAssembly compilers faithfully preserve program semantics in the resulting binaries. We also present WasmChecker, a differential testing framework for checking semantic equivalence between x86-64 binaries of C/C++ programs and their corresponding Wasm counterparts.

Upcoming cellular networks aim to enhance the efficiency and flexibility of mobile systems by incorporating technologies such as Software-Defined Networking (SDN), Network Function Virtualization (NFV), and Network Slicing (NS). Several open-source projects provide implementations of components across different cellular generations. In this paper, we leverage these projects to build a flexible and extensible testbed for experimenting with next-generation cellular networks.

We extend our prior work (published in TAP’22) and introduce static specifications for four common memory corruption vulnerabilities, i.e., heap-based buffer overflow, stack-based buffer overflow, use-after-free, and double-free. Leveraging these specifications, we identify relevant test units within x86-64 executable binaries which may contain such vulnerabilities. We then apply our unit-based symbolic execution approach to generate unit-level inputs which trigger these vulnerabilities and their corresponding system-level inputs.

We propose a novel method for discovering vulnerabilities in executable code. Our approach restricts the scope of symbolic execution to a set of statically identified test units, enabling efficient computation of path and vulnerability constraints within these units. By solving these constraints using an SMT solver, we generate inputs that trigger the vulnerability in the targeted test unit. We then approximate the relationship between global system inputs and unit-level inputs by using curve fitting. Given the derived unit inputs, we subsequently compute corresponding system-level inputs which trigger a heap overflow.