3 papers
cs.PL2021
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
Ximeng Li, Qianying Zhang, Guohui Wang +2
A reliable technique for deductive program verification should be proven sound with respect to the semantics of the programming language. For each different language, the construct…
cs.CR2019
MicroTEE: Designing TEE OS Based on the Microkernel Architecture
Dongxu Ji, Qianying Zhang, Shijun Zhao +2
ARM TrustZone technology is widely used to provide Trusted Execution Environments (TEE) for mobile devices. However, most TEE OSes are implemented as monolithic kernels. In such de…
cs.CR2019
A Comprehensive Formal Security Analysis and Revision of the Two-phase Key Exchange Primitive of TPM 2.0
Qianying Zhang, Shijun Zhao
The Trusted Platform Module (TPM) version 2.0 provides a two-phase key exchange primitive which can be used to implement three widely-standardized authenticated key exchange protoc…