跳到主要內容

臺灣博碩士論文加值系統

(75.101.211.110) 您好!臺灣時間:2022/01/26 13:49
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

: 
twitterline
研究生:楊嘉欣
研究生(外文):Chia-Hsin Yang
論文名稱:智慧卡作業系統的驗證
論文名稱(外文):Formal Verification of a Smart CardOperating System
指導教授:侯廷偉侯廷偉引用關係
指導教授(外文):Ting-Wing Hou
學位類別:碩士
校院名稱:國立成功大學
系所名稱:工程科學系碩博士班
學門:工程學門
學類:綜合工程學類
論文種類:學術論文
論文出版年:2002
畢業學年度:90
語文別:中文
論文頁數:99
中文關鍵詞:爪哇卡驗證智慧卡作業系統智慧卡
外文關鍵詞:Java Cardsmart cardsmart card operating systemformal verification
相關次數:
  • 被引用被引用:4
  • 點閱點閱:925
  • 評分評分:
  • 下載下載:189
  • 收藏至我的研究室書目清單書目收藏: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月
連結至畢業學校之論文網頁點我開啟連結
註: 此連結為研究生畢業學校所提供,不一定有電子全文可供下載,若連結有誤,請點選上方之〝勘誤回報〞功能,我們會盡快修正,謝謝!
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關期刊