电讯技术

作者：王一华,周晴,胡婉如,杜家昊

单位：(1.中国科学院 国家空间科学中心，北京 100190;2.中国科学院大学，北京 100049)

关键词：CAN总线；健壮性验证；需求建模；模型检测；时间自动机；

基金：民用航天技术预先研究项目（B0204）

为评估控制器局域网络（Controller Area Network,CAN）攻击者入侵风险的影响，增强CAN总线设计的健壮性，提出了一种基于UPPAAL SMC的CAN总线健壮性验证方案。该方案首先针对嵌入式软件系统需求对CAN总线数据链路层与应用层进行形式化建模，采用模型检测技术对总线控制、收发、仲裁、应用层等功能进行仿真；其次使用攻击报文对CAN总线系统抗攻击性能进行验证与分析，开发人员可根据验证结果改进软件需求参数指标。实验结果表明，参数优化后，在总线被攻击情况下节点传输的准确率保持在75%以上，应答正确率可提升12.4%，加强了总线抗攻击能力。该方法为嵌入式软件通信总线系统设计的合理性提供了理论指导，规避开发后期的风险，可广泛应用于通信总线安全性能验证领域。

来源：2023年第9期

《电讯技术》期刊编辑部

查看电讯技术杂志2023年第9期