SysML-Sec: A Model-Driven Environment for Developing Secure Embedded Systems

SysML-Sec：用于开发安全嵌入式系统的模型驱动环境

摘要

我们介绍SysML-Sec，这是一个新的SysML环境，旨在使安全专家在嵌入式系统设计和开发的所有方法阶段与系统设计人员合作。 SysML-Sec还旨在支持评估安全性对安全性的影响。安全性和安全性问题在扩展的SysML图中捕获，该图根据围绕体系结构的软件/硬件分区的迭代过程进行了详细说明。捕获的需求可以衍生到安全性和加密机制以及可以正式验证的安全性属性中。

SysML，安全性，嵌入式系统，模型驱动的工程。

1 介绍

围绕ModelDrivenEngineering（MDE）的大多数贡献现在都适用于设计安全，复杂，分布式和实时嵌入式系统的方法和建模环境。这些环境通常处理时序约束，调度，资源分配和并发性的分析。相反，长期以来，人们一直只考虑反思安全性，尤其是在发现严重的僵局之后。安全问题尤其是直到最近才成为嵌入式系统中的主要问题。但是，现代嵌入式系统的大小，异构性和通信功能使其必须开发合适的工程环境来更明确地定义安全目标和威胁并实施对策。系统的复杂性还使得在对特定实现做出任何承诺之前，有必要验证要求是否与候选设计相符并满足要求。

安全意识MDE领域中的贡献通常针对特定的方法论阶段（例如，需求[NNY10]，验证[Tou93]）或特定应用领域（例如，基于加密协议的证明[ABB + 05] [ORR00]），或者着眼于安全机制的即时建模[Jür02] 而不是根据明确定义的方法来定义这些机制。

本文介绍了SysML-Sec，这是一个具有更全面方法的新SysML环境，它同时介绍了针对安全事项的定制SysML图和相关方法。我们希望SysML-Sec能够使安全专家与系统设计人员一起干预嵌入式系统的设计和开发。 SysML-Sec方法和图表已在FP7欧洲项目EVITA的范围内开发和试验。 EVITA定义了用于汽车嵌入式系统的安全架构。该架构的定义，设计和验证是通过本文介绍的方法进行的。因此，为此目的考虑了20多个用例（特别是紧急制动用例），本文中的图表直接摘自该案例研究。

2 嵌入式系统中的软硬件划分

以软件为中心的系统通常以V周期进行设计，其构建阶段（需求，分析，设计，实施）随后是验证阶段（例如测试，形式证明）。对于嵌入式系统，显然只有在将功能划分为软件和硬件后，V周期才能启动。系统分区通常取决于Y图表方法[BWH + 03]。该过程的结果是针对该特定系统的关键标准（例如成本，性能等）的最佳硬件/软件体系结构，包括：

首先将应用程序描述为抽象的通信任务：任务代表的功能与其实现形式无关。
硬件架构被描述为一组抽象执行节点（例如，具有操作系统和中间件的CPU，硬件加速器），通信节点（例如，总线）和存储节点（例如，存储器）。
映射模型定义如何将任务和任务之间的通信分别分配给计算和通信/存储元素。例如，任务映射的硬件加速器是硬件实现的功能，而映射在CPU上的任务是软件实现的功能。

我们已经定义了几个基于MDE的环境来支持嵌入式系统的开发（DIPLODOCUS UML配置文件[AMAB + 06]，AVATAR [ADSS11] SysML环境和TEPE [KAD11]环境）。所有这些环境都在免费软件TTool [Apv13]中实现。 TTool自动执行模型的形式验证和仿真，并向UML图提供实时反馈。 SysML可以与这些环境和工具一起使用，以描述上面讨论的分区问题以及性能和安全要求。

这些问题无法解决安全问题。我们设计了SysML-Sec环境，以便能够将此类问题与分区要求一起描述，如[RIA13]中进一步讨论的。特别是，我们的扩展弥合了安全性和攻击的面向目标的描述与基于软件/硬件体系结构（及其模型驱动的分析）的资产细化表示之间的鸿沟。

3 SysML-Sec方法

越来越多的嵌入式系统已成为一种通信工具，它们之间或与后端系统之间的新交互功能越来越强大，因此暴露于犯罪分子之中。例如，攻击显示可能无法置顶置顶盒，例如Microsoft的XBox [Hua02]或ADSL路由器[Ass12]，移动设备[Ess11]，航空电子设备[Tes13]或汽车系统[HKD11]。这些安全问题中的许多问题反映了对低级漏洞的利用（通常可以通过适当的编程实践和特定的组件测试来解决），或者由于对功能或安全性组件对硬件体系结构的映射缺乏足够的了解而导致设计漏洞。我们认为，SysML-Sec模型驱动工程方法可以双向执行适当的系统分析，并通过以下方式描述安全威胁和安全目标：

在整个嵌入式系统生命周期中指导并增强系统工程师和安全专家之间的协作。这就是我们采用OMG标准，尤其是SysML的原因，这些标准在当今的嵌入式系统世界中非常普遍。
提供与使用的MDE方法兼容的安全威胁和安全要求的详细表示，并可以采用逐步完善的方法来定义功能和安全体系结构。这种改进还应该有可能弥合最初的高层次要求和定义精确而详细的安全机制之间的差距。
将软件/硬件代码签名与安全问题的处理结合在一起。我们认为这个特定的设计目标是嵌入式系统领域的关键。

SysML-Sec方法采用三个阶段的方法，首先处理系统分析，然后处理软件设计，最后处理系统验证，如以下部分所述。

4 系统需求工程与分析

安全需求和威胁分析通常被视为IT系统中风险分析的序言。此过程通常旨在决定是否在系统中引入安全性对策，这意味着要增加成本。对于嵌入式系统，我们认为安全性分析还对系统架构及其实时性能产生重大影响：因此，安全性要求和威胁分析应在分区迭代过程中进行。我们还声称，在说服日益复杂的嵌入式系统的设计人员其安全体系结构的一致性和详尽性方面，安全分析应发挥重要作用，至少在已识别的威胁和风险模型方面。

4.1 迭代安全性/系统代码签名过程

系统分区，安全要求和威胁会根据一种或几种典型用例逐步得到完善。因此，以下阶段从初始架构开始进行迭代，以达到令人满意的改进水平：

初始架构映射。这些用例中突出显示的系统功能首先被建模为任务。功能之间的交换以信息流和事件流为模型。还捕获了基于事件的通信，以控制信息流。然后可以将任务和通信映射到系统的架构草案。设计师的经验对于确定架构的初稿起着关键作用。

架构分析系统资产在架构元素（处理器，软件，传感器，硬件加速器，通信通道）之间进行标识，并且首先涉及通用组件，例如：“所有系统总线”。当体系结构变得更加详细时，资产更有可能被细分为特定元素。此处采用的硬件/软件分区和功能映射在定义现有资产的类型（及其后的漏洞）中起着关键作用。

**安全问题识别。**所选资产的威胁和安全漏洞应尽可能描述攻击者应达到或超过的能力以及攻击的源头（本地，远程，通过特定接口）。遵循EVITA案例研究[Rea09，HAF +]中更详细描述的方法，SysML安全环境支持对风险的评估。我们还根据安全目标实施了对威胁覆盖率的自动检查。基于风险分析，还应确定映射到威胁的安全目标并确定其优先级。安全目标可能来自（1）来自系统期望的安全标准或属性，或者（2）来自未解决的威胁或对资产的攻击，或者（3）来自在迭代过程和详细程度时对另一个安全目标的定义。架构发生了变化。在进一步的迭代中，可能需要更新因体系结构更改而弃用的安全目标。

体系结构优化。 体系结构的精炼源自对体系结构组件的更详细的描述，随着系统及其使用的更加精确地已知（例如，新的通信渠道，将执行环境精炼为OS /中间件/应用程序层等）。这也可能是由于将需求映射到系统信息流中而造成的，这些信息流通常分布在多个硬件元素之间。如果架构和安全性要求不兼容，例如，如果安全性机制的性能开销过高，则优化阶段可能会失败。还应该执行一致性检查，以确保安全目标不与针对同一资产表达的另一要求冲突。失败表明分析应回溯到优化的前一个阶段。

4.2 Diagrams

在我们提出的框架中，使用硬件节点上的任务分配来进行分区。使用SysML块对任务和硬件节点进行建模。使用SysML“分配”关系对分配进行建模。

安全需求在SysML需求图（RD）中建模。 RD的主要运算符是用于定义需求之间关系的需求包含和派生依赖性形式。包含关系按照层次结构描述子需求，并使复杂的需求分解为包含其子需求的需求，而deriveReqt确定支持源需求的多个派生需求。这些需求通常表示需求层次结构中的下一层。引入了安全性需求原型，以明确区分系统的功能性需求和安全性需求，同时在单个环境中对功能性需求和非功能性需求进行建模。此外，定义了Kind参数以指定安全要求的类别（机密性，访问控制，完整性，新鲜度等）。

攻击树可以用稍微定制的SysML参数图建模。攻击被建模为嵌入到代表攻击目标的块中的值。攻击可以与逻辑运算符（如OR，AND）以及时间因果运算符（如AFTER）链接在一起，后者被认为对于描述嵌入式系统中的攻击特别有用。可以将它们在不同参数图中的实例链接在一起，以便评估特定漏洞的影响以及在风险评估阶段解决该漏洞的需求。攻击也可以标记为根攻击，这意味着该攻击位于树的顶部。最后但并非最不重要的一点是，可以将攻击与需求联系起来，从而可以自动检查攻击的覆盖范围。

在紧急制动（或本地危险警告）用例的范围内，图1给出了功能映射的示例。表示两个电子控制单元子域。左侧的机箱安全控制器，右侧的车身电子模块。每个子域都有一个主处理器，一个本地闪存，一个本地主存储器，一组硬件加速器以及一个通往主系统总线的桥。功能既可以映射在处理器上（这些功能要通过软件实现），也可以映射在硬件加速器上（功能可以用硬件编码）。任务之间的通信也将通过总线和内存进行映射，以突出显示数据传输。

5 软件设计

5.1 方法论方面

软件设计定义了分区阶段在处理器节点上映射的所有功能的体系结构和行为。从安全的角度出发，设计旨在精确确定如何在分区阶段定义的硬件体系结构之上执行面向安全的软件机制来满足安全要求，并验证该设计确实满足了在分区阶段确定的要求。分区中表达的需求是非正式的，并且涉及资产：因此，需要对其进行完善，直到其表达直接涉及设计元素（例如，属性，方法，交换的消息，状态等）。一旦完善，它们便构成了设计要验证的安全属性。 SysML-Sec扩展了SysML的方法，可以显式地对安全机制和属性进行建模。

5.2 安全设计扩展

SysML-Sec设计是基于SysML框图和状态机图进行设计的，具有多种功能扩展，并在pi演算（过程代数）中正式定义。尤其是，我们假设一个Dolev-Yao攻击者模型，即仅在块之间交换消息，然后将消息丢弃，对块的属性相反。该攻击模型足以描述从系统外部或内部对嵌入式系统组件之间部署的协议的攻击。但是，它既不旨在捕获对硬件的物理攻击，也不旨在利用多个组件的漏洞。由于通信通道可能已在分区阶段映射到安全或非安全总线上，因此，如果攻击者可以窃听，我们可以使用公共标签标记块之间的链接，否则可以使用私有标签标记块之间的链接。而且，SysML-Sec块可以定义与密码算法相对应的一组方法（例如，加密），以便能够描述建立在这些算法之上的安全机制，例如密码协议。块还可以预共享值，这是设置密码协议通常需要的功能。 SysML-Sec为此目的引入了特定的pragma（InitialSystemKnowledge和InitialSessionKnowledge）。

5.3 Security Properties

已基于SysML参数图[KAD11]定义了一种专用语言来描述常见的复杂安全属性。相反，安全属性通常可以用类型（例如，机密性）和与该类型相关的设计元素（例如，块的属性的机密性）来定义。这种简单性要求一种基本的建模解决方案，该解决方案不基于复杂的图或运算符。我们的解决方案依赖于框图注释中提供的实用性：可以在此级别直接表达机密性和真实性。

例如，真实性说明指出由块block2接收的消息m2必须先于块block1在消息m1中发送。以下示例描述了这种情况：真实性block1.s1.m1 block2.s2.m2此真实性杂注指定两种状态：发送者块之一，即block1的一个状态s1，以及block2的一个状态s2。同样，在块1的状态机图中，s1对应于发送m1之前的状态。类似地，s2对应于消息m2已被接收并被接受为真实之后的状态。

图2说明了EVITA体系结构中定义的密钥分发协议的SysML-Sec软件设计。该协议将会话密钥分布在车辆中分布的一组电子控制单元（ECU）中。语法在图的左上方给出：该知识在ECU和密钥主控（KM）之间预先共享，并且具有两个属性：与ECU1预共享的密钥的保密性，以及从ECU1发送给KM的消息的真实性。下面的块为ECU初始化密钥分配（ECU1），密钥主控和另一个ECU（ECUN）建模。

6 系统验证

可以从映射模型（例如，所选硬件体系结构的性能评估：CPU和总线的负载），设计模型（安全性和安全性证明）或从设计模型自动生成的可执行代码（安全性和安全性）执行验证。测试）。模型转换已定义为将SysML-Sec模型转换为正式规范。整个过程可以在TTool中无缝实现，即，由于模型转换和回溯到模型是完全自动化的，因此TTool用户无需了解基础形式技术。可以从分区或软件设计模型中进行证明。从分区模型中，可以评估安全机制对实时约束（例如，延迟）的影响。从SysML-Sec设计中，正式的证明依赖于ProVerif的安全性。 ProVerif [Bla09]是一个工具包，在Dolev-Yao模型下，依赖于Horn子句解析来通过密码协议自动分析安全性属性。 ProVerif接受输入一组Horn Horn子句，或者输入Picalculus中的规范和一组查询。 ProVerif输出是否满足每个查询。在后一种情况下，ProVerif尝试识别一条轨迹，以解释未满足查询的结论。图3描绘了在TTool中成功验证的图2中建模的机密性和真实性属性。尽管我们可以指定任何安全性要求，但是我们目前仅支持对可以用这两个安全性属性表示的形式要求的形式验证。

7 相关工作

在[NNY10]中，Nhlabatsi等人。将软件系统中的安全需求工程工作按照四个维度进行分类，即：（1）基于目标的方法是使用这种方法来建模，指定和分析安全要求的目标，这些安全要求是使用通用模式将目标的组织化定义为一组子目标。（2）基于模型的方法：相反，这些方法论着重于将安全性映射到软件体系结构。（3）面向问题的方法侧重于攻击的表达和基于威胁的安全需求（滥用框架，滥用案例）的得出。（4）面向过程的方法最终主要针对现有设计的风险分析，并遵循相当严格的瀑布方法进行工程设计，但并未解决井的设计探索和改进问题。我们的方法将基于目标的安全需求描述与模型驱动的系统体系结构工程结合在一起，并验证安全属性的健全性或它们在安全方面的无害性。在这方面，它与Nuseibeh [Nus01]提倡的TwinPeaks方法具有一些相似之处，尽管后者并不针对硬件系统。并非像TwinPeaks所建议的那样，在需求和体系结构之间进行简单的螺旋交替，而是在软件的Y-Chart建模及其与硬件组件的映射，资产和威胁的识别以及安全需求的识别之间进行交替。

UMLsec [Jür02]具有如上所述的基于模型的方法，它定义了如何将安全协议描述和安全属性集成到UML框架。但是，设计元素和安全性属性在相同的图上以及功能和非功能需求上混合在一起。

评估嵌入式系统的安全性主要依赖于形式化方法。例如，[Tou93]建议使用概率分析方法来验证密码协议。在更近的版本中，[DBTS]在Isabelle / HOL定理证明者中嵌入了一阶线性时序逻辑（LTL），从而使对系统及其安全属性进行建模成为可能，但不幸的是，这导致了无法轻松重用的特定模型。 [MP08]混合了正式和非正式的安全属性，但是整个验证过程不是完全自动化的，再次需要特定的技能。

8 总结和未来工作

嵌入式系统的复杂性以及上市时间和软件工程方面的限制要求采用具有自动化和简化验证功能的面向用户的工具来满足工程安全要求。我们的建议SysML-Sec专门解决了系统设计和开发各个阶段的需求。它基于一种流行且友好的语言（OMG的SysML），并受到依赖公认的安全性验证工具包（ProVerif）的开源工具包（TTool）的支持。我们还开发了一种使用SysML-Sec图的方法，该方法已进行实验以定义安全的汽车嵌入式系统。