A Property-Based Attestation Scheme with the Variable Privacy. - Yu Qin; Dexian Chang; Shijun Zhao; Qianying Zhang (TrustCom, 2011)

TEEM: A User-Oriented Trusted Mobile Device for Multi-platform Security Applications. - Wei Feng; Dengguo Feng; Ge Wei; Yu Qin; Qianying Zhang; Dexian Chang (TRUST, 2013)

Providing Root of Trust for ARM TrustZone using On-Chip SRAM. - Shijun Zhao; Qianying Zhang; Guangyao Hu; Yu Qin; Dengguo Feng (TrustED@CCS, 2014)

Mdaak: A Flexible and Efficient Framework for Direct Anonymous Attestation on Mobile Devices. - Qianying Zhang; Shijun Zhao; Li Xi; Wei Feng; Dengguo Feng (ICICS, 2014)

Improving the Security of the HMQV Protocol Using Tamper-Proof Hardware. - Qianying Zhang; Shijun Zhao; Yu Qin; Dengguo Feng (SecureComm (1), 2014)

Providing Root of Trust for ARM TrustZone using SRAM PUFs. - Shijun Zhao; Qianying Zhang; Guangyao Hu; Yu Qin; Dengguo Feng (IACR Cryptol. ePrint Arch., 2014)

Universally Composable secure TNC protocol based on IF-T binding to TLS. - Shijun Zhao; Qianying Zhang; Yu Qin; Dengguo Feng (IACR Cryptol. ePrint Arch., 2014)

Urban Disaster Comprehensive Risk Assessment Research Based on GIS: A Case Study of Changsha City, Hunan Province, China. - Chaolin Wang; Shaobo Zhong; Qianying Zhang; Quanyi Huang (GRMSE, 2015)

A Unified Security Analysis of Two-Phase Key Exchange Protocols in TPM 2.0. - Shijun Zhao; Qianying Zhang (TRUST, 2015)

sHMQV: An Efficient Key Exchange Protocol for Power-limited Devices. - Shijun Zhao; Qianying Zhang (IACR Cryptol. ePrint Arch., 2015)

Security analysis of SM2 key exchange protocol in TPM2.0. - Shijun Zhao; Li Xi; Qianying Zhang; Yu Qin; Dengguo Feng (Secur. Commun. Networks, 2015)

函数矩阵及其微积分的高阶逻辑形式化 (Higher-order Logic Formalization of Function Matrix and its Calculus). - Xiumei Yang; Yong Guan; Zhiping Shi 002; Aixuan Wu; Qianying Zhang; Jie Zhang 074 (计算机科学, 2016)

A New Way to Prevent UKS Attacks Using Hardware Security Chips. - Qianying Zhang; Zhiping Shi 002 (Int. J. Netw. Secur., 2017)

Formalization of Symplectic Geometry in HOL-Light. - Guohui Wang; Yong Guan; Zhiping Shi 002; Qianying Zhang; Xiaojuan Li; Yongdong Li (ICFEM, 2018)

Formal Modelling and Verification of Spinlocks at Instruction Level. - Leping Zhang; Qianying Zhang; Guohui Wang; Zhiping Shi 002; Minhua Wu; Yong Guan (APSEC, 2019)

SecTEE: A Software-based Approach to Secure Enclave Architecture Using TEE. - Shijun Zhao; Qianying Zhang; Yu Qin; Wei Feng; Dengguo Feng (CCS, 2019)

Towards Verifying Ethereum Smart Contracts at Intermediate Language Level. - Ximeng Li 003; Zhiping Shi 002; Qianying Zhang; Guohui Wang; Yong Guan; Ning Han (ICFEM, 2019)

Minimal Kernel: An Operating System Architecture for TEE to Resist Board Level Physical Attacks. - Shijun Zhao; Qianying Zhang; Yu Qin; Wei Feng; Dengguo Feng (RAID, 2019)

MicroTEE: Designing TEE OS Based on the Microkernel Architecture. - Dongxu Ji; Qianying Zhang; Shijun Zhao; Zhiping Shi 002; Yong Guan (TrustCom/BigDataSE, 2019)

A Comprehensive Formal Security Analysis and Revision of the Two-phase Key Exchange Primitive of TPM 2.0. - Qianying Zhang; Shijun Zhao; Zhiping Shi 002; Yong Guan; Guohui Wang (CoRR, 2019)

Formalization of Geometric Algebra in HOL Light. - Li-Ming Li; Zhi-Ping Shi 002; Yong Guan; Qianying Zhang; Yong-Dong Li (J. Autom. Reason., 2019)

SoftME: A Software-Based Memory Protection Approach for TEE System to Resist Physical Attacks. - Meiyu Zhang; Qianying Zhang; Shijun Zhao; Zhiping Shi 002; Yong Guan (Secur. Commun. Networks, 2019)

Formal Verification of Memory Isolation for the TrustZone-based TEE. - Yuwei Ma; Qianying Zhang; Shijun Zhao; Guohui Wang; Ximeng Li 003; Zhiping Shi 002 (APSEC, 2020)

Formalizing the Transaction Flow Process of Hyperledger Fabric. - Xiangyu Chen; Ximeng Li 003; Qianying Zhang; Zhiping Shi 002; Yong Guan (ICFEM, 2020)

A comprehensive formal security analysis and revision of the two-phase key exchange primitive of TPM 2.0. - Qianying Zhang; Shijun Zhao (Comput. Networks, 2020)

Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula. - Shanyan Chen; Guohui Wang; Ximeng Li 003; Qianying Zhang; Zhi-Ping Shi 002; Yong Guan (Formal Aspects Comput., 2020)

Reasoning About Iteration and Recursion Uniformly Based on Big-Step Semantics. - Ximeng Li 003; Qianying Zhang; Guohui Wang; Zhiping Shi 002; Yong Guan (SETTA, 2021)

Design and Implementation of OOM Module based on Rust. - Linhan Li; Qianying Zhang; Shijun Zhao; Zhi-Ping Shi 002; Yong Guan (QRS Companion, 2022)

Formal Verification of Interrupt Isolation for the TrustZone-based TEE. - Leping Zhang; Qianying Zhang; Xinyue Wang; Ximeng Li 003; Guohui Wang; Zhiping Shi 002; Yong Guan (APSEC, 2023)

A unified proof technique for verifying program correctness with big-step semantics. - Ximeng Li 003; Qianying Zhang; Guohui Wang; Zhi-Ping Shi 002; Yong Guan (J. Syst. Archit., 2023)

Intrinsic Image Transfer for Illumination Manipulation. - Junqing Huang; Michael V. Ruzhansky; Qianying Zhang; Haihui Wang (IEEE Trans. Pattern Anal. Mach. Intell., 2023)

A nonlocal diffusion competition model with seasonal succession and free boundaries. - Qianying Zhang; Mingxin Wang (Commun. Nonlinear Sci. Numer. Simul., 2023)

Refinement Verification of OS Services based on a Verified Preemptive Microkernel. - Ximeng Li 003; Shanyan Chen; Yong Guan; Qianying Zhang; Guohui Wang; Zhiping Shi 002 (FASE, 2024)

rOOM: A Rust-Based Linux Out of Memory Kernel Component. - Linhan Li; Qianying Zhang; Zekun Xu; Shijun Zhao; Zhiping Shi 002; Yong Guan (IEICE Trans. Inf. Syst., 2024)

Formal Verification of Functional Correctness for Mutexes in Microkernel. - Linyan Zhang; Ximeng Li 003; Zhi-Ping Shi 002; Yong Guan; Qinxiang Cao; Qianying Zhang (Int. J. Softw. Informatics, 2024)