软件学报

作者：苗新亮，常瑞，潘少平，赵永望，蒋烈辉

单位：苗新亮，数学工程与先进计算国家重点实验室(战略支援部队信息工程大学), 河南 郑州 450002;浙江大学 计算机科学与技术学院, 浙江 杭州 31002711,常瑞，浙江大学 计算机科学与技术学院, 浙江 杭州 310027;浙江省区块链与网络空间治理重点实验室, 浙江 杭州 31002702,潘少平，浙江大学 计算机科学与技术学院, 浙江 杭州 31002703,赵永望，浙江大学 计算机科学与技术学院, 浙江 杭州 31002704,蒋烈辉，数学工程与先进计算国家重点实验室(战略支援部队信息工程大学), 河南 郑州 45000205

关键词：内存标签;可信执行环境;访问控制;模型检测;安全性分析

基金：国家自然科学基金(61872016,62132014)

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

来源：2023年第8期

《软件学报》期刊编辑部

查看软件学报杂志2023年第8期