Shenghao YUAN Researcher, Zhejiang University Email: shenghao.yuan@inria.fr(Deprecated) / nuaaysh@126.com Open Source Software: GitLab (read-only) / GitHub / GitHub Organization 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, France

---

Serment des docteurs relatif à l'intégrité scientifique (English version: Doctoral Oath on Scientific Integrity; 中文版本: 博士科学诚信誓言)

At the end of the defence and in case of admission, I takes an oath, individually committing myself to respect the principles and requirements of scientific integrity in the rest of my professional career, whatever the sector or area of activity.

• The text of the oath is as follows: In the presence of my peers. With the completion of my doctorate in computer science, in my quest for knowledge, I have carried out demanding research, demonstrated intellectual rigour, ethical reflection and respect for the principles of research integrity. As I pursue my professional career, whatever my chosen field, I pledge to the greatest of my ability to continue to maintain integrity in my relationship to knowledge, in my methods and in my results.

Research Interests

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

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 (CVE-2025-40169)
  • bpf: Add range tracking for BPF_DIV and BPF_MOD and related selftests
  • bpf: Add bitwise tracking for BPF_END and related selftests (bad news: introduce another issue; BUT now has been fixed)
  • bpf: reject bpf-to-bpf call with large offset in interpreter (Working on a better solution)
  • (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
  • Cleanup - Remove unreachable None branch in emit_profile_instruction_count

---

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)

Perhaps it is often assumed that the future work section in a paper merely outlines ideas that may never be pursued. I would like to clarify that when I discuss future work, I am either actively carrying out those follow-up studies or explaining here why I have chosen to move in a different direction.

• [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]
  Future Work: Serving for [OOPSLA2025]
  
• [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]
  Future Work: No progress. I noticed that EVM and Solana are actually using this hybrid solution, which suggests that a fully JIT-compiled approach may not be strictly necessary. By the way, this was my final work during my Ph.D. After that, I shifted my focus to Solana and Linux eBPF, see [OOPSLA2025]
  
• [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]
  Future Work:No progress. One reason is that LLM could do something like AutoCorres, and I was interested in Rust after Ph.D.
  
• [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]
  Future Work: Working on verified eBPF JIT, see [CAV2024]
  
• [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]
  Future Work: No progress. as I have since shifted my focus to my PhD topic, and no one else has shown interest in pursuing this line of work.
  

---

Visitors: