专注于车载信息安全和预期功能安全技术研究
电话:+86 21 62655001
您的位置: 网站首页 > 学术前沿
2021-06-21 15:25:31

欧盟EVITA项目预研 第一章(三)

来源:学术前沿 浏览次数:162 点赞数:2

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

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



车载信息安全协议

  • 抽象网络结构如下:

图片

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

图片

-       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和硬件加速器

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产生可达图

    - 最小化可达图

    - 搜索包含attackOKattackKO操作的轨迹

  • 可达图(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

 抽象化成流程图

图片


  • 进程1:

图片

  • 进程2:

图片