轩辕实验室丨欧盟EVITA项目预研第一章（三）

本文主要是介绍轩辕实验室丨欧盟EVITA项目预研第一章（三），希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

本文主要介绍车载通信的安全协议、对结构和协议的验证方法和攻击分析，以及模型驱动的安全工程的相关内容。

本文来自本实验室龚思陈的读书笔记

车载信息安全协议

抽象网络结构如下：

在实体网联汽车上对应如下：

- EBCM：Electronic Brake Control Module电子制动控制模块

外部通信

- 目标车是一个黑盒

对新应用的新的安全要求：

-    采用虚拟化方法

-    屏蔽执行环境

-    允许第三方设施和应用加入的开放的环境

-    访问控制

EVITA的车载协议

原则：

对依赖外部数据的应用程序建立信任；
基于以下两类加密材料

- 受保护而不会遭到攻击的

- 已被外部信任的第三方证实的
基于整个汽车平台的完整性

设计目标（Design Goals）：

高效的-用于安全的开销小
可扩展的-ECU的数量
网络无关的-可用于CAN,FlexRay,Ethernet等
可移植的-适用于不同的运行环境（RTE）

方法：

面向服务的分层协议设计
基于仿真模拟的费用估计
结合对称加密和非对称加密

内部通信（ECU之间）

一对多的安全通信

- 在ECU/HSM处实现基础使用控制

- 在KeyMaster处实现全面的访问控制

数据的传递和处理

- 使用“通信传输协议”以确保在不同的总线上启用通信和路由

安全会话

通用传输协议（CTP,the Common Transport Protocol）提供：

- 发送者地址和发送终点地址

- 较大的有效载荷
在通用传输协议的基础上，EVITA项目额外提供以下：

- 安全有效载荷

- 一对多通信

结构和协议的验证方法和攻击分析

车载系统

ECU（电子控制单元）=硬件元件的集合

-     执行元素（CPU,HWA）

-     通信元素（总线）

-     存储元素（RAM,flash）

-     输入输出设备（传感器、制动器）
软件元件

- 在CPU上执行

安全属性的证明（EVITA的目标之一）：整体的方法论

需求识别
结构规范
安全相关的协议规范
整个系统安全性能的验证包括：

1）性能测评

评价安全机制对系统性能的影响

2）攻击分析

a.放大视图法

- 从EVITA结构中的一个子区域中得出安全性能的依据

b.全局合成法

- 用实施在子元素上的证明方法去证实对整个系统的要求
验证方法

-  考虑输入（如：EVITA的可交付成果）

-  建模：用统一建模语言建模（如：SysML,UML）

-  仿真分析

-  形式化验证

整体概览

TTool

主要特征

开放源码的统一建模语言（UML）工具包
支持UML2 profiles（数据建模）

- 当下支持8个UML profile

如：TURTLE，DIPLODOCUS
大部分用Java编程

- 使用外部工具的编辑器与接口

- 模拟器用C++或SystemC编程
形式化验证和仿真的特点

- 向建模者隐藏形式化验证和仿真模拟的复杂性

- 依赖于外部工具

- 使用按钮（Press-button）

TTool的例子：TURTLE和DIPLODOCUS

DIPLODOCUS——性能测评的方法论

主要特征

-     数据抽象

-     形式化语义

-     高速仿真支持

-    完全由开源工具支持（TTool）
use cases：主动制动（active brake）

C2C之间传递的信息：

- 即将发生碰撞的危险警告

- 即时制动操纵
在通信单元接收并校验了的信息
对底盘安全控制器的合理性检查

- 如果刹车是最好的解决方案，那么刹车指令将被发送到刹车控制单元
动力总成控制器也获知了这条指令以减速

- 刹车的信息可能会被传递到邻近的车
建模与制图

一些仿真的结果

- CPU和硬件加速器

CPU	Load	Contention delay
Load_Emulation	0.15711	29973
CPU_CU	0.11244	0
HSM_CU	0.11939	0
CPU_BCU	0.00010	6806
HSM_BCU	0.00004	0
CPU_PTC	0.00018	0
CPU_ChassisSensor	0.00035	200000
CPU_EnvSensor	0.01115	5818
HSM_CSC	0.11827	0
…	…	…

- 总线

Bus	Load
BCU_local_Bus	0.00017
CSC_local_Bus	0.56926
PTC_local_Bus	0.00026
CU_local_Bus	0.55783
CU_SOC_Bus	0.78811
Main_CAN	0.71469
CSC_SOC_bus	0.74216
…	…

TURTLE——攻击分析的方法论

简介

-       针对带有时间约束的嵌入式系统

-       3个子概要（sub-profiles）：分析、设计、部署

-       形式化验证和仿真

-       TURTLR设计=类图+一组活动图
主要特征

- 非确定性的运算

->选择，延迟

- 完全由开源工具包支持（TTool）
主要原则

1、建模元素

ECU里的硬件元件

a. HSM

b. 通信网络
软件元件

a.涉及ECU的协议栈

2、对安全性能的证明
用观察的技巧
运用模型检查的方法来搜索给定的操作

用CADP进行形式化验证

验证方法

- 用CADP产生可达图

- 最小化可达图

- 搜索包含attackOK和attackKO操作的轨迹
可达图(Reachability graph)

用UPPAAL进行形式化验证

验证方法

- 在UML模型中选择感兴趣的操作

- 自动调用UPPAAL

- 搜索已选中操作的可访问性和活性
待探测的网络

无法被探测的网络

总能被探测的网络

总结

1) 为嵌入式系统的设计和验证完全集成的环境

基于UML/SysML，开源工具包（TTool）
形式化验证可以解决：

- 安全性和安全属性

->实现对真实性、保密性、新鲜度的验证

- 功能属性和非功能属性

2) 回顾方法论的阶段

捕捉需求（SysML,DIPLPDPCUS）

- 攻击树，需求的定义和组织
性能测评（DIPLODOCUS）
攻击分析，放大视图法（TURTLE）

模型驱动的安全工程方法

什么是模型驱动的工程？

- 专注于创建模型或抽象的软件开发方法。例如：基于对象建模组（UML）的模型驱动架构。

将模型从抽象细化为具体：

- 计算无关模型（CIM）→平台无关模型（PIM）→平台相关模型（PSM）

智能汽车中的模型驱动工程：AUTOSAR的方法论

安全工程的形式化方法

-    形式模型检查，一种安全验证技术。

-    尝试为安全属性提供正式定义。

-    允许对安全属性进行推理，而不会出现误解的问题

形式化方法的语言非常复杂：

-    假设S是一个满足precede(x,b)的体系，设B为系统的行为。那么，如果动作w∈B且b∈alph(w),那么x∈alph(w).

-   进而，如果precede(a,x)在体系S中成立，那么，如果w∈B,x∈alph(w),则a∈alph(w).

-   因此，我们得出：当b∈alph(w)时，a∈alph(w),即precede(a,b)在S体系中成立。

便于理解的图示：

即，precede（x,y）具有传递性

具体的安全工程的进程

agent的缩写

V0	sensing Vehicle
V1	braking Vehicle
Env	Environment-Sensor
Cha	Chassis-Sensor
App	Application-ECU
CU	Communication Unit
HMI	Human-Machine-Interface
BC	Brake Controller
D	Driver of V1

数据的缩写

Pos	Position-Information
EnvInfo	Environment-Information
VeDy	Vehicle-Dynamics
CAM	Car2x-Awareness-Message
LDW	Local-Danger-Warning-Message
Warn	Driver-Warning-Message