Software systems remain vulnerable because developers inevitably make mistakes in their code. These bugs can often be triggered in ways that leave software in an exploitable state rather than simply causing a crash. As the number and complexity of vulnerabilities continue to rise, it becomes essential to develop systems that can automatically detect and mitigate them across different layers of the software stack.
Our research has introduced a suite of tools aimed at addressing this challenge. Talos provides runtime workarounds that neutralize vulnerabilities before they are patched, while Senx automatically generates source-level patches competitive with those written by developers. LMP leverages recent Intel hardware to defend against memory corruption attacks. Easier enables vulnerability detection in Android device drivers without requiring physical hardware, and Emila identifies Iago attacks in legacy code within trusted execution environments like SGX. On the distributed systems front, Consistency Oracles and Caelus work to detect attacks and logic errors in replicated systems. 
Building on this foundation, our recent work enhanced our ability to detect vulnerabilities earlier and more precisely. FLUX targets compiler bugs by constructing novel LLVM IR test cases through crossover mutations of high-coverage unit tests. Unlike traditional fuzzers, FLUX focuses on compiler optimizations, revealing 28 previously unknown bugs in LLVM—6 of which were patched.
EvoCrawl improves the security of web applications by using evolutionary search to explore sequences of user interactions that can lead to hidden server-side states and vulnerabilities. EvoCrawl exceeds the capabilities of traditional crawlers by modeling dependencies between elements and selectively filling form inputs. It achieved 59% higher code coverage and discovered eight zero-day vulnerabilities (IDOR and XSS) in widely used platforms such as WordPress and GitLab.
Modulo systematically uncovers convergence failure bugs in distributed systems. Through the use of Divergence Resync Models (DRMs), Modulo explores how systems respond to replica divergence and failure recovery. It found 11 critical bugs in ZooKeeper, MongoDB, and Redis—including 6 previously unknown ones—by triggering edge cases in the systems’ convergence logic.
Our CAR system improves targeted execution in Android applications by approximating and refining execution contexts for sensitive paths. Rather than trading off soundness or coverage, CAR leverages static constraint analysis and dynamic error recovery to reach paths that would otherwise be infeasible to analyze soundly. In our evaluation, CAR reached 3.1× more target locations than prior work, with a false-positive rate of just 9%.
We also explore how machine learning can accelerate symbolic execution by predicting path satisfiability. Through a new simulation framework, we studied the impact of predictor accuracy, path cost distributions, and tool design across two domains: Android applications (TIRO) and smart contracts (Mythril). Our findings show that effective integration of predictors, especially via prioritization strategies rather than strict filtering, can significantly reduce analysis time without sacrificing coverage.
Related Software Projects
- Talos
- Ocasta
- FLUX
- EvoCrawl
- Exploring Strategies for Guiding Symbolic Analysis with Machine Learning Prediction