Assertion Labs Research

Program Analysis & Formal Methods

Research at the intersection of static analysis, formal verification, and systems security. Work published at IEEE, ASPLOS, ICSE, and DSN. Affiliated with Northeastern University and IMDEA Software Institute.

Research areas

WebAssembly Security
Binary-level analysis of WASM modules — semantic fragility detection, memory protection, vulnerability classification, and symbolic execution.
Abstract Interpretation
Static analysis via abstract domains for reasoning about program properties without execution. Applied to compiled binaries and bytecode.
Formal Verification
Machine-checked proofs of software correctness using Coq, Why3, and Rosette. Contract synthesis and specification inference.
Differential Privacy
Formal privacy guarantees for data-releasing mechanisms, with applications to secure multiparty computation.
Program Synthesis
Automated generation of programs from specifications, with prior work on contract synthesis using solver-aided languages.
AI-Assisted Code Analysis
Formal validation layers for LLM-generated code transformations — where AI tooling can and cannot self-certify correctness.

Publications

SANER 2023 · IEEE
SOLDER: Retrofitting Legacy Code with Cross-Language Patches
IEEE →

Framework for patching legacy C/C++ codebases by replacing vulnerable functions with memory-safe Rust equivalents, operating on LLVM bitcode with data-flow analysis and symbolic execution validation.

Rust Program Analysis Security LLVM
ASPLOS (target)
Proteus: Semantic Fragility Analysis for WebAssembly

Abstract interpretation framework for detecting semantic fragility in WebAssembly binaries. Analyzes how small perturbations in WASM modules affect observable program behavior.

WebAssembly Abstract Interpretation Formal Methods
ICSE (submission)
WASM-V: A Multi-Source WebAssembly Vulnerability Dataset

Comprehensive dataset of WebAssembly vulnerabilities aggregated from multiple sources, enabling systematic security analysis and benchmarking of WASM analysis tools.

WebAssembly Datasets Security
Conference paper
WASP: Symbolic Execution for WebAssembly Security

Symbolic execution pipeline targeting WebAssembly binaries using the Owi framework, enabling automated vulnerability detection and property verification.

Symbolic Execution WebAssembly Verification
DSN (target)
Sentinel: Memory Protection for WebAssembly

Runtime memory protection system for WebAssembly execution environments, providing fine-grained isolation guarantees beyond the standard WASM sandboxing model.

WebAssembly Memory Safety Runtime

Affiliations

Northeastern University
PhD, Computer Science · 2025
Dissertation: WebAssembly security analysis and formal program verification
IMDEA Software Institute
Research Affiliate · Madrid
Collaboration on formal methods and program analysis
Amazon Web Services
Senior Security Engineer
Authentication and authorization infrastructure at cloud scale