Shenghao YUAN Researcher, Zhejiang University Email: shenghao.yuan@inria.fr / nuaaysh@126.com Software: GitLab / GitHub https://orcid.org/0000-0002-8467-5827

---

[ Education ] [ Research ] [ Projects ] [ Publications ]

---

Education

• Undergraduate. Sept.2013 - Jun.2017, Software Engineering
  • College of Computer Science and Technology (CCST), Nanjing University of Aeronautics and Astronautics (NUAA), China
• Master. Sept.2017 - Apr.2020, Software Engineering (supervised by Prof. Zhibin Yang)
  • College of Computer Science and Technology (CCST), Nanjing University of Aeronautics and Astronautics (NUAA), China
• PhD. Sept.2020 - Dec.2023, Computer Science (Co-advisors: Jean-Pierre Talpin and Frédéric Besson)
  • The Time, Events and Architectures(TEA) team, Université de Rennes / Inria-Rennes, Franch

---

Research Interests

I am interested in theorem proving (Coq, Isabelle/HOL, and Lean4), compiler/OS formal verification. Especially, eBPF-related verification~

Current Research

• Compiler Verification (CompCert-related)
  • From Coq to C [CAV2022]
  • JIT (Just-In-Time) Compiler [CAV2024]
  • EVM AOT Compiler (TBC)
• OS/VM Verification
  • RIOT-OS rBPF VM [MIDDLEWARE2022], bootloader [MEMOCODE2021]
  • Solana Blockchain VM [OOPSLA2025]
  • Linux eBPF (WIP)
• Model-driven development
  • AADL / Synchronous Lanuage [SCP2021]

Action within Practice

Our research should make real-world software better: e.g. find issues, present soluations, and so on~

• Linux Patches
  • bpf: Reject negative offsets for ALU ops
  • bpf: Add range tracking for BPF_DIV and BPF_MOD and related selftests
  • (TBC)
• Solana Issues
  • assembler: register inconsistency
  • Interpreter LD_DW_IMM: add !sbpf_version.disable_lddw() checking
  • Cleanup - unused JIT-generated instruction
  • Feature - Expand X86Instruction::opcode field to to optimize multiplications

---

Projects

I join the TRust² project currently, working on formal verification of Rust. The Solana verification is a part of TRust²: the Solana eBPF VM is a real-world Rust case study.

• 2025-01 to 2025-12: End-to-end formal verification of Solana eBPF JIT Compiler. (Overivew) [2024CCF-Huawei Populus Grove Fund: Formal Method Track (News in Chinese)]

• 2026-01 to 2028-12: Mechanized Safety Proof of an eBPF Virtual Machine. National Science Foundation for Young Scientists of China

• 2025-xx to 2026-xx: Porting an eBPF JIT Compiler to RISC-V for Solana. Open Source Project for Solana [repo]

---

Selected Publications [DBLP] [Google Scholar] (* = corresponding author)

• OOPSLA2025: A complete formal semantics of eBPF instruction set architecture for Solana
  Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, Yongwang Zhao*
  In ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (CCF-A conf) [local copy]
• SETTA2024: Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness
  Jiayi Lu, Shenghao Yuan*, David Sanan, Yongwang Zhao
  In 10th Symposium on Dependable Software Engineering: Theories, Tools and Applications (CCF-C conf) [local copy]
• CAV2024: End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
  Shenghao Yuan*, Frédéric Besson, Jean-Pierre Talpin
  In 36th International Conference on Computer-Aided Verification (CCF-A conf) [local copy]
• SETTA2023: Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification
  Shenghao Yuan*, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin
  In 9th Symposium on Dependable Software Engineering: Theories, Tools and Applications (CCF-C conf) [local copy]
  (An invited extension to Journal of Systems Architecture, CCF-B journal)
  
• CAV2022: End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
  Shenghao Yuan*, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli
  In 34th International Conference on Computer-Aided Verification (CCF-A conf) [local copy] [slide]
• SCP2021: Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study
  Zhibin Yang*, Shenghao Yuan, Jean-Paul Bodeveix, Mamoun Filali, Tiexin Wang, Yong Zhou
  Science of Computer Programming (CCF-B journal) [local copy]

---

Visitors: