软件学报

作者：刘乔森，孙聪，魏晓敏，曾荟铭，马建峰

单位：刘乔森，西安电子科技大学 网络与信息安全学院, 陕西 西安 71007111,孙聪，西安电子科技大学 网络与信息安全学院, 陕西 西安 71007102,魏晓敏，西安电子科技大学 网络与信息安全学院, 陕西 西安 71007103,曾荟铭，西安电子科技大学 网络与信息安全学院, 陕西 西安 71007104,马建峰，西安电子科技大学 网络与信息安全学院, 陕西 西安 71007105

关键词：无干扰性;时间自动机;精化关系;可达性分析;信息流安全

基金：国家自然科学基金(62272366, 61872279); 陕西省重点研发计划(2023-YBGY-371); 陕西省自然科学基础研究计划(2021JQ-207)

安全关键嵌入式软件的运行时行为通常具有严格时间约束, 对安全属性的执行提出额外要求. 针对嵌入式软件的信息流安全保护要求, 以及现有安全性验证方法面向单一属性且存在假阳性等问题, 首先从现实场景的安全需求出发, 提出一种新的时间无干扰属性timed SIR-NNI; 然后提出一种兼容多种时间无干扰属性(timed BNNI, timed BSNNI及timed SIR-NNI)统一验证的信息流安全验证方法, 该验证方法依据不同的时间无干扰性要求, 从待验证时间自动机自动构造测试自动机和精化自动机, 通过UPPAAL的可达性分析实现精化关系检查和安全性验证. 实现的验证工具TINIVER从SysML顺序图模型或C++源码提取时间自动机实施验证流程. 使用TINIVER对现有时间自动机模型和安全属性的验证说明方法的可用性, 对无人机飞行控制系统ArduPilot和PX4的典型飞行模式切换模型的安全验证说明方法的实用性和可扩展性. 此外, 方法能避免现有典型验证方法的假阳性缺陷.

来源：2024年第10期

《软件学报》期刊编辑部

查看软件学报杂志2024年第10期