EMV卡安全性研究：基于SysML模型的鲁棒性测试用例

© 2013年。由爱思唯尔公司出版由美国应用科学研究所负责选择和/或同行评审可在www.sciencedirect.comwww.sciencedirect.com上在线获取ScienceDirectIERI Procedia 4（2013）133 - 1382013年电子工程与计算机科学EMV卡：基于SysML模型Noura Ouerdia *，Mostafa Azizib，Jean-louis Lanetc，Abdelmalek Azizia，alab ACSA，FSO，Mohammed First University，Oujda，60000，Moroccob labMATSI，EST，Mohammed First University，Oujda，60000，Moroccoc lab XLIM，SSD，Limoges，87000，France摘要智能卡越来越多地用于需要安全性的关键数据的几个领域。我们举医疗领域和智能卡支付购物为例。因此，智能卡的硬件和软件安全是敏感信息安全处理的关键要素之一。目前，一些科学研究人员有兴趣研究和提高智能卡的安全性。对漏洞的研究是建立这类设备安全保障的先决条件。事实上，每个漏洞都很容易导致攻击。在本文中，我们产生的基础上，模型的Europay-MasterCard和Visa（EMV）规范的漏洞测试用例。我们使用SysML语言通过机器状态图对EMV事务进行建模。然后，我们生成的Event-B模型，我们利用它来生成脆弱性和鲁棒性测试用例。这项工作旨在确保EMV卡的安全性，防止利用系统的漏洞进行攻击。© 2013作者。由Elsevier B. V.在CC BY-NC-ND许可下开放获取。信息工程研究院负责评选和同行评议关键词：EMV，智能卡，SysML，Event-B，测试用例;* 通讯作者。联系电话：+212 6 06 43 16 86。电子邮件地址：noura.ouerdi@gmail.com。2212-6678 © 2013作者由Elsevier B. V.在CC BY-NC-ND许可下开放获取。信息工程研究所负责的选择和同行评审doi：10.1016/j.ieri.2013.11.020134Noura Ouerdi等人/ IERI Procedia 4（2013）1331. 介绍嵌入式系统执行预定义的任务。它们在能耗、成本、可靠性和安全性方面都有具有约束力的规范。事实上，这些系统可能是应该为其用户维护和保护的机密信息的持有者。特别是关于通过智能卡传输支付信息。在这种情况下，智能卡成为攻击目标有几个原因：首先，它们是可用的，容易获得[1]并且价格便宜，这有助于攻击者获得大量的测试。第二，它们是手机。因此，攻击者很容易将它们提交给敌对环境。第三个也是重要的原因是，成功的攻击可能允许访问用户的机密和敏感数据。由于所有这些原因，智能卡的设计者和开发者都非常清楚。他们非常重视产品的安全性，尤其是当安全系统的攻击者不断开发新技术来访问信息时。智能卡是用于传输潜在关键数据的设备，因此是不可侵犯的。 例如，对智能卡的攻击是通过利用系统漏洞来确定其加密密钥的值。为了避免这种攻击，我们应该确保系统不容易受到攻击。验证过程是通过对真正的智能卡进行一系列测试来完成的。我们的贡献对这一轴心特别感兴趣。在本文中，我们提出了一种新的方法来测试支付应用程序的EMV规范的基础上，使用基于模型的测试集成到一个SysML开发过程。本文的组织如下：第二部分介绍了Europay智能卡Visa规范的概述。第三部分列出了用于建立我们的方法的各种工具。在第四部分中，我们讨论了我们的方法和步骤。2. EMV概述在本节中，我们提供了EMV规范的高级概述，该规范包含在题为：符合Europay-Visa-Mastercard（EMV）规范的集成电路卡（ICC）的卷中[2]。EMV是集成电路卡（ICC）支付的标准，即包含智能芯片的信用卡。20世纪90年代，Europay、MasterCard和Visa率先推出EMV。目前，EMV标准由EMVCo维护。EMV规范定义了一组规则，这些规则规定了要实现的最低功能以及如何实现这些功能。四本书介绍了EMV规范[2]：Book1：独立于应用的ICC到终端Book2：安全和密钥管理第3册：应用规范第四册：持卡人、服务员和收单行在我们的工作中，我们特别感兴趣的应用规范定义的书3和安全和密钥管理中提出的书2，特别是，卡和终端之间的交易的应用协议数据单元（APDU）的命令。所有智能卡都遵循ISO/IEC 7816标准[9]，而大多数银行或信用卡中的智能卡都遵循EMV标准[2]，称为EMV卡。在我们的工作中，我们处理EMV卡与终端交互，以确保支付交易。终端向卡发送APDU命令，卡响应。因此，终端和卡之间的交互是通过一组Noura Ouerdi等人/ IERI Procedia 4（2013）133135终端和卡分别发送的命令/响应。为了成功执行EMV交易，需要遵循六个步骤应用选择：第一个APDU命令由终端发送，用于选择应用。该命令是SELECT APPLICATION命令APDU，用于使用其AID（小程序标识符）选择卡中存在的所需小程序。使用GET PROCESSING OPTIONS命令对EMV事务进行重命名。它使卡准备好与终端通信。卡认证：有两种类型的卡认证：静态认证和动态认证。对于静态认证，终端使用公钥对卡中包含的静态数据进行签名，以证明卡的合法性。而动态认证允许终端使用APDU命令对卡进行动态认证。因此，卡必须为每笔交易更新签名。然后，签名取决于交易，并且对于每个交易都是唯一持卡人身份验证：持卡人通过终端输入个人识别码（PIN）。终端将该PIN码发送到卡，并使用VERIFY命令APDU对其进行验证密码生成：由于对卡和持卡人都进行了认证，因此初始化了必要的参数。终端决定发送GENERATE APPLICATION PROTOCOL命令。该命令APDU的数据字段包含交易金额，货币和终端功能[10]。我们的方法是基于这些APDU命令来建模EMV卡和终端之间的通信。然后，生成系统的漏洞测试用例。下一节描述了用于实现我们目标的工具。3. 用于应用我们方法的SysML（System Modeling Language）是一种用于系统工程应用的通用建模语言。它重用了UML2.0的一个子集，并通过使用UML的profile机制定义了额外的扩展Rodin是一个开源平台，也是Event-B的一个基于JavaScript的IDE，它为精化和数学证明提供了有效的支持。它为Eclipse框架做出了贡献，并且可以通过UML-B等插件进行进一步扩展。UML-B[3]是一种图形化的形式化建模符号，它依赖于Event-B的语义。它是RODIN工具包的一个插件，由Eclipse建模框架（EMF）实现[5]。UML-B有自己的元模型，并提供工具支持，包括基于UML的绘图工具和生成Event-B模型的翻译器[6]。ProB是B方法的动画和模型检查器它允许B规格的自动动画除了B方法，ProB现在甚至支持Event-B方法。事件B是由B方法衍生而来的它保留了经典的B方法[8]的概念，并增加了事件的概念。事件B模型提供了定义良好的语法、概念和语义，并且可以通过证明在软件过程中进行的转换（事件）是正确的来测试它们。在这种情况下，Java Card字节码验证器的漏洞测试的自动生成已经被执行[11]。为了确保模型的正确性，Event-B使用由罗丹自动证明工具支持的证明义务[4]。4. 结果和我们的新方法作为我们研究的一部分，我们对安全和漏洞测试感兴趣，这些测试旨在确保被模型拒绝的行为也被其实现拒绝我们首先使用SysML语言对EMV事务进行建模我们选择SysML是因为使用SysML图更容易表达需求。136Noura Ouerdi等人/ IERI Procedia 4（2013）133事实上，从复杂任务的正式模型开始，所以我们使用不太正式的模型，然后，我们继续生成可用于自动化测试生成的Event-B模型。我们的方法分为三个主要步骤，详见下图使用UML-B生成事件B模型测试用例使用：VTG工具[11]图1.图解说明我们的方法4.1. 基于SysML语言我们假设卡的定制阶段已经完成。在我们的工作中，我们处理的EMV交易所代表的EMV卡的使用阶段。基于本文第2.2节中总结的EMV规范[2]，我们使用SysML语言提出了我们的模型。实际上，我们创建了Machine状态图，它详细描述了从初始化到事务完成的EMV事务过程（参见图2）。图2. EMV事务状态表示系统终端卡的状态，转换是APDU命令。对于以下过渡：GAC1_TC_AAC_ARQC AAC：GAC1表示第一次调用GENERATE AC命令。它以TC、AAC或ARQC密码作为参数，并返回AAC密码SysML模型抽象测试用例Noura Ouerdi等人/ IERI Procedia 4（2013）133137GAC1_ARQC ARQC：第一次调用带有ARQC密码参数的GENERATE AC命令。它返回ARQC密码。GAC1_TC TC：第一次调用GENERATE AC命令。TC密码作为参数和返回值TC。GAC2_TC TC：GENERATE AC命令的第二次调用。TC密码作为参数和返回值TC。GAC2_AAC_TC AAC：GENERATE AC命令的第二次调用。它以AAC或TC密码作为参数，并返回AAC密码密码AAC ARQC和TC分别表示翻译拒绝，在线授权请求和交易批准。4.2. 事件B模型生成使用Rodin接口，我们创建了我们的机器状态图;我们为每个转换（APDU命令）指定了参数，保护和动作。然后，我们通过利用UML-B插件提供的机会生成Event-B模型。例如，为SELECT APPLICATION命令生成的Event-B模型如下：事件SELECT_APPLICATION任何C CA哪里@C.typeC卡@Statemachine1_isin_InitialisationStatemachine1=Initialisation@SELECT_APPLICATION.Guard1blocked（C）=NULL@SELECT_APPLICATION.Guard2last_store_data_value_bit8=TRUE然后@Statemachine1_enterState_Application_SelectedStatemachine1Application_Selected@SELECT_APPLICATION.STA2成功TRUE端由于形式化模型的生成是成功的，我们验证了警卫，条件，参数和模型的上下文。我们开始使用ProB为模型制作动画。因此，我们通过ProB插件提供的模型检查来验证我们的模型。5. 测试用例生成为了生成漏洞测试，我们继续对模型的连续约束进行否定。该方法由VTG [11]考虑下面是生成的抽象测试的一部分<扩展测试套件><测试案例><步骤名称=”SELECT_APPLICATION“>卡1/value>ca1/value> Application_Selected/modified><修改名称=“成功”> TRUE/修改>ca2/value>138Noura Ouerdi等人/ IERI Procedia 4（2013）133执行/修改><步骤名称=”SELECT_APPLICATION“>卡1/value>ca1/value> Application_Selected/modified><修改名称=“成功”> TRUE/修改><测试案例><扩展测试套件>本测试用例介绍了以下命令APDU系列的测试选择应用获取处理选项选择应用最后一个命令APDU显示漏洞测试。6. 结论以状态机图的形式提出的SysML模型对于熟悉EMV标准的人来说很容易理解，并且清楚地显示了终端和卡之间的真实EMV交易的步骤。通常，终端卡的规格分布在四本书中.因此，我们提出了一个简单的模型，收集规范的终端卡之间的EMV交易。然后，使用Event-B方法生成具有良好定义的概念和语义的形式化模型。用ProB对形式化模型进行动画处理，以保证模型的正确性。Newt提出了基于约束求反的抽象测试用例生成方法。我们现在的目标是在已经生成的抽象测试用例的基础上生成具体的测试用例引用[1] IMS Research，《智能卡和智能卡IC的世界市场》，2010年1月[2] EMVCo.第1-2-3-4册-独立于应用程序的ICC到终端接口要求，4.3版，2011年11月。[3] Snook，Colin和Butler，Michael，UML-B：Event-B工具集的插件。在抽象状态机，B和Z，第一届国际会议ABZ 2008。[4] Butler，M.，和Hallerstede，S.罗丹正式建模工具。2007年圣诞节BCS-FACS研讨会论文集[5] 托萨彭·朱钦将需求工程引入形式化方法的论文：Event-B和KAOS的时序图。2010年2[6] Abrial，J.-R. （1996年）。The B-book：Programs to Meanings，Cambridge University Press.[7] Vanderperren，Y.，和Dehaene，W.（2005年）。UML 2和SysML：一种处理SoC/NoC设计复杂性的方法。在欧洲设计，自动化和测试会议（DATE05），慕尼黑，德国，IEEE计算机学会的会议记录。[8] Schneider，S.，The B-Method：An Introduction，Palgrave Macmillan 2001.[9] ISO/IEC，ISO/IEC 7816：识别卡集成电路卡。[10] Julien Lancia，“智能卡模糊框架：EMV协议的应用。SSTIC 2011。[11] Savary，A.，Frappier，M.和Lanet，J.，“Java Card Byte Code verifier的漏洞测试自动生成”，网络和信息系统安全（SAR-SSI）会议，2011年。DOI：10.1109/SAR-SSI.2011.5931379. 2011年5月