基于TrustZone的TEE设计与信息流形式化验证

• 作者: 乔磊 孙海泳 杨拯 杨霞 雷航
• 来源期刊: 电子科技大学学报
• 学科: 工学
• 关键词: 形式化方法 信息流验证 可信执行环境 TrustZone
• 年，卷（期）: 2019,（2）
• 所属期刊栏目: 计算机工程与应用
• 页码范围: 259-263
• 页数: 5页
• 分类号: TP311
• 字数: 4995字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0548.2019.02.016

摘要

基于可信硬件构建安全关键应用的可信执行环境(TEE),是嵌入式安全领域的一个研究热点.虽然底层硬件可信,但TEE软件仍可能因错误使用硬件指令或存在其他安全漏洞而导致机密信息泄露.该文基于ARM TrustZone技术提出了多层次的TEE架构,并建立了安全通信通道,用户层可信应用不能直接访问非可信环境的软硬件资源,只能通过内核层的安全通信通道API与外界通信,因此整个TEE的信息流不再受用户层影响.该文进一步提出了TEE形式化模型(TEEFM),借助Coq辅助证明器验证了TEE信息流无干扰性并证明了TEE安全监控模块不存在整型溢出、程序返回地址异常等资源边界类软件漏洞,以此保证了TEE的自身安全性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	雷航	电子科技大学信息与软件工程学院	92	1434	17.0	35.0
2	杨霞	电子科技大学信息与软件工程学院	19	117	7.0	10.0
3	乔磊		17	39	4.0	5.0
4	孙海泳	电子科技大学信息与软件工程学院	3	4	1.0	2.0
5	杨拯	电子科技大学信息与软件工程学院	1	0	0.0	0.0