Pengfei Gao

Pengfei Gao

Ph.D. student on Formal Verification

ShanghaiTech University

Biography

Pengfei Gao is a fifth-year Ph.D. student at ShanghaiTech University under supervision of Prof. Fu Song. His research interests broadly involve program analysis and verification for correctness and security-driven concerns. He has focued on developing new techniques to formally verify side-channel resistance of cryptographic algorithms and design secure and efficient masked implementations against side-channel attacks. He is also interested in software testing, e.g. how to automatically find bugs in software or further improve the code coverage.

Outside of Lab, he likes going to the gym and DIY electronic projects.

Email: $$ ((x \to (y \to xy@shanghaitech.edu.cn))(gao))(pf)$$

Download my resumé.

Interests
  • Program Verification
  • Static Program Analysis
  • Software Testing
Education
  • PhD in Computer Science, 2023

    ShanghaiTech University

  • BSc in Computer Science, 2017

    China University of Mining and Technology

News

  • Jan 2022. 🙋‍♂️🙋‍♂️I am on the job market now!
  • Dec 2021. Attend CCF Chinasoft 2021 online and give a talk at Excellent Doctoral Student Forum.
  • Feb 2021. Our paper “A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs.” is accepted by ACM TOSEM 2021.
  • Nov 2020. Attend CCF Chinasoft 2020 at Chongqing, China.
  • Jul 2020. Our paper “Formal Verification of Masking Countermeasures for Arithmetic Programs” is accepted by IEEE TSE 2020.
  • Jul 2019. Attend ISSTA 2019 and serve as a student volunteer at Beijing, China.
  • Apr 2019. Our paper “Verifying and Quantifying Side-channel Resistance of Masked Software Implementations” is accepted by ACM TOSEM 2019.
  • Apr 2019. Attend ETAPS 2019 and serve as a student volunteer at Prague, Czech.
  • Jan 2019. Our paper “Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks” is accepted by TACAS 2019 / ETAPS 2019.
  • Nov 2018. Attend FMAC 2018 and give a talk at Chongqing, China.
  • Jul 2018. Attend CAV 2018 at Oxford, UK.
  • Apr 2018. Our paper “SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks” is accepted by CAV 2018.
  • Nov 2017. Attend ICFEM 2017 at Xi’an, China.

Recent Publications

(2021). A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs. In ACM TOSEM 2021.

PDF

(2020). Formal Verification of Masking Countermeasures for Arithmetic Programs. In IEEE TSE 2020.

PDF

(2019). Verifying and Quantifying Side-channel Resistance of Masked Software Implementations. In ACM TOSEM 2019.

PDF

(2019). Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks. In the proceedings of TACAS 2019 (ETAPS 2019).

PDF

(2019). Model-based Automated Testing of JavaScript Web Applications via Longer Test Sequences. In Frontiers of Computer Science 2022.

PDF

(2018). SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks. In the proceedings of CAV 2018.

PDF

Service

  • Student Volunteer: ETAPS'19@Prague, ISSTA'19@Beijing
  • Sub-reviewer: CAV'21, IEEE TSE

Awards

Scholarship

  • Baosteel Excellent Student Scholarship (2021)
  • National Scholarship for Graduates (2020)
  • CSC-IBM Excellent Chinese Student (2019)
  • ETAPS Scholarship (2019)
  • FLoC Travel Grant (2018)

Honours

  • Merit Student at ShanghaiTech (2021)
  • Merit Student at ShanghaiTech (2020)
  • Excellent Student at ShanghaiTech (2019)
  • Excellent Graduate of CUMT (2017)
  • Excellent Graduation Thesis from CUMT (Topic: Static Memory Leak Detection of Rust Programs) (2017)