多應用智能卡形式化建模研究

陳贊

摘要：該文簡單介紹了多應用智能卡的發(fā)展現(xiàn)狀以及智能卡的文件系統(tǒng)結構，重點從形式化建模語言、模型驗證工具以及建模過程三方面分析了當前智能卡的建?，F(xiàn)狀。

關鍵詞：智能卡； 多應用建模

中圖分類號：TP311 文獻標識碼：A 文章編號：1009-3044（2014）29-6961-05

Abstract： This paper first introduce current situation of Multi-Application smart card and the file system used by chip operating system（COS）of smart card. And then analyzes the modeling status of smart card based on formal modeling languages， modeling tools and modeling process.

Key words： smart card； multi-application formal modeling

智能卡（Smart Card）又稱集成電路卡，即IC卡。它將一個集成電路芯片鑲嵌在某種材質(zhì)中，封裝成卡式、本式或者其他形式，其外形與覆蓋磁條的磁卡相似[1][2]。智能卡內(nèi)含CPU，通常具有芯片操作系統(tǒng)（Chip Operating System，COS），其安全性高。在電子商務、電子金融和電子政務迅速發(fā)展的今天，智能卡作為身份憑證、電子錢包、電子存折和各種證書以及重要數(shù)據(jù)的載體，正發(fā)揮越來越重要的作用[3]。

智能卡從不同的角度有多種分類方法，例如，從智能卡的應用結構不同，可以將其分為多應用智能卡、單應用智能卡。其中，多應用智能卡中又包含不支持動態(tài)應用管理的Native卡以及支持多應用動態(tài)下載的Java卡。Java卡是一種可以運行Java程序的CPU智能卡，使用Java卡平臺創(chuàng)建的智能卡上存有Java applet，Java卡使多個應用程序被安裝并且各自獨立地共存。

目前，專一功能的智能卡覆蓋了我國金融、電信、社會保障等多個領域，改變了人們沿襲多年的現(xiàn)金支付方式，大大方便了人們的生活，提高了效率。各行業(yè)發(fā)行的具有支付功能的智能卡應用于生活、生產(chǎn)的各個領域，不同行業(yè)的智能卡之間互不兼容，不僅造成社會資源的浪費，與低碳生活的理念背道而馳；同時卡的種類和數(shù)量過度繁多，也給人們生活帶來不便，浪費了很多不必要的時間。因此，多應用智能卡是智能卡行業(yè)發(fā)展的必然趨勢，它不僅可以使我們的生活更加便捷，而且也符合了時下低碳、環(huán)保、節(jié)能的生活理念。

1 多應用智能卡的文件系統(tǒng)

目前，最廣為人知的智能卡標準就是ISO7816，此標準主要定義了塑料基片的物理和尺寸特性，觸點的尺寸和位置，信息交換的底層協(xié)議描述，以及跨行業(yè)的命令集等等。ISO7816標準支持兩類文件：DF（Dedicated File）和EF（Elementary File），在下面的我們將對這兩類文件做詳細介紹。

智能卡中，用戶的應用數(shù)據(jù)都存放在智能卡的EEPROM中，以文件形式組織。智能卡文件系統(tǒng)是由專有文件DF（Dedicated File）和基本文件EF（Elementary File）組成的?？▋?nèi)數(shù)據(jù)的邏輯組織結構由專有文件DF的結構化分級組成。在根處的DF稱為主文件（MF） 。MF是必備的，其它DF是任選的?；疚募址譃閮?nèi)部基本文件和工作基本文件。其中內(nèi)部基本文件存放的數(shù)據(jù)由卡進行解釋，即為了達到管理和控制的目的，由卡來分析和使用這些數(shù)據(jù)；而對于工作基本文件，卡不能對文件中的數(shù)據(jù)進行解釋，而是由外界來使用這些數(shù)據(jù)。

對于智能卡文件系統(tǒng)中的三種文件類型：MF、DF、和EF，圖1給出了這三種文件的關系。其中，MF（第1級）為根文件，是必須有的，卡片中只能有一個MF 文件。它是在卡的個人化過程被首先建立起來，在卡的整個生命周期內(nèi)一直保持有效，可存儲卡片的公共數(shù)據(jù)信息并為各種應用服務?？ㄆ瑥臀缓?，自動選擇MF 文件為當前文件。DF（第2，3，...級）是可選的。包含用戶設置的系統(tǒng)信息和應用相關數(shù)據(jù)，在MF 下DF 的數(shù)量只取決與卡片容量和用戶的應用，它也可以包含若干的DF?；疚募﨓F是文件結構的末端，只包含系統(tǒng)信息、內(nèi)部數(shù)據(jù)或用戶數(shù)據(jù)。基本文件EF從結構上可分為四類，分別是透明結構、線性定長結構、線性變長結構和環(huán)形結構[4]。

2 多應用智能卡形式化建模現(xiàn)狀

在復雜的智能卡中，邏輯攻擊是非常敏感的，也就是說多應用智能卡的安全極易受到威脅。以下列出了在設計智能卡過程中幾條防止邏輯攻擊的策略：

1） 結構化設計：在卡中構建小的函數(shù)模塊，這樣可以更加簡單地理解和校驗。

2） 形式化驗證：使用數(shù)學模型去驗證函數(shù)的穩(wěn)固性。

3） 測試：對軟件的運行情況進行測試。

智能卡應用系統(tǒng)的安全環(huán)境很復雜，對智能卡的保護僅靠以上三條是遠遠不夠的，但是若在設計層面能盡可能地保證智能卡的安全性，在智能卡使用過程中就會在很大程度上減少智能卡的不可靠性[5]。

智能卡的安全機制保障了所下載的應用是無害的，并且遵循與初始化及訪問控制相關的基礎策略。這樣的基礎策略均為所有的智能卡必須遵循的基礎。所以，要來驗證安全機制是否遵循了這些基本策略是很重要的。因此，一個智能卡安全的重要的形式化方法應用是驗證平臺，驗證平臺旨在提供Java平臺和安全機制的抽象模型，并且驗證智能卡的安全功能是可靠的。然而，這不能充分說明我們對安全功能的設計是正確的，更不必說我們還需要保證智能卡其它部分也是安全可靠的：Java卡的API和GP（Global Platform）規(guī)范的API是智能卡組成的重要部分，兩個API的正確設計是對安全的核心需求。因此，對于平臺驗證的另一個重要的方面就是展示API是不是被正確設計了。endprint

平臺驗證對于智能卡的安全保證來講是最為基礎的一步，并且是通用標準評估的先決條件。然而，Java卡安全機制所提供的保障都是限制性的，并且進一步對應用是否對基礎設施合法使用進行了驗證，同時不可以嘗試任何敵對性的動作。所以，應用認證對智能卡的形式化方法來講是另一個重要的應用。平臺驗證和應用確認是保證智能卡安全的兩個重要方面[6]。

形式化方法是提高系統(tǒng)安全等級必不可少的保障技術。形式化方法使用謂詞邏輯、集合、關系等數(shù)學元素和原理表達系統(tǒng)中的部件及其運動規(guī)律，形式化方法的使用過程及形式規(guī)范、求精和實現(xiàn)等幾個階段，可以用于保證系統(tǒng)初始規(guī)范和后續(xù)過程的正確性和一致性。目前比較著名的形式化方法有Z語言，和由Z語言發(fā)展而來的B語言以及Event-B語言。

下面著重分析多應用智能卡中形式化方法的研究現(xiàn)狀。

2.1 Z方法

2.1.1 Z方法簡介

Z方法[7][8]最初是由法國學者Jean-Raymond Abrial等人設計的一種基于一階謂詞邏輯和集合論的形式規(guī)格說明方法，它采用了嚴格的數(shù)學理論，可以產(chǎn)生簡明、精確、無歧義且可證明的規(guī)格說明。

Z方法的核心是模式，它有兩種模式：狀態(tài)模式和操作模式。狀態(tài)模式定義目標軟件系統(tǒng)某一部分的狀態(tài)空間及其約束特性。操作模式[9]描述了系統(tǒng)某部分的行為特征，它通過描述操作前該部分的狀態(tài)值和操作后該部分狀態(tài)值之間的關系來定義系統(tǒng)該部分的一種操作特性。模式還可以修飾，模式修飾的作用是將修飾應用到被修飾模式的聲明部分中所有的變量[10]。

2.1.3 Z方法的應用：電子錢包

Z語言具有靈活且擴展性良好的特點，在安全應用系統(tǒng)開發(fā)實踐過程中獲得了巨大的成功。例如電子錢包系統(tǒng)規(guī)范就是運動了Z方法進行形式化描述。

電子錢包的形式化模型[11]主要包括兩個部分：抽象模型和具體模型。在電子錢包系統(tǒng)的抽象模型中，描述了整個錢包和電子交易的過程（如圖2） ，包括請求、支付和確認支付等步驟，表達了卡片必須遵守的安全屬性。在具體模型中，反映了錢包在交、

