多时间无干扰性验证方法
作者:
作者单位:

作者简介:

刘乔森(1998-), 男, 博士生, 主要研究领域为无人系统安全, 信息流安全;孙聪(1982-), 男, 博士, 教授, 博士生导师, CCF专业会员, 主要研究领域为软件安全, 程序分析, 无人系统安全;魏晓敏(1990-), 男, 博士, 讲师, CCF专业会员, 主要研究领域为系统安全, 可靠安全, 无人机, 嵌入式软件;曾荟铭(1997-), 男, 工程师, 主要研究领域为无人系统安全;马建峰(1963-), 男, 博士, 教授, 博士生导师, CCF会士, 主要研究领域为信息安全, 密码学, 网络安全

通讯作者:

孙聪, E-mail: suncong@xidian.edu.cn

中图分类号:

TP311

基金项目:

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


Multi-timed Noninterference Verification
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

刘乔森,孙聪,魏晓敏,曾荟铭,马建峰.多时间无干扰性验证方法.软件学报,2024,35(10):4729-4750

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-09-29
  • 最后修改日期:2023-03-28
  • 录用日期:
  • 在线发布日期: 2023-11-15
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号