微信服务号

微信订阅号

2025-4-6- 7
Home > Archive>Volume 33, Issue 6, 2022 >2189-2207. DOI:10.13328/j.cnki.jos.006577
PDF HTML XML Export Cite reminder
Refinement-based Verification of Memory Isolation Mechanism for Trusted Execution Environment
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    A trusted execution environment (TEE) provides security-sensitive applications with an isolated execution environment based on hardware isolation mechanisms to protect sensitive data. The memory isolation mechanism is one of the key mechanisms of TEE, which is used to isolate the secure memory from the non-secure memory and to control the access to the secure memory. If the security of the memory isolation mechanism can not be guaranteed, sensitive data stored in the secure memory may be leaked. To verify the security of the TEE memory isolation mechanism, a refinement-based security verification method of the memory isolation mechanism is propose for ARM TrustZone-based TEE. An abstract model and a concrete model are established, a refinement relation between these two models is defined, and the information flow security of the concrete model is verified on the premise of proving that the refinement relation is held and the abstract model satisfies the information flow security properties. The proposed concrete model consists of key hardware and software of the TEE memory isolation mechanism, including TrustZone address space controller, MMU, and TrustZone monitor, and using the theorem prover Isabelle/HOL, it is verified that the concrete model satisfies the information flow security properties, such as noninterference, nonleakage, and noninfluence.

    Reference
    Related
    Cited by
Get Citation

靳翠珍,张倩颖,马雨薇,李希萌,王国辉,施智平,关永.基于精化的可信执行环境内存隔离机制验证.软件学报,2022,33(6):2189-2207

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 04,2021
  • Revised:October 14,2021
  • Online: January 28,2022
  • Published: June 06,2022
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033305Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063