SysML-Sec攻击图：复杂攻击的紧凑表示
摘要
我们在本文中讨论了如何将SysML-Sec攻击图用作复杂攻击的图形和半正式表示形式。 我们举例说明了该PC和移动恶意软件的示例。我们还提供了在这些图中使用的运算符表达性的示例。 最终，我们根据定时自动机正式化了这些操作员描述的攻击踪迹。
1 介绍
在分布式系统中，甚至在嵌入式系统中，对安全威胁进行建模是安全分析师工作的一个常见方面。 但是，威胁分析比往常更多地仅依赖于特定恶意软件及其变体的知识，或者依赖于利用众所周知的漏洞，而不是寻找新的攻击组合。
不幸的是，越来越多的嵌入式系统已成为通信工件，具有与其直接环境或后端系统的新交互功能，因此容易受到犯罪分子的攻击。 这些安全问题中的许多问题反映了对低级漏洞的利用（通常可以通过适当的编程实践和特定的组件测试来解决），或者由于对功能或安全逻辑组件到硬件体系结构的映射了解不足而导致设计漏洞。 。
我们在SysML-Sec框架[2]中引入了更系统的攻击表示，这些攻击是在设计和/或开发中的系统上设想的或已知的可行的攻击。 在遵循模型驱动工程（MDE）方法进行的活动的框架中，攻击建模阶段被认为是非常重要的驱动因素，可以激发在风险分析中引入安全对策以及选择那些安全措施的位置。 更好的机制。
SysML-Sec扩展了SysML的参数图，以便描述攻击，攻击的组成并在攻击图中表示这些攻击的资产目标。 我们还将在本文中讨论攻击图及其操作符的使用，并基于定时自动机（新颖贡献）定义其形式语义。 我们还将介绍一个更完整的应用示例，以分析之前未发布的Zeus / Zitmo移动恶意软件。
2 攻击建模
威胁和攻击所选资产的威胁和安全漏洞应尽可能描述攻击者应达到或超过的功能以及攻击的源头（本地，远程，通过特定的接口）。SysML安全环境按照以下更详细描述的方法来支持风险评估。 EVITA案例研究中的详细信息[13,8]。 我们还根据安全目标实施了对威胁覆盖率的自动检查。 基于风险分析，还应确定映射到威胁的安全目标并确定其优先级。
攻击图我们建议不要使用传统的攻击树方法[14]，而应使用稍微自定义的SysML参数图，使用更相关的方法更好地对威胁进行建模。威胁被建模为嵌入到代表攻击目标的块中的值，从而实现了从视觉上强调资产的表达。攻击（<< Attack >>构造型）可以与一些原始运算符链接在一起。这些运算符或者是逻辑运算符，例如AND，OR和XOR，或者是时间因果运算符，例如SEQUENCE，BEFORE或AFTER。我们认为后一种构造对于描述攻击者在嵌入式系统中的操作观点特别有用，例如在两次因果相关的攻击之间存在最大持续时间的情况。例如，使用限时认证令牌攻击系统时，必须首先检索该令牌，然后必须在该令牌到期之前使用该令牌。
可以将不同参数图中的攻击实例链接在一起，以评估特定漏洞的影响以及在风险评估阶段解决该漏洞的需求。 攻击也可以标记为根攻击，这意味着此攻击位于攻击树的顶部。 换句话说，这种攻击不用于建立更复杂的攻击。 最后但并非最不重要的一点是，攻击可以链接到需求，因此可以通过验证每种攻击是否都链接到至少一个安全需求来自动检查攻击的覆盖范围。
最终，在多个图中进行的攻击会生成一个有向图，该图的顶点可以是单个攻击（或叶攻击），中间攻击（由多种其他攻击的组合产生）或组合其他攻击的运算符。 我们目前仅考虑非循环图，但目前正在考虑扩展循环图以对资源使用进行建模（请参见第6节中的讨论）。 最后但并非最不重要的一点是，我们并不是说这些运算符总是非常适合于对攻击图进行建模，但是至少，攻击图比攻击树具有更丰富的语义，因此导致了更紧凑的表示（换句话说：更少 必须使用运算符）。 此外，攻击图还展示了它们对复杂攻击场景进行建模的能力，例如 宙斯/齐莫
3 示例：对Zeus / Zitmo建模
ZeuS犯罪软件套件的移动组件（也称为或TrojanSpy。*。Zitmo）于2010年发布，目的是拦截来自手机的移动交易验证码（mTAN代码）。
PC / Windows组件Zeus使用恶意插件修改了Microsoft Windows计算机的浏览器，因此，任何访问在线银行网站的尝试都会将请求重定向到攻击者提供的伪造银行网站。 另外，键盘记录器会监视用户名/密码对，以使攻击者有可能在未被检测到的情况下登录到用户的真实银行系统中。 Zitmo还恶意建议用户在他/她的手机上安装伪造的手机银行应用程序。 完成后，伪造的应用程序间谍会收到SMS消息，从而以静默方式窃取mTAN。
图1给出了该木马的SysML-Sec攻击图。它是由TTool [1]制作的。系统攻击者通过两个主要子模块进行建模：攻击者PC用来收集有关用户凭据（用户名，密码，mTAN）的信息并使用这些凭据执行非法交易，以及一台用于托管假银行网站的网络服务器。被攻击的系统包括目标人员的Windows PC和他/她的Android手机。第一个漏洞利用是在Windows PC上使用Win32漏洞利用，浏览器漏洞利用或在应用程序中使用其他漏洞利用来执行的：攻击图模型因此在“ UserPC”块中包含三个子块。 XOR操作员表示，一旦在目标PC上执行了一个利用程序，就可以安装该木马，并且不再需要链接到XOR的进一步利用程序。该木马拦截用户的用户名和密码，并将其发送回攻击者系统。同时，为了拦截对银行系统的请求，必须进行几次攻击：攻击者必须安定一个伪造的银行服务器。攻击者还必须控制对银行系统的http请求。他/她还必须在被攻击的PC的浏览器中安装恶意插件。完成所有这些操作后（AND运算符），浏览器可以要求用户在其手机上安装伪造的Android应用程序（该模型右下方的SEQUENCE运算符）。安装后，伪造的应用程序可以静默监视SMS（“UserMobilePhone_Android”块中的SEQUENCE运算符），从而检索mTAN。获得mTAN时，攻击者有120秒的时间使用它（操作员之前）。
4 攻击图构造的语义
攻击痕迹的语义由定时自动机捕获，定时自动机是自动机并行且同步组成的结果，自动机并行表达了单个攻击的潜在发生和再次发生，自动机也表达了描述这些攻击方式的操作员行为 组成。 在不失一般性的前提下，下面我们描述由两种攻击的二进制组合生成的自动机（但它们支持两种以上的攻击）。
可以按图2中的Attack1所示对独立的攻击（可能是攻击树的叶子）进行建模。一个攻击可以：
- 成功（a1！）。 在这种情况下，此后可以再次执行。
- 停止（stop_a1？）。 当攻击图的所有相关自动机都同步之后，如果系统不允许激活这种攻击，则停止攻击，例如，XOR运算符禁止执行该攻击。
4.1 中间攻击
图中的中间攻击节点在攻击的构成中起着重要作用，因此，它们相互连接运营商。 根据前一个运算符的语义，这样的节点对应于在定向攻击图中在其之前的一个或多个攻击的成功。 这些节点的语义必须更具体地支持图中停止事件的向后传播。 因此，中间攻击（请参见图3）首先等待其激活运算符（attack_OPERATOR），然后可以执行几次（attack_inter），或将其停止（stop_inter）。 同样，在其激活运算符完成之前，可以将其停止（（从初始状态停止stop_inter）：在后一种情况下，只能执行其运算符的完成（attack_OPERATOR）。
最后，我们假设攻击Attack1和Attack2之间的定向连接是Attack1到OR节点，然后从OR节点到Attack2的快捷方式。
4.2 AND操作符
AND运算符对期望联合执行多个攻击（可能以并行方式）的期望进行建模。 未能实现任何基本攻击都会导致后续依赖攻击的整体失败。 例如，许多恶意软件都依靠检查来确保它们未在虚拟蜜罐中运行：所有这些检查都应该成功，因此可以将其建模为AND下的攻击。
时间自动机将操作员的行为形式化，如图4所示。它执行基础攻击自动机的同步。 处理额外的攻击将导致在此定时自动机的第二状态下发生额外的迁移。
4.3 OR操作符
OR运算符对可以执行多种攻击以启用其他复合攻击的情况进行建模。 第一次成功的攻击将使在攻击图中更远的位置执行新的复合攻击。 同样，在使用OR进行的复合攻击进行甚至成功之前，也不需要在OR运算符下进行所有攻击（参见图5）。
例如，该操作员可以对攻击者或恶意软件可能执行的冗余操作进行建模，以提取某些信息。
让我们以从Chuli Android移动恶意软件[7]的模型中提取OR运算符为例。基本上，Chuli通过垃圾邮件感染手机，然后将包含在手机中的私人信息发送到远程攻击者的服务器。 该恶意软件的一个有趣功能是它能够使用由外部事件（例如ScreenOn和BatteryLevel事件）触发的回调服务监视它是否正在运行。 一旦系统中发生此事件之一，必要时Chuli可以重新启动其主应用程序。 因此，所有这些触发事件都可以并行监控。 换个说法，所有事件之一足以让Chuli进行检查。 同样，一旦Chuli使用了一个事件，Chuli就会继续其他事件。 所有这些都对应于OR运算符，请参见图6。
4.4 XOR操作符
XOR运算符为替代攻击和排他性独立攻击建模。 因此，此操作员表达的感兴趣行为是一次攻击的成功。 换种说法，在操作员提到的攻击中，任何第一个成功的攻击都是在排除所有其他攻击的情况下出现在攻击痕迹中的攻击。
OR的语义是不同的，因为XOR禁止执行其他攻击，而第一个成功的攻击除外。 相反，OR不会对其他攻击施加任何约束。 例如，在并行测试攻击的情况下（例如，等待多个回调通知成功的监视器），则应使用OR运算符。 如果只测试一种攻击，一种又一种攻击，而没有强加测试顺序，则应使用XOR运算符。
更正式地讲（请参见图7），一旦成功执行了一次攻击（a1？或a2？），就会停用未执行的攻击（stop_a1！或stop_a2！），然后执行中间攻击（attack_XOR）。
4.5 SEQUENCE操作符
SEQUENCE运算符对必须严格按照a1，a2，…，an顺序执行的攻击进行建模（请参见图8）。 未能实现一个攻击ai使得不可能随后执行j> i的攻击aj。
4.6 BEFORE操作符
BEFORE运算符基于一系列攻击，两次连续攻击之间的持续时间最长（见图9）。 就像SEQUENCE一样，无法实现一次攻击就无法实现后续攻击。 此外，在给定的允许执行时间内未能实现一次攻击也使得不可能执行后续攻击。
该运算符特别适合于对寿命有限的令牌建模。
4.7 AFTER操作符
AFTER运算符基于一系列攻击，两次连续攻击之间的持续时间最短（请参见图10）。 就像SEQUENCE一样，无法实现一次攻击就无法实现后续攻击。 此外，如果可以在最小持续时间之前执行攻击，则系统将强制其仅在最小持续时间之后执行。
AFTER运算符对于在等待访问可用之前对攻击无用的情况进行建模尤为有趣，例如，在两次尝试之间的延迟最小的情况下暴力破解密码系统时。
5 系统验证
从形式验证的角度来看，可以从TTool直接根据攻击的可达性，活性和“导致(lead to)”性质来正式分析攻击图。
- 攻击的可达性 表示至少存在一系列导致a的攻击a1，a2，…，an，a（即攻击trace）。
- 攻击活性a。 意味着无论系统a1，a2，…; an中有什么可能的攻击trace，都存在i / ai = a。
- 进行了又一次攻击a之后的攻击b的活性。 意味着每当攻击trace包含a = ai：a1，a2，…; an，?j> i / aj = b。 该性质通常被称为“导致”（在TTool中就是这种情况）或“响应”。
通过在TTool中编辑的SysML-Sec模型，用户可以模拟模型或使用UPPAAL进行形式证明[3]。 集成在TTool中的模拟引擎允许执行常规命令（逐步执行，到达下一个断点等），并在模拟攻击图时对其进行动画处理。 还将显示代表已执行攻击的跟踪的序列图。 也可以直接从TTool中使用按钮方法来进行形式证明（但需要安装UPPAAL）：确实，TTool会自动将攻击图转换为UPPAAL规范，将其馈入UPPAAL，获取结果，并将其显示在 一种友好的方式。 在我们进行的所有案例研究（线性算法）中，从用户的角度来看，这种模型转换都是即时的。 形式证明的复杂性显然取决于模型并发性，例如，使用OR运算符会增加并发性，而使用SEQUENCE约束跟踪。
图11显示了TTool的Zitmo模型的“根攻击”（“IllegalBankAccountTransactionBasedOnToken”）的可达性和活性对话框窗口（图1）。 可达性和活性都得到了满足。
如果选择了两次攻击，则可以评估“导致(lead to)”性质。 例如，在Zitmo模型（图1）中，我们可以选择两种攻击方式a1 =“ RedirectHttpRequestFromBankToFakeBank”和a2 =“ IllegalBankAccountransactionBasedOnToken”（请参见图12）：“ Leads to”属性适用于a1 a2而不适用于a2 a1 。
TTool还允许启用/禁用攻击树攻击，以了解攻击对系统的重要性/影响。 例如，如果我们禁用攻击“ SilentlyInterceptSMS”，则根本无法再进行根攻击。
6 结合操作符和攻击
本节讨论了依靠第4节中描述的攻击之间的关系来处理复杂攻击关系的方法。
6.1 在XOR下对攻击进行优先级排序
XOR运算符不对执行可能的攻击施加任何优先级。 但是，可以通过将XOR与各个攻击的所有可接受的顺序组合来实现这种顺序，如使用SEQ运算符所描述的。 这样的复合运算符可以在上述运算符的基础上实现，但需要生成所有可能的交织。为简化规范，我们建议定义宏运算符SXOR。这样的宏运算符可以集成在TTool环境中。 从长远来看，如果此类操作符证明有用，则可以将它们标准化为所有SysML-Sec设计人员共享的库。
6.2 时间约束之间的兼容性
由于这些运算符的时间值，AFTER和BEFORE的联合使用会导致无法进行攻击的情况。 例如，在图14中，根攻击无法到达，因为需要在10个时间单位之前执行一次攻击。 但是AFTER运算符禁止这种情况。 修改AFTER和BEFORE中的时间值可以使根攻击达到目的，例如，通过使用相同的时间值。 TTool已经可以分析这种情况，即由于时序不兼容，它可以识别出无法到达的攻击。
6.3 环和可达性
通过将操作符产生的攻击与先前在攻击跟踪中已经处理过的操作符链接起来，可以在攻击图中获得环。
例如，如果我们考虑图15，因为循环发生在OR运算符上，所以rootattack2是可到达的。 如果对AND运算符执行相同的循环，则将永远无法执行后者，因此rootattack1不可访问。
当前，TTool和我们的语义不支持这种情况。 通常，对循环使用情况进行更精细的控制将需要定义可以允许执行同一运算符的次数，例如，通过在每个运算符上添加一个执行计数器。 同样，只要没有明确停止攻击，就可以无限次执行攻击：还应将计数器添加到这些构造中。 面对拒绝服务攻击的建模，这项工作尤其有用，因为拒绝服务攻击不仅需要定性，而且需要对攻击者的能力进行定量评估。 我们计划在未来的工作中开发这些技术。
7 相关工作和观点
[14]所揭示的攻击树的形式主义长期以来一直被用来描述对应用程序和系统的威胁，以及用于实现这些威胁的攻击。 在这方面，在可靠的计算中，攻击树与故障树密切相关。 攻击树遵循面向目标的方法，该方法与攻击者的目标相匹配并大致描述了攻击痕迹。 但是，它们捕获了唯一的跟踪，并使其难以捕获基于子攻击构建的复杂攻击方案。 他们也无法捕获与被攻击资产有关的给定攻击中涉及的体系结构组件，即使这通常构成了重要信息，可以使人们信任该组件。 在我们的案例中，攻击的位置是通过映射到体系结构组件来确定的。
已经开发了攻击树的多种变体：它们以越来越高级的语义（例如[10]）引入了运算符，但尚未解决上述问题。 我们的工作试图根据攻击图的结构解决这些问题，而不是仅基于操作符本身。 除其他好处外，该结构还简化了子攻击的重用，而没有任何重复。
甚至在攻击树还没有被广泛使用之前，就已经提出并形式化了攻击图，例如特权图[5]，并且最近为了自动从其他形式主义生成它们[15]。 [5]特别强调了威胁安全评估的量化方面。 使用马尔可夫模型确定攻击图中的特权边缘。 我们的工作还旨在引入量化评估，同时仍然保留使攻击树成功的分层模型，并且与SysML-Sec中的系统架构相联系，这与[5]作者描述的“迷宫”图相反。 ]。
建议扩展以用更多动态模型来补充静态攻击树表示。 例如，提出了一种基于Petri网的方法[6,12]，以描述攻击树内攻击的不同阶段的触发。 [11]还建议使用马尔可夫过程（BDMP）来描述以树状方式组织的各种攻击之间的关系，但其触发可能与该结构无关。 最近，[16]依靠攻击树来补充对Android恶意软件的静态分析和动态分析：节点充斥着例如权限和功能（“ P”：可能实现；“ I”：不可能实现）。 除了捕获树以外，还引入了其他形式主义来捕获攻击，但是它们通常首先针对安全机制。 我们可以提到诸如UMLSec [9]之类的建模环境，以及用于证明安全协议中的安全属性的工具[4]。
在某种程度上，所有这些模型还描述了具有对应于不同关系的边的攻击图。 但是，本文描述的方法主要集中在表达多条攻击痕迹上。 它旨在了解系统是否易受攻击，从而通过攻击可达性和活动性分析来帮助确定最重要的安全对策。 确实，TTool促进了图中攻击的激活/取消激活，从而允许分析不同情况下攻击的可达性和活跃性。 结合攻击的位置，这有助于确定首先应对哪些攻击以及在何处应对。 我们还认为，与刚刚概述的方法相比，我们的阶段建模更为直接，因为它的功能更加丰富。 攻击树，并且由于以资产为中心的攻击分布，更容易以模块化的方式表达威胁。
8 总结和未来工作
根据我们的经验，在对攻击进行建模时，分区是一个非常重要的元素，以便了解处于风险中的资产，其潜在漏洞以及攻击者的能力。 因此，SysML-Sec建议在安全性要求，攻击图和分区模型之间使用迭代。 攻击图采用以块为中心的观点，并考虑到重用。 我们特别认为，这将允许安全分析人员对通过系统特定分析的现成组件（COTS）执行的威胁建模进行组合。
第6部分已经讨论了我们工作的一些扩展。我们计划进一步扩展SysML-Sec的表达能力，如下所示：我们的声明性方法应该特别有用，以便将其他威胁建模方法的知识纳入其中。 在这方面，我们的建议将攻击明确地映射到体系结构，并有可能在SysML参数图中引入攻击者的抽象模型以进行威胁建模。 我们基本上计划将我们的方法扩展到对威胁进行更定量的评估，并且还将攻击图和风险评估整合在一起，例如，使用攻击和操作符之间的风险值。