???global.info.a_carregar???
The main goal of my research is the verification, specification, and testing of JavaScript applications with a particular focus on client-side Web applications that interact with the DOM API. I am primarily interested in the enforcement of security properties (such as secure information flow) and the automated verification of functional correctness properties of critical JavaScript code. To achieve these goals, I make use of program analyses and instrumentation techniques well established for static languages, advancing them to the setting of a highly complex, dynamic language, such as JavaScript. My research goes from theory to practice delivering industrial-strength tools that enable JavaScript programmers to better test, verify, and understand their code. As JavaScript is the key element of the internet of today, these tools can significantly impact the quality of current web applications, potentially improving the experience of users on a global scale.
Read full resume ↓
Identification

Personal identification

Full name
José Fragoso Santos

Citation names

  • José Fragoso Santos

Author identifiers

Ciência ID
1319-F56C-0E1E
ORCID iD
0000-0001-5077-300X

Knowledge fields

  • Ciências Exatas - Ciências da Computação e da Informação

Languages

Language Speaking Reading Writing Listening Peer-review
Francês Utilizador independente (B2) Utilizador independente (B2) Utilizador independente (B2) Utilizador independente (B2)
Inglês Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador proficiente (C1)
Education
Degree Classification
2014
Concluído
 Doctorat en Informatique (Doutoramento)
Université de Nice Sophia Antipolis, França
"Enforcing Secure Information Flow in Client-Side Web Applications" (THESIS/DISSERTATION)
 Mention Très Honorable
