Formal Security for Web Technologies
We use Formal Methods to enhance the security and reliability of modern web technologies. Our research focuses on Static Analysis, Symbolic Execution, and Automated Exploit Generation for languages like JavaScript and WebAssembly.
Research Projects
We develop open-source tools to solve real-world security challenges.
smtml
An SMT solver frontend for OCaml, providing a unified interface for multiple solvers.
graphjs
An MDG-based static vulnerability scanner for npm packages, detecting taint-style and prototype pollution vulnerabilities.
owi
A symbolic execution engine for WebAssembly (superseded wasp). Developed by OCamlPro.
wasp
A symbolic execution engine for WebAssembly, providing a framework for testing and verifying Wasm modules.
ocaml-cvc5
OCaml bindings for the cvc5 SMT solver, allowing easy integration of cvc5 into OCaml projects.
explode-js
Automated exploit generation for Node.js packages based on static analysis findings.
whilloc
A simple 'while'-like programming language with memory allocation support, used for educational and research purposes.
Our Team
Selected Publications
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
Mafalda Ferreira, Miguel Monteiro, Tiago Brito, Miguel E. Coimbra, Nuno Santos, Limin Jia, and José Fragoso Santos
PLDI'24 PaperContact & Location
We are part of INESC-ID and the Instituto Superior Técnico (IST) at the University of Lisbon.
INESC-ID LisboaRua Alves Redol 9
1000-029 Lisboa, Portugal