微信服务号

微信订阅号

2025年3月14日 20:35 星期五
首页 > 过刊浏览>2023年第34卷第8期 >3507-3526. DOI:10.13328/j.cnki.jos.006866
PDF HTML阅读 XML下载 导出引用 引用提醒
基于精化的TrustZone多安全分区建模与形式化验证
作者:
作者简介:

曾凡浪(1994-),男,博士生,CCF学生会员,主要研究领域为可信执行环境,形式化方法;潘少平(1994-),男,硕士生,主要研究领域为可信执行环境,形式化验证.<;常瑞(1981-),女,博士,副教授,博士生导师,CCF高级会员,主要研究领域为硬件辅助安全,形式化验证,程序分析;赵永望(1979-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为形式化,操作系统与安全,编程语言与编译,安全认证;许浩(1999-),男,硕士生,主要研究领域为可行执行环境,形式化方法.

通讯作者:

常瑞,E-mail:crix1021@zju.edu.cn

基金项目:

浙江省重点研发计划（2022C01165）；国家自然科学基金（62132014）；浙江省尖兵计划（2022C01045）；中央高校基本科研业务费（NGICS）专项资金


Refinement-based Modeling and Formal Verification for Multiple Secure Partitions of TrustZone
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [33]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    TrustZone作为ARM处理器上的可信执行环境技术，为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而，可信操作系统与所有可信应用运行在同一个可信环境中，任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术，支持在安全世界建立多个隔离分区来缓解这个问题，但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构，提出一种基于精化的TrustZone多安全分区建模与安全性分析方法，并基于定理证明器Isabelle/HOL完成了分区管理器的建模和形式化验证.首先，基于逐层精化的方法构建了多安全分区模型RMTEE，使用抽象状态机描述系统运行过程和安全策略要求，建立多安全分区的抽象模型并实例化实现分区管理器的具体模型，遵循FF-A规范在具体模型中实现了事件规约；其次，针对现有分区管理器设计无法满足信息流安全性验证的不足，设计了基于DAC的分区间通信访问控制，并将其应用到TrustZone安全分区管理器的建模与验证中；再次，证明了具体模型对抽象模型精化的正确性以及具体模型中事件规约的正确性和安全性，从而完成模型所述137个定义和201个定理的形式化证明（超过11 000行Isabelle/HOL代码）.结果表明：该模型满足机密性和完整性，并可有效防御分区的恶意攻击.

    Abstract:

    As a trusted execution environment technology on ARM processor, TrustZone provides an isolated and independent execution environment for security sensitive programs and data on the device. However, making trusted OS and all trusted applications run in the same trusted environment may cause problems-the exploitation of vulnerabilities on any component will affect the others in the system. Although ARM proposed S-EL2 virtualization technology, which supports multiple isolated partitions in the security world to alleviate this problem, there may still be security threats such as information leakage between partitions in the actual partition manager. Current secure partition manager designs and implementations lack rigorous mathematical proofs to guarantee the security of isolated partitions. This study analyzes the multiple secure partitions architecture of ARM TrustZone in detail, proposes a refinement-based modeling and security analysis method for multiple secure partitions of TrustZone, and completes the modeling and formal verification of the secure partition manager based on the theorem prover Isabelle/HOL. First, a multiple security partitions model named RMTEE is built based on refinement, an abstract state machine is used to describe the system running process and security policy requirements, and the abstract model of multiple secure partitions is established and instantiated. Then the concrete model of the secure partition manager is implemented, in which the event specification is implemented following the FF-A specification. Secondly, in view of the problem that the existing partition manager design cannot meet the goal of information flow security verification, a DAC-based inter-partition communication access control is designed and applied to the modeling and verification of TrustZone security partition manager. Finally, the correctness of the concrete model's refinement of the abstract model and the correctness and security of the event specification in the concrete model are proved, thus completing the formal proof of 137 definitions and 201 lemmas in the model (more than 11 000 lines of Isabelle/HOL code). The results show that the model satisfies confidentiality and integrity, and can effectively defend against malicious attacks of partitions.

    参考文献
    [1] Ngabonziza B, Martin D, Bailey A, et al.TrustZone explained:Architectural features and use cases.In:Proc.of the 2nd Int'l Conf.on Collaboration and Internet Computing.Pittsburgh:IEEE, 2016.445-451.[doi:10.1109/CIC.2016.065]
    [2] GlobalPlatform.Introduction to trusted execution environments.2018.https://globalplatform.org/wp-content/uploads/2018/05/Introduction-to-Trusted-Execution-Environment-15May2018.pdf
    [3] Pinto S, Santos N.Demystifying arm trustzone:A comprehensive survey.ACM Computing Surveys (CSUR), 2019, 51(6):1-36.[doi:10.1145/3291047]
    [4] Cerdeira D, Santos N, Fonseca P, et al.Sok:Understanding the prevailing security vulnerabilities in trustzone-assisted tee systems.In:Proc.of the 41st IEEE Symp.on Security and Privacy.San Francisco:IEEE, 2020.1416-1432.[doi:10.1109/SP40000.2020.00061]
    [5] VulDB.NVIDIA jetson OTE protocol message parser memory leak.2021.https://vuldb.com/?id.177340
    [6] F-Secure.Security advisory:OP-TEE TrustZone bypass at wakeup on NXP i.MX6UL.2021.https://github.com/f-secure-foundry/advisories/blob/master/Security_Advisory-Ref_FSC-HWSEC-VR2021-0002-OP-TEE_TrustZone_bypass_at_wakeup.txt
    [7] ARM.Learn the architecture-AArch64 virtualization.https://developer.arm.com/documentation/102142/0100
    [8] ARM.Arm firmware framework for arm a-profile.https://developer.arm.com/documentation/den0077
    [9] VulDB.Qualcomm snapdragon auto TrustZone memory transfer interface information disclosure.2021.https://vuldb.com/?id.189552
    [10] Wirth N.Program development by stepwise refinement.Communications of the ACM, 1983, 26(1):70-74.[doi:10.1145/357980.358010]
    [11] Back RJR, Sere K.Stepwise refinement of action systems.In:Proc.of the Int'l Conf.on Mathematics of Program Construction.Berlin, Heidelberg:Springer, 1989.115-138.[doi:10.1007/3-540-51305-1_7]
    [12] Azab AM, Ning P, Shah J, et al.Hypervision across worlds:Real-time kernel protection from the arm trustzone secure world.In:Proc.of the 2014 ACM SIGSAC Conf.on Computer and Communications Security.New York:Association for Computing Machinery, 2014.90-102.[doi:10.1145/2660267.2660350]
    [13] Li W, Xia Y, Lu L, et al.TEEv:Virtualizing trusted execution environments on mobile platforms.In:Proc.of the 15th ACM SIGPLAN/SIGOPS Int'l Conf.on Virtual Execution Environments.New York:Association for Computing Machinery, 2019.2-16.[doi:10.1145/3313808.3313810]
    [14] Cerdeira D, Martins J, Santos N, et al.REZONE:Disarming TrustZone with TEE privilege reduction.In:Proc.of the 31st USENIX Security Symp.(USENIX Security 2022).Boston:USENIX Association, 2022.2261-2279.
    [15] Li D, Mi Z, Xia Y, et al.TwinVisor:Hardware-isolated confidential virtual machines for ARM.In:Proc.of the 28th SIGOPS Symp.on Operating Systems Principles.New York:Association for Computing Machinery, 2021.638-654.[doi:10.1145/3477132.3483554]
    [16] ARM.Introducing arm confidential compute architecture.2022.https://developer.arm.com/documentation/den0125/latest
    [17] Mulligan DP, Petri G, Spinale N, et al.Confidential computing-A brave new world.In:Proc.of the 2021 Int'l Symp.on Secure and Private Execution Environment Design (SEED).Washington:IEEE, 2021.132-138.[doi:10.1109/SEED51797.2021.00025]
    [18] Li X, Li X, Dall C, et al.Design and verification of the arm confidential compute architecture.In:Proc.of the 16th USENIX Symp.on Operating Systems Design and Implementation (OSDI 2022).Carlsbad:USENIX Association, 2022.465-484.
    [19] Klein G, Elphinstone K, Heiser G, et al.seL4:Formal verification of an OS kernel.In:Proc.of the 22nd ACM SIGOPS Symp.on Operating Systems Principles.New York:Association for Computing Machinery, 2009.207-220.[doi:10.1145/1629575.1629596]
    [20] Gu R, Shao Z, Chen H, et al.CertiKOS:An extensible architecture for building certified concurrent OS kernels.In:Proc.of the 12th USENIX Symp.on Operating Systems Design and Implementation (OSDI 2016).Savannah:USENIX Association, 2016.653-669.
    [21] Zhao Y, Sanán D, Zhang F, et al.Reasoning about information flow security of separation kernels with channel-based communication.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2016.791-810.[doi:10.1007/978-3-662-49674-9_50]
    [22] Zhao Y, Sanán D, Zhang F, et al.Refinement-based specification and security analysis of separation kernels.IEEE Trans.on Dependable and Secure Computing, 2017, 16(1):127-141.[doi:10.1109/TDSC.2017.2672983]
    [23] Li S W, Li X, Gu R, et al.A secure and formally verified Linux KVM hypervisor.In:Proc.of the 2021 IEEE Symp.on Security and Privacy (SP).San Francisco:IEEE, 2021.1782-1799.[doi:10.1109/SP40001.2021.00049]
    [24] Li S W, Li X, Gu R, et al.Formally verified memory protection for a commodity multiprocessor hypervisor.In:Proc.of the 30th USENIX Security Symp.(USENIX Security 2021).USENIX Association, 2021.3953-3970.
    [25] Ma Y, Zhang Q, Zhao S, et al.Formal verification of memory isolation for the trustzone-based TEE.In:Proc.of the 27th Asia-Pacific Software Engineering Conf.Singapore:IEEE, 2020.149-158.[doi:10.1109/APSEC51365.2020.00023]
    [26] Jin CZ, Zhang QY, Ma YW, et al.Refinement-based verification of memory isolation mechanism for trusted execution environment.Ruan Jian Xue Bao/Journal of Software, 2022, 33(6):2189-2207(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/6577.htm[doi:10.13328/j.cnki.jos.006577]
    [27] Miao XL, Chang R, Pan SP, et al.Modeling and security analysis of access control in trusted execution environment.Ruan Jian Xue Bao/Journal of Software, 2023, 34(8):3637-3658(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/6612.htm[doi:10.13328/j.cnki.jos.006612]
    [28] Haigh JT, Young WD.Extending the noninterference version of MLS for SAT.IEEE Trans.on Software Engineering, 1987, (2):141-150.[doi:10.1109/TSE.1987.226478]
    [29] Oheimb D.Information flow control revisited:Noninfluence=noninterference+nonleakage.In:Proc.of the European Symp.on Research in Computer Security.Berlin, Heidelberg:Springer, 2004.225-243.[doi:10.1007/978-3-540-30108-0_14]
    [30] Hoare CAR.An axiomatic basis for computer programming.Communications of the ACM, 1969, 12(10):576-580.[doi:10.1145/363235.363259]
    附中文参考文献
    [26] 靳翠珍, 张倩颖, 马雨薇, 等.基于精化的可信执行环境内存隔离机制验证.软件学报, 2022, 33(6):2189-2207.http://www.jos.org.cn/1000-9825/6577.htm[doi:10.13328/j.cnki.jos.006577]
    [27] 苗新亮, 常瑞, 潘少平, 等.可信执行环境访问控制建模与安全性分析.软件学报, 2023, 34(8):3637-3658.http://www.jos.org.cn/1000-9825/6612.htm[doi:10.13328/j.cnki.jos.006612]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

曾凡浪,常瑞,许浩,潘少平,赵永望.基于精化的TrustZone多安全分区建模与形式化验证.软件学报,2023,34(8):3507-3526

复制
分享
文章指标
  • 点击次数:1322
  • 下载次数: 4032
  • HTML阅读次数: 2125
  • 引用次数: 0
历史
  • 收稿日期:2022-09-04
  • 最后修改日期:2022-10-13
  • 在线发布日期: 2022-12-30
  • 出版日期: 2023-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19700992位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号