2008
Concluído
 Mestrado em Engenharia Informática e de Computadores (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
"Learning Techniques: From SAT to Pseudo-Boolean Optimization" (THESIS/DISSERTATION)
 18
2006
Concluído
 Licenciatura em Ciências da Engenharia Informática e de Computadores (Licenciatura)
Universidade de Lisboa Instituto Superior Técnico, Portugal
"Learning Techniques: From SAT to Pseudo-Boolean Optimization" (THESIS/DISSERTATION)
 16
Affiliation

Ciência

Category
Host institution 		Employer
2019/09/01 - Current Investigador (Investigação) Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
2015/03/01 - 2019/08/31 Pós-doutorado (Investigação) Imperial College London, Reino Unido
2009/08/01 - 2010/08/01 Estagiário de Investigação (Investigação) Instituto de Telecomunicações, Portugal
2009/01/01 - 2009/06/30 Estagiário de Investigação (Investigação) Laboratório de Robótica e Sistemas de Engenharia, Portugal
2007/10/01 - 2008/10/31 Estagiário de Investigação (Investigação) Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal

Docência no Ensino Superior

Category
Host institution 		Employer
2019/09/01 - Current Professor Auxiliar (Docente Universitário) Universidade de Lisboa Instituto Superior Técnico, Portugal
Projects

Projeto

Designation Funders
2021/01/01 - 2025/12/31 Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa
LA/P/0078/2020
10.54499/LA/P/0078/2020
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
 Fundação para a Ciência e a Tecnologia
Em curso
2024/03/01 - 2025/02/28 WebCAP: Web Data Collection via Automated Program Synthesis
2024.07393.IACDC
Investigador responsável
2022/03/27 - 2023/06/26 DIVINA: Detecting Injection Vulnerabilities In Node.js Applications
CMU/TIC/0053/2021
Investigador responsável
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
Concluído
2020/01/01 - 2022/12/31 LAIfeBlood - Inteligência Artificial para a Gestão do Sangue
DSAIPA/AI/0033/2019
Associação do Instituto Superior Técnico para a Investigação e Desenvolvimento, Portugal

Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
Fundação para a Ciência e a Tecnologia
Em curso
2020/09/30 - 2022/09/30 INFOCOS: Intelligent Feedback for Content Students
PTDC/CCI-COM/32378/2017
Investigador responsável
Concluído
2019/01/01 - 2021/12/31 Data2Help: Ciência de Dados para Optimização de Serviços de Emergência Médica
DSAIPA/AI/0044/2018
Instituto Nacional de Emergência Médica IP, Portugal

Associação do Instituto Superior Técnico para a Investigação e Desenvolvimento, Portugal

Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
Fundação para a Ciência e a Tecnologia
Em curso
2017/01/01 - 2019/08/31 REMS: Rigorous Engineering for Mainstream Systems
EP/K008528/1
Investigador
2013/09/30 - 2016/12 Certified Verification of Client-Side Web Programs
EP/K032089/1
 UK Research and Innovation
2009/08/01 - 2010/08/01 KLog - Logics for Security
PTDC/MAT/68723/2006
Bolseiro de Mestrado
2009/01/01 - 2009/07/31 BIO-LOOK - Biomimetic Oculomotor Control for Humanoid Robots
PTDC/EEA-ACR/71032/2006
2007/09/01 - 2008/09/01 BSOLO - Boolean constraint SOLving and Optimization
PTDC/EIA/76572/2006
Bolseiro de Iniciação Científica
Outputs

Publicações

Artigo em conferência
  1. Mafalda Ferreira; Miguel Monteiro; Tiago Brito; Miguel Coimbra; Nuno Santos; Limin Jia; José Fragoso Santos. "Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs". Paper presented in Programming Language Design and Implementation (PLDI), 2024.
  2. Ramos, Frederico; Reis, Diogo Costa; Trigo, Miguel; Morgado, António; Fragoso Santos, José. "MetaData262: Automatic Test Suite Selection for Partial JavaScript Implementations". Paper presented in ACM SIGSOFT International Symposium on Software Testing and Analysis, 2023.
    10.1145/3597926.3604923
  3. Almeida, Luís; Gonzaga, Miguel; Santos, José Fragoso; Abreu, Rui. "Rexstepper: a Reference Debugger for JavaScript Regular Expressions". Paper presented in 2023 IEEE/ACM 45th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 2023.
    10.1109/icse-companion58688.2023.00021
  4. Ferreira, Mafalda; Brito, Tiago; Santos, José Fragoso; Santos, Nuno. "RuleKeeper: GDPR-Aware Personal Data Compliance for Web Frameworks". Paper presented in 2023 IEEE Symposium on Security and Privacy (SP), 2023.
    10.1109/sp46215.2023.10179395
  5. Frederico Ramos; Nuno Sabino; Pedro Adão; David A. Naumann; José Fragoso Santos. "Toward Tool-Independent Summaries for Symbolic Execution". Paper presented in European Conference on Object-Oriented Programming (ECOOP), 2023.
    Publicado • 10.4230/LIPICS.ECOOP.2023.24
  6. Filipe Marques; José Fragoso Santos; Nuno Santos; Pedro Adão. "Concolic Execution for WebAssembly". Paper presented in 36th European Conference on Object-Oriented Programming, ECOOP 2022, 2022.
    10.4230/LIPICS.ECOOP.2022.11
  7. Mikolas Janota; Manquinho, Vasco; José Fragoso Santos; António Morgado. "The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets". Paper presented in 27th International Conference on Principles and Practice of Constraint Programming (CP'21), 2021.
    10.4230/LIPICS.CP.2021.31
  8. Petar Maksimovic; Sacha Elie Ayoun; José Fragoso Santos; Philippa Gardner. "Gillian, Part II: Real-World Verification for JavaScript and C". Paper presented in Computer Aided Verification-33rd International Conference, CAV, 2021.
    Aceite para publicação
  9. Geraldo, Eduardo; Santos, José Fragoso; Seco, João Costa. "Hybrid Information Flow Control for Low-Level Code". Paper presented in Software Engineering and Formal Methods (SEFM), 2021.
    10.1007/978-3-030-92124-8_9
  10. Gabriela Sampaio; José Fragoso Santos; Petar Maksimovic; Philippa Gardner. "A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications". Paper presented in European Conference on Object Oriented Programming (ECOOP), 2020.
  11. José Fragoso Santos; Petar Maksimovic; Sacha Elie Ayoun; Philippa Gardner. "Gillian, Part I: A Multi-language Platform for Symbolic Execution". Paper presented in Programming Language Design and Implementation (PLDI), London, 2020.
  12. Santos, José Fragoso; Maksimovic, Petar; Grohens, Théotime; Dolby, Julian; Gardner, Philippa. "Symbolic Execution for JavaScript". Paper presented in International Symposium on Principles and Practice of Declarative Programming (PPDP), 2018.
    10.1145/3236950.3236956
  13. Santos, José Fragoso; Gardner, Philippa; Maksimovic, Petar; Naudžiuniene, Daiva. "Towards Logic-Based Verification of JavaScript Programs". Paper presented in 26th International Conference on Automated Deduction (CADE), 2017.
    10.1007/978-3-319-63046-5_2
  14. Raad, Azalea; Santos, José Fragoso; Gardner, Philippa. "DOM: Specification and Client Reasoning". Paper presented in 14th Asian Symposium on Programming Languages and Systems (APLAS), 2016.
    10.1007/978-3-319-47958-3_21
  15. Fragoso Santos, José; Rezk, Tamara; Matos, Ana Almeida. "Modular Monitor Extensions for Information Flow Security in JavaScript". Paper presented in 10th International Symposium on Trustworthy Global Computing (TGC), 2015.
    10.1007/978-3-319-28766-9_4
  16. Fragoso Santos, José; Jensen, Thomas; Rezk, Tamara; Schmitt, Alan. "Hybrid Typing of Secure Information Flow in a JavaScript-Like Language". Paper presented in 10th International Symposium on Trustworthy Global Computing (TGC), 2015.
    10.1007/978-3-319-28766-9_5
  17. Almeida-Matos, Ana; Fragoso Santos, José; Rezk, Tamara. "An Information Flow Monitor for a Core of DOM". Paper presented in 9th International Symposium Trustworthy Global Computing, 2014.
    10.1007/978-3-662-45917-1_1
  18. Santos, José Fragoso; Rezk, Tamara. "An Information Flow Monitor-Inlining Compiler for Securing a Core of JavaScript". Paper presented in 29th IFIP International Conference on Systems Security and Privacy Protection (SEC), 2014.
    10.1007/978-3-642-55415-5_23
  19. Matos, Ana Almeida; Santos, José Fragoso. "Typing illegal information flows as program effects". Paper presented in 7th Workshop on Programming Languages and Analysis for Security (PLAS), 2012.
    10.1145/2336717.2336718
  20. Santos, Jose´; Bernardino, Alexandre; Santos-Victor, Jose´. "Sensor-based self-calibration of the iCub's head". Paper presented in 2010 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2010.
    10.1109/iros.2010.5651275
Artigo em revista
  1. Tiago Brito; Mafalda Ferreira; Miguel Monteiro; Pedro Lopes; Miguel Barros; Jose Fragoso Santos; Nuno Santos. "Study of JavaScript Static Analysis Tools for Vulnerability Detection in Node.js Packages". IEEE Transactions on Reliability (2023): http://dx.doi.org/10.1109/tr.2023.3286301.
    Open access • 10.1109/tr.2023.3286301
  2. Brito, Tiago; Lopes, Pedro; Santos, Nuno; Santos, José Fragoso. "Wasmati: An efficient static vulnerability scanner for WebAssembly". Computers & Security 118 (2022): 102745. https://doi.org/10.1016/j.cose.2022.102745.
    10.1016/j.cose.2022.102745
  3. Fragoso Santos, José; Maksimovic, Petar; Sampaio, Gabriela; Gardner, Philippa. "JaVerT 2.0: compositional symbolic execution for JavaScript". Proceedings of the ACM on Programming Languages (POPL'19) 3 POPL (2019): 1-31. https://doi.org/10.1145/3290379.
    10.1145/3290379
  4. Fragoso Santos, José; Maksimovic, Petar; Naudžiuniene, Daiva; Wood, Thomas; Gardner, Philippa. "JaVerT: JavaScript verification toolchain". Proceedings of the ACM on Programming Languages 2 POPL (2017): 1-33. https://doi.org/10.1145/3158138.
    10.1145/3158138
  5. Luo, Z.; Santos, J.F.; Matos, A.A.; Rezk, T.. "Mashic compiler: Mashup sandboxing based on inter-frame communication". Journal of Computer Security 24 1 (2016): 91-136. http://www.scopus.com/inward/record.url?eid=2-s2.0-84960408868&partnerID=MN8TOARS.
    10.3233/JCS-160542
Poster em conferência
  1. Ramos, Frederico; Filipe Marques; Pedro Miguel Adão; Nuno Santos; José Fragoso Santos. "Empirical Study on Applying Program Analysis and Testing Tools to Student Code". Paper presented in 3rd International KLEE Workshop on Symbolic Execution, 2022.
Activities

Orientação

Thesis Title
Role 		Degree Subject (Type)
Institution / Organization
2024/09/01 - 2029/08/31 LLM-based Vulnerability Detection for Node.js Applications
Coorientador of Rafael Gonçalves
 Computer Science and Engineering (Doutoramento)
Universidade de Lisboa Instituto Superior Técnico, Portugal

Carnegie Mellon University, Estados Unidos
2022/09/01 - 2026/09/30 A Symbolic Analysis for Detecting Injection Vulnerabilities in Node.js Applications
Orientador of Filipe Marques
 Computer Science and Engineering (Doutoramento)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/09/01 - 2026/09/30 Summary Synthesis for Symbolic Execution
Coorientador of Frederico Ramos
 Computer Science and Engineering (Doutoramento)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/09/01 - 2025/09/30 Multi-version Dependency Graphs for Vulnerability Detection and GDPR Conformance
Coorientador of Mafalda Ferreira
 Computer Science and Engineering (Doutoramento)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/25 A Sound and Efficient Symbolic Memory Model for JavaScript
Orientador of Juliana Yang
Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/15 Specifying Distributed Hash Tables with Allen’s Temporal Logic in Alloy
Orientador of Nuno Alexandre Marques Policarpo
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/12 Detecting Multi-file Vulnerabilities Using Code Property Graphs
Orientador of Guilherme Figueira da Silva Gonçalves
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/12 A Multi-Backend Frontend for SMT Solvers in OCaml
Orientador of João Maria Henriques Madeira Pereira
Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/11 Graph.js 2.0: Efficient and Trustworthy Code Property Graphs for JavaScript
Orientador of Tomás de Araújo Tavares
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/08 Two New Datasets for Understanding TypeScript Coding Patterns and Bugs
Orientador of António Pedro Gomes Coutinho Leopoldo Marques
Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/07 A New Language Server for the ECMAScript Specification Language
Orientador of Ricky Xu
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/06 ComplyQL: Towards Building GDPR Storage Compliant Applications
Coorientador of Cristi Savin
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/09/01 - 2024/11/05 Detect.ts: A Library for Detecting Unsafe TypeScript Coding Patterns
Orientador of Diogo Fernandes Afonso
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023/01/01 - 2024/06/19 Implementation-Based Generation of the ECMAScript Standard
Orientador of Patrícia Alexandra Ferreira Pereira
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2019/09/01 - 2024/05/31 Applying code property graphs on modern web languages for security and privacy analysis
Coorientador of Tiago Luís de Oliveira Brito
 Computer Science and Engineering (Doutoramento)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/09/01 - 2023/11/17 Specification-driven Synthesis of Summaries for Symbolic Execution
Orientador of Rafael Henriques dos Santos Gonçalves
Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/09/01 - 2023/11/14 A Typed Intermediate Language for Specifying the ECMAScript Standard
Orientador of André Filipe Ferreira do Nascimento
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/09/01 - 2023/11/10 Memory Models for Symbolic Execution of JavaScript Applications
Orientador of Manuel Marques Costa
Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/09/01 - 2023/11/10 An Efficient Memory Data Structure for Wasm Symbolic Execution
Orientador of André Alexandre Inácio Mendes
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/09/01 - 2023/11/09 ExplodeQ.js: A Library of Queries to Detect Injection Vulnerabilities in Node.js Applications
Orientador of Miguel Alexandre Figueiredo Monteiro
Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2021/09/01 - 2023/06/22 Classic Symbolic Execution of WebAssembly
Orientador of João Pedro Lopes Borges
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/01/01 - 2023/06/16 RexStepper 2.0: Interactive Debugging for Regular Expressions in the Browser
Orientador of Miguel Gonzaga Serra Victorino Correia da Silva
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2022/01/01 - 2023/06/15 Live Metadata for Test262
Orientador of Diogo Costa Reis
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2021/09/01 - 2023/06/12 ECMARef6: A Reference Interpreter For Modern JavaScript
Orientador of Rafael Rosa Rahal
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2021/09/01 - 2022/11/23 A Reference Implementation of ES6 Built-in Libraries
Orientador of Jorge Pedreira Cardoso Brown
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2021/01/20 - 2022/06/20 Infra-estrutura de Testes para Implementações de Referência do Standard ECMAScript
Orientador of Miguel Maria Marçalo Pires Trigo
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2017/09/01 - 2022/03/31 A Trusted Infrastructure for Symbolic Analysis of Event-based Web APIs
Coorientador of Gabriela Cunha Sampaio
 Computer Science (Doutoramento)
Imperial College London, Reino Unido
2020/09/01 - 2021/12/22 A Sound Type System for the Meta Language of the JavaScript Standard
Orientador of Pedro José Fernandes Nunes
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/09/01 - 2021/12/03 Robust Symbolic Execution for WebAssembly
Orientador of Filipe dos Santos Oliveira Marques
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/09/01 - 2021/11/24 A Reference Implementation of ECMAScript Built-in Objects
Orientador of David Manuel Sales Gonçalves
 Computer Science and Engineering
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/09/01 - 2021/11/23 Code-Stepping Regular Expressions in the Browser
Orientador of Luís Alberto Carvalho de Almeida
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/09/01 - 2021/11/23 Toward Tool-Independent Summaries for Symbolic Execution
Orientador of Frederico Duarte Ramos
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/01/01 - 2021/09/23 ECMA-SL - A Platform for Specifying and Running the ECMAScript Standard
Orientador of Luís Miguel Alves Loureiro
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/09/01 - 2021/09/22 Precise Information Flow Control for JavaScript
Orientador of Francisco João Do Vale Lopes e Silva Quinaz
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2019/09/01 - 2021/02/28 Discovering Security Vulnerabilities in WebAssembly with Code Property Graphs
Orientador of Pedro Daniel Rogeiro Lopes
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2019/09/01 - 2020/11/20 Concolic Execution for WebAssembly
Orientador of Carolina Silva Costa
 Computer Science and Engineering (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2018/09/01 - 2019/11/25 A JavaScript Information Flow Monitor for Symbolic Testing
Orientador of André Baptista Neves Ribeiro
 Telecommunications Engineering and Informatics (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
Distinctions

Prémio

2018 Research Award on Continuous Reasoning Research (USD 50K)
Facebook Inc, Estados Unidos