PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot. - Zhuoruo Zhang; Chenyang Yu; He Huang; Rui Chang; Mingshuai Chen; Qinming Dai; Wenbo Shen; Yongwang Zhao; Kui Ren 001 (CoRR, 2022)

VeriReach: A Formally Verified Algorithm for Reachability Analysis in Virtual Private Cloud Networks. - Zhuoruo Zhang; Jilin Hu; Chenyang Yu; Rui Chang; Yongwang Zhao (ICWS, 2023)

Lark: Verified Cross-Domain Access Control for Trusted Execution Environments. - Fanlang Zeng; Zhuoruo Zhang; Rui Chang; Chenyang Yu; Zijun Zhang; Yongwang Zhao (ISSRE, 2023)

Interp-flow Hijacking: Launching Non-control Data Attack via Hijacking eBPF Interpretation Flow. - Qirui Liu; Wenbo Shen; Jinmeng Zhou; Zhuoruo Zhang; Jiayi Hu; Shukai Ni; Kangjie Lu; Rui Chang (ESORICS (3), 2024)

ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile. - Jilin Hu; Fanlang Zeng; Yongwang Zhao; Zhuoruo Zhang; Leping Zhang; Jianhong Zhao; Rui Chang; Kui Ren 001 (IEEE Trans. Dependable Secur. Comput., 2024)

A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana. - Shenghao Yuan; Zhuoruo Zhang; Jiayi Lu; David Sanán; Rui Chang; Yongwang Zhao (Proc. ACM Program. Lang., 2025)