抽象模型的大致構建思路為：單個的電子錢包包括余額?？赡軗p失的數(shù)額兩個組件，在單個電子錢包的基礎上，可以將系統(tǒng)本身定義為電子錢包的集合體，在這里，每個錢包都有一個獨立唯一的名字。在此基礎上，建立從名字到錢包之間的映射，其自變量域是轉(zhuǎn)賬過程中要涉及到的已認證過的錢包，這樣就形成抽象系統(tǒng)空間。電子錢包的操作模式有兩類：輸入和輸出，即轉(zhuǎn)入和轉(zhuǎn)出。在抽象模型的基礎上，對該形式化模型進行精華，可以對系統(tǒng)的組件和操作進行實例化，添加某種安全性質(zhì)或消除某項安全假設，從而構造出更接近于實現(xiàn)的一個具體模型，并使其符合原有抽象模型的性質(zhì)和要求[12]。

2.2 B方法

2.2.1 B方法簡介

B方法[13]是一種用于描述、設計計算機軟件的方法，支持在從抽象到具體的各個層而上對軟件規(guī)范進行描述，覆蓋了從規(guī)范說明到代碼生成的整個軟件開發(fā)周期。B方法定義了一套數(shù)學推理和符號描述，支持在不同抽象層面上對軟件規(guī)范的內(nèi)在一致性和功能正確性進行嚴格的數(shù)學證明.人們已開發(fā)了一些商用和開源工具，支持基于B方法的軟件開發(fā)過程，支持自動或交互式的軟件規(guī)范證明.使用B方法進行軟件開發(fā)與傳統(tǒng)方法不同之處在于工程師先在抽象層面上（而不是最終在常規(guī)編程語言層面上）嚴格描述軟件功能，可以完全沒有執(zhí)行的概念，可以擺脫實現(xiàn)細節(jié)的干擾，只描述所開發(fā)軟件的最根本最重要的屬性，并嚴格證明其性質(zhì)，為后面開發(fā)出更可靠的系統(tǒng)打下堅實基礎。而在常規(guī)開發(fā)過程中，前期工作一直用非形式文檔，其內(nèi)在一致性和功能正確性沒有嚴格保證，只能靠人工檢查.

用B方法描述軟件的基本單元是抽象機，抽象機類似于我們常說的抽象數(shù)據(jù)結構，包括：數(shù)據(jù)描述（常量、變量等）、操作描述（數(shù)據(jù)上的一組操作）、不變式（數(shù)據(jù)狀態(tài)必須滿足的一組關系）。

要保證一個抽象機M的描述是完整的無矛盾的，需要證明由抽象機生成的不變式定理：

1） M的所有可能初始狀態(tài)都滿足它的不變式

2） 從任何滿足M的不變式的M抽象機狀態(tài)出發(fā)，執(zhí)行M的任何操作，可能達到的狀態(tài)必定滿足M的不變式。

3） 不變式定理和其他要證明的定理稱為“證明義務”，如果能證明由抽象機M生成所有不變式定理，M就是無矛盾的。

2.2.2 B方法的工具：Atelier-B

Atelier-B是由ClearSy開發(fā)，操作使用B形式化方法的證明工業(yè)工具軟件。用于由阿爾斯通和西門子等手工開發(fā)，對世界上各種地鐵安全自動化進行建模。根據(jù)“通用標準”發(fā)展模型系統(tǒng)，由Atmel公司和意法半導體（ST）進行標準認證。也被用于其他一些行業(yè)，如汽車電子3個車型經(jīng)營原則的建模。

Atelier-B中的主要工具及其關系如上圖所示。其中，B Compiler是最核心的部分。用于分析B模型的語義，證明類型的統(tǒng)一性、構造規(guī)則以及模型在B項目中的可見性。因此，是一個允許新應用產(chǎn)生的強大的庫。

最后，我們介紹一下Atelier-B的用戶界面。在運行Atelier-B之后出現(xiàn)的界面中，主要顯示項目中的組成部分以及證明結果，即類型是否一致，產(chǎn)生多少證明義務，以及成功證明和失敗證明的數(shù)量。雙擊項目名稱可編輯項目，即圖中最上面一層窗口，會顯示組成部分的具體信息以及之間的關系。圖中中間一個窗口時證明窗口，顯示證明義務是否成功證明，以及失敗的原因。[13]

智能卡是由許多邏輯和物理組件組成，旨在在發(fā)行者控制的環(huán)境中，使應用程序具備安全性和互用性。

Java卡不提供標準的機制來管理卡中的應用。為了從這樣的機制中獲取便利，大多數(shù)的Java卡同樣實現(xiàn)GP規(guī)范，GP給多應用智能卡的管理機制提供了已經(jīng)發(fā)布的工具。GP機制使用兩種截然不同的規(guī)格詳細描述，兩種分別描述卡的功能需求以及其相關的安全需求。智能卡的安全很強地依賴于GP的正確設計和實現(xiàn)，但是現(xiàn)在很少有使用形式化方法來分析GP的，B方法則是其中的一個例外。endprint

參考文獻：

[1] 王愛英.智能卡技術——IC卡[M].3版.北京：清華大學出版社，2009.

[2] 張之津.智能卡安全與設計[M].北京：清華大學出版社，2010.

[3] 劉玉珍，張煥國.多應用安全智能卡結構的研究[J].武漢大學學報（理學版），2006， 52（1）： 87-91.

[4] 李曉航.認證理論及應用[M].北京：清華大學出版社， 2009.

[5] Witteman M. Advances in Smartcard Security[J].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.

[9] Susan Stepney， David Cooper， Jim Woodcock. AN ELECTRONIC PURSE， Specification， Refinement， and Proof[R].

[10] 夏建勛，唐紅武.需求分析的Z語言形式化方法[J].科學技術與工程，2008，8，（8）：2245-2248.

[11] 李改成.安全應用系統(tǒng)的形式化規(guī)范與求精過程研究[J].信息網(wǎng)絡安全，2009（5）.

[12] Abrial J. The B-Book： Assigning Programs to Meanings[M]. Cambridge University， November 3， 2005.

[13] Global Platform[DB/OL].http：//www.globalplatform.org.

[14] Abrial J. Modeling in Event-B： System and Software Engineering[M].Cambridge University， 2010.

[15] 章玥，郭建，朱曉冉.基于模型的開發(fā)方法在多應用智能卡中的應用[J].信息網(wǎng)絡安全，2013， （12）：75-79.endprint

參考文獻：

[1] 王愛英.智能卡技術——IC卡[M].3版.北京：清華大學出版社，2009.

[2] 張之津.智能卡安全與設計[M].北京：清華大學出版社，2010.

[3] 劉玉珍，張煥國.多應用安全智能卡結構的研究[J].武漢大學學報（理學版），2006， 52（1）： 87-91.

[4] 李曉航.認證理論及應用[M].北京：清華大學出版社， 2009.

[5] Witteman M. Advances in Smartcard Security[J].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.

[9] Susan Stepney， David Cooper， Jim Woodcock. AN ELECTRONIC PURSE， Specification， Refinement， and Proof[R].

[10] 夏建勛，唐紅武.需求分析的Z語言形式化方法[J].科學技術與工程，2008，8，（8）：2245-2248.

[11] 李改成.安全應用系統(tǒng)的形式化規(guī)范與求精過程研究[J].信息網(wǎng)絡安全，2009（5）.

[12] Abrial J. The B-Book： Assigning Programs to Meanings[M]. Cambridge University， November 3， 2005.

[13] Global Platform[DB/OL].http：//www.globalplatform.org.

[14] Abrial J. Modeling in Event-B： System and Software Engineering[M].Cambridge University， 2010.

[15] 章玥，郭建，朱曉冉.基于模型的開發(fā)方法在多應用智能卡中的應用[J].信息網(wǎng)絡安全，2013， （12）：75-79.endprint

參考文獻：

[1] 王愛英.智能卡技術——IC卡[M].3版.北京：清華大學出版社，2009.

[2] 張之津.智能卡安全與設計[M].北京：清華大學出版社，2010.

[3] 劉玉珍，張煥國.多應用安全智能卡結構的研究[J].武漢大學學報（理學版），2006， 52（1）： 87-91.

[4] 李曉航.認證理論及應用[M].北京：清華大學出版社， 2009.

[5] Witteman M. Advances in Smartcard Security[J].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.

[9] Susan Stepney， David Cooper， Jim Woodcock. AN ELECTRONIC PURSE， Specification， Refinement， and Proof[R].

[10] 夏建勛，唐紅武.需求分析的Z語言形式化方法[J].科學技術與工程，2008，8，（8）：2245-2248.

[11] 李改成.安全應用系統(tǒng)的形式化規(guī)范與求精過程研究[J].信息網(wǎng)絡安全，2009（5）.

[12] Abrial J. The B-Book： Assigning Programs to Meanings[M]. Cambridge University， November 3， 2005.

[13] Global Platform[DB/OL].http：//www.globalplatform.org.

[14] Abrial J. Modeling in Event-B： System and Software Engineering[M].Cambridge University， 2010.

[15] 章玥，郭建，朱曉冉.基于模型的開發(fā)方法在多應用智能卡中的應用[J].信息網(wǎng)絡安全，2013， （12）：75-79.endprint