Formal Security Logo

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.

Formal Verification Web Security Program Analysis SMT Solving

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.

OCaml Formal Methods SMT Solver
Repository Learn More
graphjs

An MDG-based static vulnerability scanner for npm packages, detecting taint-style and prototype pollution vulnerabilities.

Security JavaScript Static Analysis
Repository Learn More
owi

A symbolic execution engine for WebAssembly (superseded wasp). Developed by OCamlPro.

WebAssembly Symbolic Execution OCaml
Repository Learn More
wasp

A symbolic execution engine for WebAssembly, providing a framework for testing and verifying Wasm modules.

WebAssembly Symbolic Execution Testing
Repository
ocaml-cvc5

OCaml bindings for the cvc5 SMT solver, allowing easy integration of cvc5 into OCaml projects.

OCaml SMT cvc5
Repository
explode-js

Automated exploit generation for Node.js packages based on static analysis findings.

Security Exploit Generation Node.js
Repository
whilloc

A simple 'while'-like programming language with memory allocation support, used for educational and research purposes.

PL Formal Verification
Repository

Our Team

José Santos
José Santos

Principal Investigator / Researcher

@j3fsantos Website
André Nascimento
André Nascimento

PhD Student

@andreffnascimento Website
Filipe Marques
Filipe Marques

PhD Student

@filipeom Website
Frederico Ramos
Frederico Ramos

PhD Student

@frediramos Website
João Pereira
João Pereira

PhD Student

@joaomhmpereira Website
José Afonso
José Afonso

PhD Student

@zezeafonso
Rafael Gonçalves
Rafael Gonçalves

PhD Student

@rafa1906 Website

Selected Publications

Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml

João Madeira Pereira, Filipe Marques, Pedro Adão, and Hichem Rami Ait El Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Petar Maksimović, Nuno Santos, José Fragoso Santos

TACAS'26 Paper
Specification-Driven Generation of Summaries for Symbolic Execution

Rafael Gonçalves, Frederico Ramos, Pedro Adão, José Fragoso Santos

ESOP'26 Paper
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 Paper
Toward Tool-Independent Summaries for Symbolic Execution

Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos

ECOOP'23 Paper
Concolic Execution for WebAssembly

Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão

ECOOP'22 Paper

Contact & Location

We are part of INESC-ID and the Instituto Superior Técnico (IST) at the University of Lisbon.

INESC-ID Lisboa
Rua Alves Redol 9
1000-029 Lisboa, Portugal

formalsec@example.com

Find us in Lisbon

Our research takes place in the heart of Portugal's capital.

View on Maps