多时间无干扰性验证方法

作     者：刘乔森 孙聪 魏晓敏 曾荟铭 马建峰 LIU Qiao-Sen;SUN Cong;WEI Xiao-Min;ZENG Hui-Ming;MA Jian-Feng

作者机构：西安电子科技大学网络与信息安全学院陕西西安710071 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2024年第35卷第10期

页      面：4729-4750页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

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

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