多时间无干扰性验证方法  

Multi-timed Noninterference Verification

作　　者：刘乔森 孙聪 魏晓敏 曾荟铭 马建峰 LIU Qiao-Sen;SUN Cong;WEI Xiao-Min;ZENG Hui-Ming;MA Jian-Feng(School of Cyber Engineering,Xidian University,Xi’an 710071,China)

机构地区：[1]西安电子科技大学网络与信息安全学院,陕西西安710071

出　　处：《软件学报》2024年第10期4729-4750,共22页Journal of Software

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

摘　　要：安全关键嵌入式软件的运行时行为通常具有严格时间约束,对安全属性的执行提出额外要求.针对嵌入式软件的信息流安全保护要求,以及现有安全性验证方法面向单一属性且存在假阳性等问题,首先从现实场景的安全需求出发,提出一种新的时间无干扰属性timed SIR-NNI;然后提出一种兼容多种时间无干扰属性(timed BNNI,timed BSNNI及timed SIR-NNI)统一验证的信息流安全验证方法,该验证方法依据不同的时间无干扰性要求,从待验证时间自动机自动构造测试自动机和精化自动机,通过UPPAAL的可达性分析实现精化关系检查和安全性验证.实现的验证工具TINIVER从SysML顺序图模型或C++源码提取时间自动机实施验证流程.使用TINIVER对现有时间自动机模型和安全属性的验证说明方法的可用性,对无人机飞行控制系统ArduPilot和PX4的典型飞行模式切换模型的安全验证说明方法的实用性和可扩展性.此外,方法能避免现有典型验证方法的假阳性缺陷.Safety-critical embedded software usually has rigorous time constraints over the runtime behaviors,raising additional requirements for enforcing security properties.To protect the information flow security of embedded software and mitigate the limitations of the existing simplex verification approaches and their potential false positives,this study first proposes a new timed noninterference property,i.e.,timed SIR-NNI,based on the security requirement of a realistic scenario.Then the study presents an information flow security verification approach that unifies the verification of multiple timed noninterference properties,i.e.,timed BNNI,timed BSNNI,and timed SIR-NNI.Based on the different timed noninterference requirements,the approach constructs the refined automata and test automata from the timed automata under verification.The study uses UPPAAL’s reachability analysis to implement the refinement relation check and the security verification.The verification tool,i.e.,TINIVER,extracts timed automata from SysML’s sequential diagrams or C++source code to conduct the verification procedure.The verification results of TINIVER on existing timed automata models and security properties justify the usability of the proposed approach.The security verifications on the typical flight-mode switch models of the UAV flight control systems ArduPilot and PX4 demonstrate the practicability and scalability of the proposed approach.Besides,the approach is effective in mitigating the false positives of a state-of-the-art verification approach.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]