簡易檢索 / 詳目顯示

回結果列表
研究生： 楊嘉欣
Yang, Chia-Hsin
論文名稱： 智慧卡作業系統的驗證
Formal Verification of a Smart Card Operating System
指導教授： 侯廷偉
Hou, Ting-Wing
學位類別： 碩士
Master
系所名稱： 工學院 - 工程科學系
Department of Engineering Science
論文出版年： 2002
畢業學年度： 90
語文別： 中文
論文頁數： 99
中文關鍵詞： 爪哇卡 、驗證 、智慧卡作業系統 、智慧卡
外文關鍵詞： Java Card, smart card, smart card operating system, formal verification
相關次數： 點閱：94  下載：2 
分享至:
查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報

    • 本研究以正規化方式驗証一個稱之ESCOS的IC卡作業系統的正確性。驗証一個智慧卡作業系統的特性在IC領域研究上或業界之共同標準(Common Criterion)都是相當重要。我們相信本研究是國內在IC卡領域中第一次的嚐試。我們藉由追蹤程式碼了解整個ESCOS如何運作，且將系統正規化至符合UPPAAL環境。UPPAAL為一模組、模擬及驗證的整合性工具環境。UPPAAL所測試的是ESCOS的執行流程，而非程式碼的正確性。ESCOS程式碼的正確與強韌度應由其他測試工具來執行，而非使用UPPAAL。我們發現ESCOS中一些並不危害本體的錯誤。修改後，經驗證可以驗証ESCOS為正確的系統且不具有deadlock的情形。

    This research is to toward formally prove the correctness of a smart card operating system, called ESCOS developed in our lab in July 2001. Proving the characteristics of an IC card operating system is very important in the IC card field such as the fillment of the Common Criterion requirements. We trace the ESCOS code to understand how ESCOS works, and formalize the descriptions of ESCOS to fit into the UPPAAL environment, which is an integrated tool environment for modeling, simulation, and verification. UPPAAL can only verify the correctness of the flows (execution paths) of the specified system. As for the correctness and robustness of the code is not covered. We find some minor errors in ESCOS. The final version of ESCOS is verified of its correctness and it is a deadlock-free smart card operating system.

    中 文 摘 要 i Abstract ii 致謝 iii 表目錄 vi 圖目錄 vii 圖目錄 vii 第一章 緒論 1 1.1研究動機與背景 1 1.2 研究目的 2 1.3 章節概要 3 第二章 智慧卡作業系統 4 2.1 智慧卡作業系統之介紹 4 2.1.1 智慧卡作業系統(COS)簡介 4 2.1.2 智慧卡作業系統的生命週期(COS Life Cycle) 5 2.1.3 智慧卡作業系統與卡機互動之情境(scenario)圖 6 2.1.4 COS之作業狀態(Process State) 7 2.1.5 不可分割之寫入需求(Atomic write requirement) 9 第三章 ESCOS介紹 12 3.1 設計過程 12 3.2 檔案 13 3.2.1 檔案組成之資料結構 13 3.2.2檔案資料結構整理 18 3-2-3檔案搜尋及管理 19 3-3 APDU 命令(command) 21 3.4檔案安全控管機制 23 3.5 ESCOS實作 24 3.5.1 各系統類別意義 26 3.5.2 I/O Layer介面整理 27 3.5.3 各系統類別介面整理 29 第四章 ESCOS系統的模組與驗證 32 4.1 正規化驗証(Formal Verification) 33 4.2 驗證工具的選擇 34 4.3 系統分析 36 4.4 系統的建構與模擬 40 4.5 系統驗證 43 4.6 驗證實例 44 4.7 系統驗證結果與修正 50 第五章 結論與未來工作 51 5.1 結論 51 5.2 未來工作 51 參考索引 54 附錄一 UPPAAL之介紹 56 附錄二 The System Description 72 自述 99

    [BeLa96] Johan Bengtsson and Fredrik Larsson, “UPPAAL a Tool for Automatic Verification of Real-Time Systems.”, DoCS Technical Report Nr 96/67, Uppsala University, ISSN 0283-0574, January 1996.
    [CC99] Common Criteria(CC), Common Criteria for Information Technology Security Evaluation-User Guide, 1999
    [CHEN00] Zhiqun Chen, Java Card Technology for Smart Cards, Addison-Wesley, 2000.
    [EMV98] Europay International S.A., MasterCard International Incorporated, and Visa International Service Association, Integrated Circuit Card Specification for Payment Systems, Version 3.1.1, May 1998.
    [Gupt92] A. Gupta. “Formal hardware verification methods: a survey.” Formal Methods in System Designs, vol.1, 1992, pp.151-238.
    [HeHW97] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, “HyTech: A Model Checker for Hybrid Systems.”, Software Tools for Technology Transfer, vol.1, no.1+2, 1997, pp.110-122.
    [ISO7816] ISO/IEC, ISO 7816, ISO, 1989~1995.
    [Karp83] Richard Alan Karp, Proving Operating System Correct, UMI Research Press an imprint of University Microfilms International Ann Arbor, Michigan 48106, 1983
    [LAPW97] Kim G. Larsen, Paul Pettersson, and Wang Yi, ”UPPAAL in a Nutshell”, In Springer International Journal of Software Tools for Technology Transfer, vol.1, no.1+2, 1997, pp.34-152.
    [Mcfe93] M.C. McFerland. “Formal Verification of Sequential Hardware: a Tutorial.” Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, vol: 12, issue: 5, pp: 633 –654, May 1993.
    [Scha99] Stephen R. Schach, Classical and Object-Oriented Software Engineering, McGraw-Hill INTERNATIONAL EDITION, 1999.
    [SUN97] Sun Microsystems, Inc ,Java Card 2.0 Application Programming Interfaces, Final Revision 1.0,October 1997.
    [SUN99A] Sun Microsystems, Inc ,Java Card Applet Developer's Guide, Java Card Version 2.1, August 1999.
    [SUN99B] Sun Microsystems, Inc ,Java Card 2.1 Runtime Environment(JCRE) Specification, Final Revision 1.1, June 1999.
    [SUN00A] Sun Microsystems, Inc ,Java Card 2.1.1 Runtime Environment (JCRE) Specification, Revision 1.0, May 18, 2000.
    [SUN00B] Sun Microsystems, Inc ,Java Card 2.1.1 Virtual Machine Specification, Revision 1.0, May 18, 2000.
    [SUN00C] Sun Microsystems, Inc ,Java Card 2.1.1 Application Programming Interface, Revision 1.0, May 18, 2000.
    [SUN00D] Sun Microsystems, Inc ,Java Card 2.1.1 Development Kit User's Guide, Version 1.0P, June 1, 2000.
    [SUN01] Sun Microsystems, Inc ,Java Card 2.1.2 Development Kit User's Guide", Revision 1.0, Apr 11, 2001.
    [RaEf00] W. Rankl, W. Effing, Smart Card Handbook Second Edition, John Wiley & Sons, Ltd., Auguest 2000.
    [WaHs02] Farn Wang and Pao-Ann Hsiung, “Efficient and user-friendly verification”, IEEE Transactions on Computers, vol.51, no.1 , Jan. 2002, pp. 61 ~83.
    [李卓俊01] 李卓俊，一個具支援Java Card的智慧卡作業系統雛形之設計與實作，國立成功大學工程科學研究所碩士論文，June 2001.
    [林昆弘98] 林昆弘，應用於Java執行環境之虛擬平台的設計與實作，國立成功大學工程科學研究所碩士論文，1998.
    [侯廷偉98] 侯廷偉，嵌入式Java VM之研究，資策會研究計劃期末報告，June 1998.
    [侯黃01] 侯廷偉、黃志文，澎湖地區健保IC卡第四期實驗計畫整體委外服務專案中央健保局期末報告，2001.
    [趙侯00] 趙健民、侯廷偉，澎湖地區健保IC卡第三期實驗計畫整體委外服務專案中央健保局期末報告，2000.
    [馬天彥00] 馬天彥，Java Card實作FISC規格健保IC卡及系統應用程式之規劃，國立成功大學工程科學研究所碩士論文，June 2000.
    [財金99] 財金公司(原金融資訊服務中心,FISC), IC金融卡規格書, V2.0，IC金融卡規格書.
    [健保局98] 中央健康保險局高屏分局, 行政院衛生署中央健康保險局『澎湖地區IC卡實驗計劃IC卡採購、製作、發行採購案』期末報告, 民國87年6月

    下載圖示 校內：立即公開
    校外：2002-08-19公開
    QR CODE