| 摘要: |
| 为评估控制器局域网络（Controller Area Network,CAN）攻击者入侵风险的影响，增强CAN总线设计的健壮性，提出了一种基于UPPAAL SMC的CAN总线健壮性验证方案。该方案首先针对嵌入式软件系统需求对CAN总线数据链路层与应用层进行形式化建模，采用模型检测技术对总线控制、收发、仲裁、应用层等功能进行仿真；其次使用攻击报文对CAN总线系统抗攻击性能进行验证与分析，开发人员可根据验证结果改进软件需求参数指标。实验结果表明，参数优化后，在总线被攻击情况下节点传输的准确率保持在75%以上，应答正确率可提升12.4%，加强了总线抗攻击能力。该方法为嵌入式软件通信总线系统设计的合理性提供了理论指导，规避开发后期的风险，可广泛应用于通信总线安全性能验证领域。 |
| 关键词: CAN总线 健壮性验证 需求建模 模型检测 时间自动机 |
| DOI：10.20079/j.issn.1001-893x.220415003 |
|
| 基金项目:民用航天技术预先研究项目（B0204） |
|
| Robustness Verification Technology of CAN Bus Based on Formalization |
| WANG Yihua,ZHOU Qing,HU Wanru,DU Jiahao |
| (1.National Space Science Center,Chinese Academy of Sciences,Beijing 100190,China;2.University of Chinese Academy of Sciences,Beijing 100049,China) |
| Abstract: |
| To evaluate the impact of the risk of attacker intrusion in Controller Area Network(CAN) and enhance the robustness of CAN bus design,a robustness verification scheme for CAN bus based on UPPAL SMC is proposed.The scheme firstly models the CAN bus data link layer and application layer formally for embedded software system requirements,and simulates the bus control,transceiver,arbitration,and application layer functions by using model detection technology.Secondly,the attack messages are used to verify and analyze the anti-attack performance of CAN bus system,and the developers can improve the software requirement parameter indexes according to the verification results.The experimental results show that after parameter optimization,the accuracy of node transmission under bus attack is maintained at more than 75%,and the correct response rate can be improved by 12.4%,which strengthens the bus anti-attack capability.The method provides theoretical guidance for the rationality of embedded software communication bus system design and avoids the risk in the later stage of development,and can be widely used in the field of communication bus security performance verification. |
| Key words: controller area network(CAN) bus robustness verification requirements modeling model checking timed automata |
