可信执行环境访问控制建模与安全性分析

可信执行环境(TEE)的安全问题一直受到国内外学者的关注.利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制,但已有方案往往依赖于测试或者经验分析表明其有效性,缺乏严格的正确性和安全性保证.针对内存标签实现的访问控制提出通用的形式化模型框架,并提出一种基于模型检测的访问控制安全性分析方法.首先,利用形式化方法构建基于内存标签的可信执行环境访问控制通用模型框架,给出访问控制实体的形式化定义,定义的规则包括访问控制规则和标签更新规则;然后利用形式化语言B以递增的方式设计并实现该框架的抽象机模型,通过不变式约束形式化描述模型的基本性质;再次以可信执行环境的一个具体实现TIMBER-V为应用实例,通过实例化抽象机模型构建TIMBER-V访问控制模型,添加安全性质规约并运用模型检测验证模型的功能正确性和安全性;最后模拟具体攻击场景并实现攻击检测,评估结果表明提出的安全性分析方法的有效性.