SysML-Sec A model Driven Approach for Designing Safe and Secure Systems

SysML-Sec用于设计安全系统的模型驱动方法

摘要

安全性是开放式的，可以攻击嵌入的系统，并且必须仔细评估顺序才能确定对安全性的威胁。随后保护系统安全，即将安全机制集成到系统体系结构本身会影响系统的安全性，例如，由于计算和通信延迟的增加，可能会错过最后期限。 SysML-Sec通过模型驱动的方法解决了这些问题，该方法可促进系统设计人员与安全专家在所有设计和开发阶段（例如需求，攻击，分区，设计和验证）的协作。 SysML-Sec的中心点是其分区阶段，在此阶段中，针对需求和攻击，可以联合和迭代地探索安全相关和安全相关的功能。分区后，系统将根据系统的功能和安全机制进行设计，并从安全和安全角度进行正式验证。本文通过对现有汽车系统中添加的安全机制进行评估，说明了整个方法。

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

1 介绍

嵌入式系统和网络物理系统逐渐影响我们的日常生活，信息系统和工业系统。因为这些系统本质上是连接的，所以它们很容易受到攻击。在类似的连接系统上只有很少的例子，我们可以提到Microsoft XBox（Huang，2002），ADSL路由器（Assolini，2012），移动智能电话（Maslennikov，2010）（Esser，2011）（Apvrille和Strazzere，2012），航空电子系统（Teso），2013年）或汽车系统（Teso，2013年），甚至家用电器，如冰箱，最近通过僵尸网络感染LG冰箱所证明（Proofpoint，2014年）。这种攻击还针对工业系统，其传感器越来越多地与易受攻击的信息系统连接，如Stuxnet，Flame或Duqu（Maynor，2006）攻击所证明的那样。此类攻击的目标当然是具有多种目标的此类攻击，例如恐怖行为和勒索软件。

此类系统在代码大小，分布和异构性等方面的复杂性是它们面临的风险的主要因素。我们认为，从最开始的开发阶段就考虑安全性，包括软件和硬件组件，都可以降低系统在安全性和安全性方面面临的风险。我们还认为，安全性和安全性应该一起设计和验证，也就是说，应该使用相同的模型，并且应该明确建立安全机制对安全相关功能的影响。我们的解决方案依赖于名为SysMLSec的模型驱动环境。 SysML-Sec涵盖所有设计和开发阶段，包括需求捕获，攻击等式，功能模型，硬件/软件分区，软件组件设计以及安全性和安全性验证。验证本身应在分区和设计阶段进行。在第一种情况下，目标是评估所选硬件/软件体系结构的有效性，以同时支持安全性和安全性要求，并抵抗已识别的攻击。在第二种情况下，验证应密切调查设计选择是否符合安全性要求。

SysML-Sec已在（Apvrille and Roudier，2013）中发表。本文着眼于一个新的方面，即SysML-Sec如何也可以用于评估面向安全的设计对具有重要方面的系统（例如，重要的嵌入式系统或攻击可能导致严重的经济损失的系统）的影响。例如新的互连信息系统，例如云服务。

本文的结构如下。第2节重点讨论攻击对安全至关重要的系统的影响。第3节讨论了在安全广告安全系统的开发过程中有效考虑系统体系结构和要求的不同建模方法。然后，我们分别在第4节和第5节中介绍SysML-Sec框架的方法论和验证过程，并重点强调安全性和安全性特性之间的关系。第6节给出了基于自动化的案例研究。第7节总结了本文。

2 攻击的影响

执行攻击依赖于对低级漏洞（例如缓冲区溢出）或设计漏洞的利用。低级漏洞通常可以通过良好的编程习惯来处理，也可以通过使用有效的安全测试（例如，不同的模糊测试）来处理。相反，设计错误通常来自不良的需求和攻击捕获，或者来自对硬件/软件组件（包括这些组件实现的安全机制）的不合理分区。不幸的是，一旦系统发布，这些错误就很难纠正。此外，安全专家通常使用的安全工具例如 ProVerif（Blanchet，2009年）和AVISPA（Armandoetal。，2005年）并未考虑硬件/软件分区。

古典信息系统仍然是攻击者的广泛目标。尽管如此，包含通信嵌入式设备的信息系统的特殊性使它们成为攻击者更为“有趣”的目标。我们可以提到与这些攻击有关的三种危险：

如果攻击依赖于硬件漏洞，则通过软件更新来纠正（即打补丁）系统可能非常困难，甚至是不可能的，尤其是如果大多数功能是通过硬件组件（例如，硬件加速器或网络过滤技术。对于通常的信息系统，“简单”的软件更新和系统重新启动通常可以解决该问题。
更新嵌入式系统的软件比更新例如PC的软件要复杂得多。例如，要修补车辆的软件，有必要向所有者发送一封信，该信随后将把汽车带到维护车库。嵌入式系统的用户最近也很少使用其系统进行更新，如最近使用IP摄像机演示的那样。相反，更新PC或服务器已成为一种常见的做法（著名的“星期二补丁”），并且可以通过自动化方式进行远程处理。
攻击对安全关键系统的影响可能比对其他类型系统的影响大得多。而且，一旦攻击者设法破坏了其中一个互连元素，信息系统与智能对象之间日益增长的互连关系便为攻击者提供了更多机会，使其非法进入那些系统。例如，对于LG冰箱攻击（Proofpoint，2014）最近证明的僵尸网络（DoS攻击，垃圾邮件）或进行加密攻击就是这种情况。

3 系统体系结构在开发安全系统中的基本作用

根据我们自己的经验，我们认为必须首先对主要系统架构元素进行建模，以便更好地捕获和分析对系统的潜在攻击。

3.1 软硬件划分

以软件为中心的系统通常以一个V周期进行设计，该V周期包括以下阶段：需求确定，软件分析，软件设计，实施。然后，在这些阶段中的每一个阶段之后，都有一个相应的验证状态，该状态通常依赖于测试，模拟和形式化验证技术。对于嵌入式系统，只有在指定了要实现的软件功能之后，这种方法显然才适用。换句话说，只有在执行了软件和硬件分区后，V周期才能启动。

系统划分（又称“设计空间探索”）是一个过程，用于分析各种功能等效的系统规范实现。它通常依赖于图1所示的Y图方法（Balarin等，2003）：

首先将应用程序描述为抽象的通信任务：任务代表的功能与其实现形式无关。
有目标的体系结构与任务无关。通常使用一组执行节点（例如CPU），通信节点（例如总线）和存储节点（例如存储器）来描述它们
映射模型定义了如何分别将应用程序任务和抽象通信分配给计算和通信/存储设备。例如，分配了硬件加速器即硬件实现的功能，而映射到CPU的任务是软件实现的功能。

理想地，Y图表方法的结果应该是针对该特定系统的关键标准（例如，成本，面积，功率，性能，灵活性，可靠性等）的最佳硬件/软件架构。此过程可以由经验丰富的工程师手动执行，也可以由特定的工具箱自动执行，例如（Balarin等，2003）。此分区步骤至关重要。确实，如果由于问题（性能，功耗等）的发现较晚而使关键的高级设计选择无效，那么这可能会导致重新设计的成本过高，以及市场的可用性不足。

3.2 尺寸标注

在某些高度关键的系统中，用于设计空间探索的模型不适用于计算和分析最坏情况执行时间。相反，基于网络演算的基于维度的技术（Leboudec和Thiran，2001）适用于计算最坏情况的执行方案。这些技术通常用于定义航空系统的体系结构。尺寸模型是我们整体工具包的一部分（Apvrille等，2010），即使尚未在SysML-Sec中使用。

3.3 模型驱动工程

模型驱动工程可能是近十年来建模方法的主要贡献。 MDE面向系统分析，设计，仿真，代码生成和文档。 MDE通常依赖于UML语言和元建模技术来定义领域特定的语言。例如，OMG的模型驱动体系结构专门针对两个抽象级别，即平台无关模型（PIM）和平台特定模型（PSM）：因此，MDE显然将嵌入式系统作为目标。 OMG也已将其定义为更多专门解决嵌入式系统的问题：SPT（OMG，2005年）和MARTE（Vidal等人，2009年），但它们都没有解决需求建模问题。相反，SysML OMG配置文件（OMG，2012年）显然考虑了具有显式建模功能和图表的要求，但忽略了嵌入式系统固有的一些问题，例如分区问题。

还提出了其他方法来开发面向软件的系统，例如极限编程（XP）（Beck and Andres，2004）或敏捷软件开发（Waters，2012）。但是，他们对软件的关注意味着他们完全忽略了分区问题。它们也使可追溯性和修复极其困难，这也是因为需求大多与设计过程分开。

4 规范系统的Security需求

与安全性相反，安全性和隐私通常是经过重新考虑的新连接和分布式信息系统（例如，云服务）和嵌入式系统。因此，通常在发现安全漏洞后，在系统已经发布后就会出现安全需求。但是，只要可以利用这些漏洞来影响经济或安全相关组件，这些漏洞就具有至关重要的意义。

4.1 安全目标和威胁

许多研究工作已经解决了安全需求和威胁的建模和分析，主要是在信息系统范围内。 Nhlabatsi等。（Nhlabatsi等人，2010）将它们分为四类：面向目标的方法，模型驱动的方法，面向过程的方法和最后针对问题的方法。前两个是最接近SysML-Sec的两个。 KAOS是众所周知的基于目标的方法（Van Lamsweerde，2007），它依赖于安全目标和反目标的显式模型。 TwinPeaks（Nuseibeh，2001年）还遵循一种目标导向的方法，在目标和系统体系结构之间进行了反复的分析。 UMLSec是一种面向模型的方法。它包括具有安全机制（包括密码协议）的规范和验证分布式系统的工具。面向模型的方法被认为更适合于安全机制的设计，但是面向目标的方法提供了一种更好的方法来分析第一次设计迭代中的安全性需求。

4.2 SysML-Sec：基于SysML的面向模型的方法

SysML-Sec的第一个目标（Apvrille和Roudier，2013年）是促进系统设计专家与系统安全和隐私专家之间的协作和交流。此外，SysML-Sec打算涵盖这些系统的所有开发方法论阶段。 SysML-Sec结合了用于捕获需求的面向目标的方法和用于系统体系结构和威胁的面向模型的方法。与TwinPeaks（Nuseibeh，2001）相反，SysML-Sec遵循Ychart方案（Balarin等，2003）及其底层分配技术。后者有助于识别受保护的资源以及资源，安全要求和安全要求之间的联系。

4.3 方法论

SysML-Sec方法首先基于基于YChart的系统分析，然后基于众所周知的V循环在软件设计阶段进行。图2给出了这种方法。

分析阶段旨在识别和分析需求和攻击，以及识别主要功能（“应用程序”），候选硬件体系结构和主要功能过执行节点（映射）的映射。在功能阶段，使用仿真和（形式化）验证来确定与安全相关的问题，例如死锁情况，错误状态的不可到达性等。功能模型是不定时的，这意味着无法进行性能研究。然而，功能在执行节点上的映射为前者提供了逻辑上和物理上的执行时间。因此，映射后仿真和形式验证旨在证明所选硬件体系结构上的系统性能，包括对延迟，处理器和总线的负载以及通信时间的研究。显然，结果是由于应用程序的逻辑部分，底层硬件的行为方式以及安全机制所致。例如，给定的安全协议可能会影响总线负载，加密功能可能会影响处理器负载：两者都可能因此增加整个系统的延迟。例如，在硬件加速器上或在通用处理器上映射密码功能的映射方案也会影响系统等待时间。因此，性能研究实际上打算一起研究在不同条件下映射的安全和安全功能。这项研究的结果是一种既符合安全性要求又符合安全要求的硬件/软件体系结构，并且可以抵御攻击，并可以达到一定的风险级别。

设计阶段的目标是设计软件组件，即前一阶段映射到处理器的功能。在设计过程中，逐步完善软件组件，直到可行的可执行代码生成点为止。该改进还包括与安全有关的功能，例如安全协议。在第一个优化中，可以使用仿真来调试模型。当模型的大小合理时，也可以使用形式验证来评估安全属性（例如，给定状态的可达性或其活动性）和安全性属性（例如，给定块属性的机密性，一个消息）。如果模型太大而无法验证，则使用模型到代码的转换来执行安全性和安全性测试。本文未涉及设计阶段，但在（Apvrille and Roudier，2013）中进行了描述。

4.4 工具包

免费且开源的TTool软件支持所有SysML-Sec方法论阶段，包括模型捕获及其仿真和验证。实际上，TTool是一个多功能的工具箱，其主要优点是提供一种按按钮的方法来执行仿真和模型的形式证明。可以自动执行安全性和安全性证明。在分区阶段，TTool依赖于DIPLODOCUS UML配置文件（Apvrilleetal。，2006），即使本文中介绍的安全性方面专门针对SysML-Sec。需求，攻击，软件设计以及所有内容均由AVATAR捕获和分析（Apvrille和De SaquiSannes，2013年），涵盖了V开发周期。可以使用TTool的集成模型检查器和仿真器，也可以使用外部正式验证工具包（例如，正式验证和仿真）来进行正式验证和仿真。 UPPAAL（Bengtsson和Yi。，2004），CADP（Garavel等，2007）和ProVerif（Blanchet，2009）。

5 面向Safety和Security的验证

面向模型的方法有利于模型的早期验证。 SysML-Sec支持从分区模型或设计模型进行此类验证。 TTool的按钮验证方法支持验证：TTool可以将模型转换为正式的规范。 TTool拥有自己的模型检查器，但它也可以依赖于外部证明。一旦获得验证结果（满足属性，不满足属性，无法证明属性），则对模型进行结果批注。形式验证更可能用于证明特定和精确的安全性和保密性，例如，给定数据是机密的。每当必须研究安全机制对安全属性（例如，与延迟相关的属性）的影响时，更可能使用模拟。这种影响主要在分区阶段进行研究。

5.1 Safety Properties

这些验证与以下模型有关：功能模型，分区模型和设计模型。可以通过使用仿真技术（Apvrille和De Saqui Sannes，2011），形式验证技术（Apvrilleand De Saqui-Sannes，2013）（Bengtsson和Yi。，2004）或生成可执行代码（仅来自经过改进的设计）来证明属性。模型）并对该代码执行测试（Apvrille和Becoulet，2012年）。从设计图来看，安全证明同时考虑了安全机制和安全机制，因为后者会影响软件组件的行为，例如采用给定的执行路径。

系统架构和行为通常使用图形语言建模。相反，用于表达属性的语言仍主要依靠文本语言，例如 LTL / CTL或从那些语言衍生而来的语言。但是，在SysML-Sec中可以使用SysML参数图对所有逻辑和时序属性进行建模（Knorreck等，2011）。

5.2 Security Properties

在设计阶段，可以进行机密性和真实性属性的形式证明。如果可能，必须首先将安全性要求重新定义为在SysML-Sec框图中作为实用程序建模的机密性和真实性属性。然后，TTool可以将设计图转换为pi演算中面向Security的形式规范（Pedroza，2013年）。可以将该规范以及要证明的机密性和真实性作为ProVerif的输入（Blanchet，2009）。

5.3 Safety和Security, safety vs. security

在分区阶段评估Safety与Security之间的关系并不常见。但是，我们认为，应按照SysML-Sec方法论的建议，在开发周期中尽快解决此问题。 Eames和Moffet（DP Eames和Moffett，1999），以及最近的Pi’etre-Cambac´ed`s（Pietre-Cambacedes和Bouissou，2013）和Raspotnig（Raspotnig和Opdahl，2013）提出了解决两者之间联系的方法。安全性和安全性。更准确地说，（Pietre-Cambacedes和Bouissou，2013年）和（Raspotnig和Opdahl，2013年）旨在明确描述这些要求之间的冲突，并提供“增强”，即，使用不同的范围以相同的方向驱动体系结构模型的要求。

就像我们在下一节中显示的那样，SysML-Sec可以依靠验证技术来评估安全机制在分区阶段的安全性方面的兼容性。在设计阶段可以进行类似的研究。

在分区阶段，根据系统等待时间和平台的使用情况（例如必要的计算能力，总线负载以及对实时期限的尊重）对机制进行评估。分区模型通常通过在系统中生成已知的平均流量进行验证，然后引入安全机制，以评估后者对前者的影响。 SysML-Sec模型的完善导致引入了细粒度的加密功能，其中要证明的属性更有可能是安全协议给定状态的可达性。因此，在设计阶段，我们还依靠证明者来评估需求和攻击范围的一致性。

6 实例：通信车辆的安全性和安全性分析

本节说明了SysML-Sec在识别需求和攻击以及定义安全体系结构方面的使用。用作案例研究的汽车系统取自欧洲FP7EVITA项目（Kelling等，2009）。 EVITA为汽车通信系统定义了第一个通用安全体系结构。该体系结构包含与CANorFlexraybus互连的安全关键的ECU（电子控制单元）。出于经济原因（可能免费激活可选功能，偷车），可能出于犯罪目的而攻击汽车系统。汽车系统与信息系统（路标，通行费等）和Internet的互连将提供对这些系统进行攻击的新方法。

在图3中给出了参考汽车架构。它基于多个领域（动力总成，底盘和安全，通信单元，主机等）。域可能包含几个子域，每个子域都包含多个总线和处理器。主CAN / FlexRay总线将所有ECU桥互连在一起。最后，通信和主机具有外部接口（蓝牙，LTE等）。

现在，我们将SysML-Sec方法应用于参考架构，并添加了安全机制。这种机制是在域和子域之间分配加密会话密钥。 ECU1询问“密钥主控器”以生成会话密钥，以便以安全方式与该会话的其他域ECUN通信。

6.1 Security需求

安全需求在SysML需求图中捕获。安全需求被定型为<< SecurityRequirement >>，并包含一个额外的领域（机密性，访问控制，完整性，新鲜度等）。可以使用需求（包含，派生）之间的通常SysML关系，特别是在不同抽象级别之间跟踪需求。图4给出了安全要求的摘要，涉及防止将错误的命令注入系统。主要要求被定义为涉及系统功能的ECU之间所有通信的真实性，完整性和新鲜度要求。

6.2 威胁和攻击

攻击通常通过攻击树来捕获（Schneier，1999）。这样的树可以将攻击有效地分解为子攻击。但是，它们不适合于复杂场景的描述。然而，当前导致对嵌入式系统的攻击通常由复杂的场景组成，有时涉及复杂的逻辑和时序关系，例如Zeus / Zitmo攻击利用了限时认证令牌。

我们根据SysML参数图确定攻击模型。这些方程式是将子攻击链接在一起的一种约束条件，以建立更复杂的攻击。

攻击是通过SysML块的“属性”捕获的。由于块代表系统的资源，因此获得了对要保护的建筑元素的直观重视。约束用于将攻击关联在一起：<< OR >>，<< AND >>，<< SEQUENCE >>，<< BEFORE >>，<< AFTER >>。每个约束具有名词性对应关系，例如带有结果攻击的两个攻击a1和2isa =a1∨a2之间的<< OR >>方程。攻击也可以与需求相关联，反之亦然。

图5描绘了我们案例研究的简化攻击。攻击者的主要资源是AutomotiveECUsandBuses，他们希望窃取汽车（Steal car root攻击）。为了成功执行该攻击，攻击者需要连接系统总线，以便能够打开门，然后启动引擎。实际上，打开门是可选的，因为攻击者可以决定打破窗户，因此与门相关的攻击是可选的（请参阅序列约束中关于（2）和（3）的括号）。要访问系统总线，攻击者可以通过调试接口（OBD-II插头）与远程接口（蓝牙，Internet）连接。对于这两种解决方案，他都需要绕过汽车系统防火墙。

6.3 软硬件划分

SysML块实例图用于描述功能及其关系。功能之间的数据和事件流可以通过端口和链接来描述。从语义上讲，数据流不对那些数据的值进行建模，而仅对交换数据的数量进行建模：这极大地简化了抽象级别的证明和模拟（注意：验证同时考虑了软件和硬件组件）。同样，在复杂系统的范围内，我们已经证明这不会影响分区决策（Jaber，2011年）。

体系结构和映射模型依赖于UML部署图，但是SysML或MARTE的分配机制可以用于此目的。功能块的映射及其通信基于添加到部署节点的工件，后者是要保护的资产。它们也可能在攻击图中显示。

为了评估安全机制的影响，对两个不同的划分执行了两次模拟。在没有安全机制的情况下，在汽车系统上进行第一次仿真。仿真的目的是评估CAN总线负载，因为它负责在域之间传递紧急和非紧急消息。没有安全性的平均负载为40％。

第二个仿真评估密钥分配协议如何影响先前系统的性能。为此，对汽车系统的一个子集进行了建模：加密硬件加速器（HSM-硬件安全模块），ECU请求会话密钥（ECU1），密钥主控（KM）和将参与该会话并需要会话密钥的ECU。仿真显示，在密钥分发期间，主CAN总线上的负载要高得多，并且对于与密钥分发无关的所有类型的流量，观察到的延迟都高得多（Schweppe等人，2011年）：这种安全机制确实会影响安全性系统的。为了解决该问题，我们尝试的一种解决方案是将认证信息拆分为多个连续的消息。

7 总结和未来工作

现在，许多攻击是在嵌入式系统和网络物理系统上进行的。上市时间短，加上强大的安全性要求，鼓励为这些系统引入新的开发方法。

SysML-Sec在相同的开发周期中集成了关于Safety和Security特征与特性的半正式规范。使用TTool可以轻松地对模型进行仿真和形式证明，以便从性能，安全性和安全性方面评估架构选择和设计选择。此外，SysML基于一种众所周知的系统工程设计语言，并且完全由TTool支持。

SysML-Sec已在EVITA项目的范围内定义和使用，即用于保护汽车嵌入式系统。本文介绍的案例研究是从该项目中摘录的，并展示了SysML-Sec的兴趣和选择。

现在，一个重要的工作目标是为SysML-Sec添加推理功能。更确切地说，我们的目标是验证关键功能不受引入安全机制（例如安全机制）的限制。消息加密或网络过滤。这可以通过逻辑推理规则来完成。