Is your access allowed or not? A Verified Tag-based Access Control Framework for the Multi-domain TEE. - Xinliang Miao; Fanlang Zeng; Rui Chang; Chenyang Yu; Zijun Zhang; Liehui Jiang; Yongwang Zhao (Internetware, 2022)

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

Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone. - Fanlang Zeng; Rui Chang; Hao Xu; Shaoping Pan; Yongwang Zhao (Int. J. Softw. Informatics, 2023)

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)

Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic. - Fanlang Zeng; Rui Chang; Hongjian Liu (Proc. ACM Softw. Eng., 2025)

KBX: Verified Model Synchronization via Formal Bidirectional Transformation. - Jianhong Zhao; Yongwang Zhao; Peisen Yao; Fanlang Zeng; Bohua Zhan; Kui Ren 001 (ACM Trans. Softw. Eng. Methodol., 2025)