Education

• Universidad Politécnica de Madrid, PhD in Formal Methods, 2026 (expected)
• Universidad Autónoma de Madrid, M. Eng. in Formal Methods, 2020
• University of Science and Technology of China, M.Sc. in Cryptography, 2020
• University of Science and Technology of China, B.S. in Information Security, 2013

Research Experience

• IMDEA Software Instritute
  • 2020.09-Present
  • Research Assistant
  • Applied formal methods to verify security at the hardware–software boundary. On a very high level, I formalize the security guarantee of processors with hardware-software contracts at register transfer level (RTL). On software side, programmers write secure programs according to the contract. On hardware side, we prove the contract satisfaction w.r.t the contract, processor and the attacker.
  • Developed a tool called ‘LeaVe’ to verify contract satisfaction. We developed a Houdini-style invariant learning algorithm and implemented it in ‘LeaVe’. For a given contract, hardware and attacker, ‘LeaVe’ can unboundly check the contract satisfaction.
  • Developed a tool called ‘LeaSyn’ to synthesize sound and precise leakage contracts. For a given processor implemented at RTL, ‘LeaSyn’ synthesizes a sound and precise leakage contract w.r.t the attacker. Here, ‘Sound’ means that all leaks at hardware level are captured while ‘precise’ means only actual leaks are exposed.
• Universidad Autónoma de Madrid
  • 2019.09-2020.09
  • Postgraduate Researcher
  • Coded a demo system for static interval analysis with Python
  • Researched the inductive logic programming approaches, and designed an explainable deep learning system for biometrics
  • Mastered the basic machine learning algorithms and TensorFlow
• University of Science and Technology of China
  • 2013.06-2020.06
  • Research Assistant
  • Analyzed the security of RSA under the lattice cryptoanalysis
  • Designed a lattice-base authenticated key exchange protocol, provided the provable security, and implemented it with python
  • Designed a lattice-base password-based authenticated key exchange protocol and provided the provable security
• Institute of Software, Chinese Academy of Sciences
  • 2014.06-2015.09
  • Intern
  • Participated in the project of creating a cryptanalysis platform
  • Coded and tested the “security level of S-box” module of the platform
• Institute of Software, Chinese Academy of Sciences
  • 2013.01-2013.06
  • Intern
  • Analyzed the encryption methods of Word and PDF documents
  • Developed a platform with C# cracking PDF documents with an improved dictionary attack
• Institute of Information Engineering, Chinese Academy of Sciences
  • 2012.06-2012.09
  • Summer Undergraduate Researcher
  • Improved and implemented the algorithm for attacking the WEP protocol
  • Developed a program to recover the password of wireless networks