Portrait of Luís Ferreirinha

Luís Ferreirinha

PhD Student at PLSec, Vrije Universiteit Amsterdam

I build type systems for assembly and prove binaries safe in zero-knowledge.

About

Hello! I am a PhD Student at the PLSec group at Vrije Universiteit Amsterdam, currently advised by Klaus von Gleissenthall. My research focuses on formal verification and security, with a particular interest in assembly language and type systems.

I am currently working on a project that aims to bring zero-knowledge proofs to the world of binaries: providing type-checking proofs for typed binaries in zero-knowledge via zkSNARK proofs, enabling safety proofs for proprietary applications that are easy and fast to verify.

Research topics: Formal Verification, Model Checking, Type Systems, Binary Analysis, Zero-Knowledge Proofs, Vulnerability Detection, Binary Patching

Languages: Rust, Haskell, Python, C

Publications

  • 2026

    BASICS: Binary Analysis and Stack Integrity Checker System for buffer overflow mitigation

    Luís Ferreirinha, Ibéria Medeiros

    Computers & Security, journal

  • 2025

    zkTAL: Type Checking Assembly in Zero-Knowledge

    Luís Ferreirinha, Klaus v. Gleissenthall

    CompSys 2025, short paper

  • 2024

    On the Path to Buffer Overflow Detection by Model Checking the Stack of Binary Programs

    Luís Ferreirinha, Ibéria Medeiros

    ENASE 2024, conference

News

  • 2026

    BASICS published in Computers & Security.

  • 2025

    Presented zkTAL at CompSys 2025, Utrecht.

  • 2024

    Started my PhD at VU Amsterdam.

Posts

Education

  • 2024

    MSc Informatics, University of Lisbon

    Thesis: Removal of Vulnerabilities in Binary Code by Program Model Checking and Concolic Execution PDF

  • 2022

    BSc Physics, University of Lisbon

    Minor in Informatics