佐治亚理工、QCRI 与普渡大学发布 CAN XL 首个形式化安全分析

佐治亚理工、QCRI 与普渡大学对 CAN XL 标准 MAC 子层完成首个形式化安全分析，发现它仍受全部已知 CAN CC MAC 子层问题影响，并新增 7 个漏洞。团队用商用 CAN XL 控制器验证漏洞，并在模拟真实车辆流量的测试台上演示了两种多阶段攻击，同时提出包括形式化验证标准修订在内的缓解方案。