Current Projects
Program Analysis for WebAssembly Binaries
Northeastern University
Research into program analysis techniques specifically designed for WebAssembly runtime environments, focusing on security analysis and vulnerability detection in WASM modules.
Synthesizing Microarchitectural Leakage Contracts from Counterexamples
IMDEA Software Institute
Developing techniques to automatically synthesize contracts that capture microarchitectural side-channel vulnerabilities, with applications to secure software verification.
Other Projects
Quantitative Analysis & Interactive Notebooks
Collection of notebooks, code, and tools for quantitative finance, forecasting, and analytics. Features interactive Pluto and Jupyter notebooks with Julia and Python implementations for statistical modeling and data analysis.
Beyond the Kernel: High-Performance Networking
Blog series exploring Rust’s capabilities in high-performance networking, kernel bypass techniques, and inline assembly for low-latency systems. Covers DPDK, XDP, RDMA, and other kernel bypass technologies.
Foundations of Coq
Pollen-based e-book
Comprehensive guide to the Coq proof assistant, covering fundamental concepts, tactics, and advanced proof techniques. Built using the Pollen publishing system for interactive documentation.
Open Source Contributions
- PatchCanary: Early warning system for patch regressions
- Solder: Cross-language patching framework
- Holepunch: Secure file deletion with crash consistency
Tools & Frameworks
Various security analysis tools and frameworks developed as part of research projects. See individual project pages for more details and source code availability.