About Me

I am a cryptography analyst at Trail of Bits.

Previously, I was an Invited Assistant Professor at the Department of Informatics of the Faculty of Sciences, University of Lisbon.

I have a PhD in Information Security from IST, Universidade de Lisboa. In my thesis, I studied conditions that allow the combination of satisfiability solvers, as well as probabilistic logics and their satisfiability procedures.

Interests

I am interested in cryptography, vulnerability research, logic, automated reasoning and type theory.

I have played CTF’s since 2014 with STT.

Vulnerability Research

• I participated in the EU-FOSSA program and audited PuTTY, an SSH client. I found a critical vulnerability which allowed to MITM SSH sessions, and an out-of-bounds write during the RSA key exchange:
  • DSA signature bypass allows to MITM SSH sessions: More details here.
  • CVE-2019-9894: Integer overflow to OOB write during RSA key exchange. More details here.

Blogposts

(2021) Disclosing Shamir’s Secret Sharing vulnerabilities and announcing ZKDocs.

(2018) GSoC 2018 Final: Debugging and Emulation Support for Cutter: how I implemented debugging in Cutter for my Google Summer of Code.

Publications

• F. Casal, A. Mordido, V. T. Vasconcelos. Mixed sessions. Theor. Comput. Sci. (2022)
• F. Casal, A. Mordido, V. T. Vasconcelos. Mixed Sessions: the Other Side of the Tape. PLACES@ETAPS 20200 (2020)
• V. T. Vasconcelos, F. Casal, B. Almeida, A. Mordido. Mixed Sessions. ESOP 2020 (2020)
• C. Caleiro, F. Casal, A. Mordido. Generalized probabilistic satisfiability and applications to modelling attackers with side-channel capabilities. Theor. Comput. Sci. (2019)
• F. Casal, J. Rasga, A. Souto. Kolmogorov One-Way Functions Revisited. Cryptography (2018)
• F. Casal, J. Rasga. Many-Sorted Equivalence of Shiny and Strongly Polite Theories. J. Autom. Reason. (2018)
• C. Caleiro, F. Casal, A. Mordido. Classical Generalized Probabilistic Satisfiability. IJCAI-26 (2017)
• C. Caleiro, F. Casal, A. Mordido. Generalized Probabilistic Satisfiability. LSFA 2016 (2016)
• F. Casal, J. Rasga. Revisiting the Equivalence of Shininess and Politeness. LPAR-19 (2013)
• F. Casal, A. P. Aguiar and J. M. Lemos. Multiple-model adaptive state estimation of the HIV-1 infection using a moving horizon approach. European Control Conference (2013)

Theses

• Combining Satisfiability Procedures and Probabilistic Satisfiability, PhD in Information Security, 2018. Advised by João Rasga @ IST, Universidade de Lisboa
• On Nelson-Oppen Techniques, MSc in Mathematics and Applications, 2013. Advised by João Rasga @ IST, Universidade de Lisboa.
• Gröbner Basis and Applications, BSc in Applied Mathematics and Computation, 2010. (in portuguese) Advised by Margarida Mendes Lopes @ IST.