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

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

车载信息安全协议

• 抽象网络结构如下：

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

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

• 外部通信

  -  目标车是一个黑盒

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

  -    采用虚拟化方法

  -    屏蔽执行环境

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

  -    访问控制

• EVITA的车载协议

• 原则：

1. 对依赖外部数据的应用程序建立信任；

2. 基于以下两类加密材料

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

   -    已被外部信任的第三方证实的

3. 基于整个汽车平台的完整性

• 设计目标（Design Goals）：

1. 高效的-用于安全的开销小

2. 可扩展的-ECU的数量

3. 网络无关的-可用于CAN,FlexRay,Ethernet等

4. 可移植的-适用于不同的运行环境（RTE）

• 方法：

1. 面向服务的分层协议设计

2. 基于仿真模拟的费用估计

3. 结合对称加密和非对称加密

• 内部通信（ECU之间）

• 一对多的安全通信

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

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

• 数据的传递和处理

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

• 安全会话

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

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

  -     较大的有效载荷

• 在通用传输协议的基础上，EVITA项目额外提供以下：

  -     安全有效载荷

  -     一对多通信

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

• 车载系统

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

  -     执行元素（CPU,HWA）

  -     通信元素（总线）

  -     存储元素（RAM,flash）

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

• 软件元件

  -    在CPU上执行

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

1. 需求识别

2.  结构规范

3. 安全相关的协议规范

4.  整个系统安全性能的验证包括：

   1） 性能测评

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

   2） 攻击分析

       a.放大视图法

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

       b.全局合成法

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

5. 验证方法

   -  考虑输入（如：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和硬件加速器

       - 总线

• 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的缩写

• 数据的缩写

 抽象化成流程图：

• 进程1：

• 进程2：