多应用智能卡形式化建模的问题和方法

　智能卡（Smart Card）又称集成电路卡，即IC卡。它将一个集成电路芯片镶嵌在某种材质中，封装成卡式、本式或者其他形式，其外形与覆盖磁条的磁卡相似[1][2]。智能卡内含CPU，通常具有芯片操作系统（Chip Operating System，COS），其安全性高。在电子商务、电子金融和电子政务迅速发展的今天，智能卡作为身份凭证、电子钱包、电子存折和各种证书以及重要数据的载体，正发挥越来越重要的作用[3]。
　　智能卡从不同的角度有多种分类方法，例如，从智能卡的应用结构不同，可以将其分为多应用智能卡、单应用智能卡。其中，多应用智能卡中又包含不支持动态应用管理的Native卡以及支持多应用动态下载的Java卡。Java卡是一种可以运行Java程序的CPU智能卡，使用Java卡平台创建的智能卡上存有Java applet，Java卡使多个应用程序被安装并且各自独立地共存。
　　目前，专一功能的智能卡覆盖了我国金融、电信、社会保障等多个领域，改变了人们沿袭多年的现金支付方式，大大方便了人们的生活，提高了效率。各行业发行的具有支付功能的智能卡应用于生活、生产的各个领域，不同行业的智能卡之间互不兼容，不仅造成社会资源的浪费，与低碳生活的理念背道而驰；同时卡的种类和数量过度繁多，也给人们生活带来不便，浪费了很多不必要的时间。因此，多应用智能卡是智能卡行业发展的必然趋势，它不仅可以使我们的生活更加便捷，而且也符合了时下低碳、环保、节能的生活理念。
　　1 多应用智能卡的文件系统
　　目前，最广为人知的智能卡标准就是ISO7816，此标准主要定义了塑料基片的物理和尺寸特性，触点的尺寸和位置，信息交换的底层协议描述，以及跨行业的命令集等等。ISO7816标准支持两类文件：DF（Dedicated File）和EF（Elementary File），在下面的我们将对这两类文件做详细介绍。
　　智能卡中，用户的应用数据都存放在智能卡的EEPROM中，以文件形式组织。智能卡文件系统是由专有文件DF（Dedicated File）和基本文件EF（Elementary File）组成的。卡内数据的逻辑组织结构由专有文件DF的结构化分级组成。在根处的DF称为主文件（MF） 。MF是必备的，其它DF是任选的。基本文件又分为内部基本文件和工作基本文件。其中内部基本文件存放的数据由卡进行解释，即为了达到管理和控制的目的，由卡来分析和使用这些数据；而对于工作基本文件，卡不能对文件中的数据进行解释，而是由外界来使用这些数据。
　　对于智能卡文件系统中的三种文件类型：MF、DF、和EF，图1给出了这三种文件的关系。其中，MF（第1级）为根文件，是必须有的，卡片中只能有一个MF 文件。它是在卡的个人化过程被首先建立起来，在卡的整个生命周期内一直保持有效，可存储卡片的公共数据信息并为各种应用服务。卡片复位后，自动选择MF 文件为当前文件。DF（第2，3，...级）是可选的。包含用户设置的系统信息和应用相关数据，在MF 下DF 的数量只取决与卡片容量和用户的应用，它也可以包含若干的DF。基本文件EF是文件结构的末端，只包含系统信息、内部数据或用户数据。基本文件EF从结构上可分为四类，分别是透明结构、线性定长结构、线性变长结构和环形结构[4]。
　　2 多应用智能卡形式化建模现状
　　在复杂的智能卡中，逻辑攻击是非常敏感的，也就是说多应用智能卡的安全极易受到威胁。以下列出了在设计智能卡过程中几条防止逻辑攻击的策略：
　　1） 结构化设计：在卡中构建小的函数模块，这样可以更加简单地理解和校验。
　　2） 形式化验证：使用数学模型去验证函数的稳固性。
　　3） 测试：对软件的运行情况进行测试。
　　智能卡应用系统的安全环境很复杂，对智能卡的保护仅靠以上三条是远远不够的，但是若在设计层面能尽可能地保证智能卡的安全性，在智能卡使用过程中就会在很大程度上减少智能卡的不可靠性[5]。
　　智能卡的安全机制保障了所下载的应用是无害的，并且遵循与初始化及访问控制相关的基础策略。这样的基础策略均为所有的智能卡必须遵循的基础。所以，要来验证安全机制是否遵循了这些基本策略是很重要的。因此，一个智能卡安全的重要的形式化方法应用是验证平台，验证平台旨在提供Java平台和安全机制的抽象模型，并且验证智能卡的安全功能是可靠的。然而，这不能充分说明我们对安全功能的设计是正确的，更不必说我们还需要保证智能卡其它部分也是安全可靠的：Java卡的API和GP（Global Platform）规范的API是智能卡组成的重要部分，两个API的正确设计是对安全的核心需求。因此，对于平台验证的另一个重要的方面就是展示API是不是被正确设计了。
　平台验证对于智能卡的安全保证来讲是最为基础的一步，并且是通用标准评估的先决条件。然而，Java卡安全机制所提供的保障都是限制性的，并且进一步对应用是否对基础设施合法使用进行了验证，同时不可以尝试任何敌对性的动作。所以，应用认证对智能卡的形式化方法来讲是另一个重要的应用。平台验证和应用确认是保证智能卡安全的两个重要方面[6]。
　　形式化方法是提高系统安全等级必不可少的保障技术。形式化方法使用谓词逻辑、集合、关系等数学元素和原理表达系统中的部件及其运动规律，形式化方法的使用过程及形式规范、求精和实现等几个阶段，可以用于保证系统初始规范和后续过程的正确性和一致性。目前比较著名的形式化方法有Z语言，和由Z语言发展而来的B语言以及Event-B语言。
　　下面着重分析多应用智能卡中形式化方法的研究现状。
　　2.1 Z方法
　　2.1.1 Z方法简介
　　Z方法[7][8]最初是由法国学者Jean-Raymond Abrial等人设计的一种基于一阶谓词逻辑和集合论的形式规格说明方法，它采用了严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说明。
　　Z方法的核心是模式，它有两种模式：状态模式和操作模式。状态模式定义目标软件系统某一部分的状态空间及其约束特性。操作模式[9]描述了系统某部分的行为特征，它通过描述操作前该部分的状态值和操作后该部分状态值之间的关系来定义系统该部分的一种操作特性。模式还可以修饰，模式修饰的作用是将修饰应用到被修饰模式的声明部分中所有的变量[10]。
　　2.1.3 Z方法的应用： 电子钱包
　　Z语言具有灵活且扩展性良好的特点，在安全应用系统开发实践过程中获得了巨大的成功。例如电子钱包系统规范就是运动了Z方法进行形式化描述。
　　电子钱包的形式化模型[11]主要包括两个部分：抽象模型和具体模型。在电子钱包系统的抽象模型中，描述了整个钱包和电子交易的过程（如图2） ，包括请求、支付和确认支付等步骤，表达了卡片必须遵守的安全属性。在具体模型中，反映了钱包在交、
　　抽象模型的大致构建思路为：单个的电子钱包包括余额。可能损失的数额两个组件，在单个电子钱包的基础上，可以将系统本身定义为电子钱包的集合体，在这里，每个钱包都有一个独立唯一的名字。在此基础上，建立从名字到钱包之间的映射，其自变量域是转账过程中要涉及到的已认证过的钱包，这样就形成抽象系统空间。电子钱包的操作模式有两类：输入和输出，即转入和转出。在抽象模型的基础上，对该形式化模型进行精华，可以对系统的组件和操作进行实例化，添加某种安全性质或消除某项安全假设，从而构造出更接近于实现的一个具体模型，并使其符合原有抽象模型的性质和要求[12]。
　　2.2 B方法
　　2.2.1 B方法简介
　　B方法[13]是一种用于描述、设计计算机软件的方法，支持在从抽象到具体的各个层而上对软件规范进行描述，覆盖了从规范说明到代码生成的整个软件开发周期。B方法定义了一套数学推理和符号描述，支持在不同抽象层面上对软件规范的内在一致性和功能正确性进行严格的数学证明.人们已开发了一些商用和开源工具，支持基于B方法的软件开发过程，支持自动或交互式的软件规范证明.使用B方法进行软件开发与传统方法不同之处在于工程师先在抽象层面上（而不是最终在常规编程语言层面上）严格描述软件功能，可以完全没有执行的概念，可以摆脱实现细节的干扰，只描述所开发软件的最根本最重要的属性，并严格证明其性质，为后面开发出更可靠的系统打下坚实基础。而在常规开发过程中，前期工作一直用非形式文档，其内在一致性和功能正确性没有严格保证，只能靠人工检查.
　　用B方法描述软件的基本单元是抽象机，抽象机类似于我们常说的抽象数据结构，包括：数据描述（常量、变量等）、操作描述（数据上的一组操作）、不变式（数据状态必须满足的一组关系）。
　　要保证一个抽象机M的描述是完整的无矛盾的，需要证明由抽象机生成的不变式定理：
　　1） M的所有可能初始状态都满足它的不变式
　　2） 从任何满足M的不变式的M抽象机状态出发，执行M的任何操作，可能达到的状态必定满足M的不变式。
　　3） 不变式定理和其他要证明的定理称为“证明义务”，如果能证明由抽象机M生成所有不变式定理，M就是无矛盾的。
　　2.2.2 B方法的工具：Atelier-B
　　Atelier-B是由ClearSy开发，操作使用B形式化方法的证明工业工具软件。用于由阿尔斯通和西门子等手工开发，对世界上各种地铁安全自动化进行建模。根据“通用标准”发展模型系统，由Atmel公司和意法半导体（ST）进行标准认证。也被用于其他一些行业，如汽车电子3个车型经营原则的建模。
　　Atelier-B中的主要工具及其关系如上图所示。其中，B Compiler是最核心的部分。用于分析B模型的语义，证明类型的统一性、构造规则以及模型在B项目中的可见性。因此，是一个允许新应用产生的强大的库。
　　最后，我们介绍一下Atelier-B的用户界面。在运行Atelier-B之后出现的界面中，主要显示项目中的组成部分以及证明结果，即类型是否一致，产生多少证明义务，以及成功证明和失败证明的数量。双击项目名称可编辑项目，即图中最上面一层窗口，会显示组成部分的具体信息以及之间的关系。图中中间一个窗口时证明窗口，显示证明义务是否成功证明，以及失败的原因。[13]
　　智能卡是由许多逻辑和物理组件组成，旨在在发行者控制的环境中，使应用程序具备安全性和互用性。
　　Java卡不提供标准的机制来管理卡中的应用。为了从这样的机制中获取便利，大多数的Java卡同样实现GP规范，GP给多应用智能卡的管理机制提供了已经发布的工具。GP机制使用两种截然不同的规格详细描述，两种分别描述卡的功能需求以及其相关的安全需求。智能卡的安全很强地依赖于GP的正确设计和实现，但是现在很少有使用形式化方法来分析GP的，B方法则是其中的一个例外。
参考文献：
　　[1] 王爱英.智能卡技术——IC卡[M].3版.北京：清华大学出版社，2009.
　　[2] 张之津.智能卡安全与设计[M].北京：清华大学出版社，2010.
　　[3] 刘玉珍，张焕国.多应用安全智能卡结构的研究[J].武汉大学学报（理学版），2006， 52（1）： 87-91.
　　[4] 李晓航.认证理论及应用[M].北京：清华大学出版社， 2009.
　　.Information Security Bulletin， 2002.
　　[6] Gilles Barthe， Guillaume Dufay. Formal Methods for Smartcard Security [R].page9
　　[7] Jean-Raymond Abrial. "Data Semantics" [C]. in Klimbie & Koffeman， Data Base Management， North-Holland， pp. 1-59.
　　[8] Jean-Raymond Abrial， Schuman， Stephen A； Meyer， Bertrand （1980）， "A Specification Language"[C].in Macnaghten， AM； McKeag， RM， On the Construction of Programs， Cambridge University Press， ISBN 0-521-23090-X.
　　.
　　[10] 夏建勋，唐红武.需求分析的Z语言形式化方法[J].科学技术与工程，2008，8，（8）：2245-2248.
　　[11] 李改成.安全应用系统的形式化规范与求精过程研究[J].信息网络安全，2009（5）.
　　[12] Abrial J. The B-Book： Assigning Programs to Meanings[M]. Cambridge University， November 3， 2005.
　　[13] Global Platform[DB/OL].http：//.
　　.Cambridge University， 2010.