A Formal Framework of Shielding Systems by Stepwise Refinement

Jiabin Zhu ； Wenchao Huang ； Fuyou Miao ； Cheng Su ； Baohua Zhao ； Yan Xiong

《International Journal of Network Security》 22卷1期 (2020/01) Pp. 54-67

https://doi.org/10.6633/IJNS.202001_22(1).06

摘要

The shielding systems, e.g., special-purpose hypervisor, provide more secure environments for security-critical applications (SCAs), compared with traditional computer systems. In this paper, we propose a general framework of formally modeling and verifying the shielding systems for enhancing the security. The framework supports multiples types of shielding systems based on different technologies, such as Intel TXT or TrustZone. It is implemented by stepwise refinement, in which the early steps model the common states, events and security properties among the systems. Then the shielding systems are modeled in latter steps, where all the events are refined from the ones in the previous steps without the requirement of reproving soundness of security properties, e.g., memory isolation, data confidentiality, upon the occurrence of each event. Therefore, the complexity of formally verifying new shielding systems is reduced. We implement the framework in the Coq proof assistant, and find potential security threats in using the shielding systems.

關鍵字

Formal Methods ； Framework ； Security Analysis ； Shielding Systems