查詢結果分析
來源資料
頁籤選單縮合
題 名 | 作業系統核心安全驗證技術探討 |
---|---|
作 者 | 蔡昌憲; 許立文; 吳孟勳; 黃世昆; | 書刊名 | 資訊安全通訊 |
卷 期 | 14:2 2008.04[民97.04] |
頁 次 | 頁89-98 |
分類號 | 312.76 |
關鍵詞 | 軟體驗證; 反例引導抽象模型微調; 驅動程式驗證; 動態模型驗證; Software verification; CEGAR; SDV; Explicit model checking; |
語 文 | 中文(Chinese) |
中文摘要 | 穩定可靠的核心一直都是作業系統設計與實作的主要目標。尤其當核心功能越來越多樣時,龐大的程式碼,造成維護的困難,任何核心程式模組的錯誤,都會造成整個系統的停頓或安全的弱點,這是典型單核心系統(monolithic)的最主要問題。微核心(micro-kernel)的設計理念因此誕生。在此理念下,我們盡可能維持最少而必要的核心功能,將系統服務功能移到核心外,以致於系統核心的執行可被掌握、被驗證。但即使如此,仍有眾多的外掛模組,如驅動程式、程式介面攔截(如封包擷取)等被置於核心內部執行,以致系統的安全與可靠度不易掌握,因此軟體驗證技術就被應用於此,以進行相關核心功能的性質確認。這方面的驗證大致可分為幾項:1.外加驅動程式是否符合核心的使用規範,是否可能危害核心程式執行,2.執行緒(thread)是否會造成競爭的情況(race condition),3.有無存在未處理的例外情況(unhandled exception),4.有無共通性的程式錯誤,例如程式呼叫介面誤用、整數運算溢位與符號錯誤(Integer overflow/signedness)。我們將先介紹軟體驗證方法(software verification),所謂CEGAR(Counter Example Guided Abstraction Refinement)、藉由反例來引導抽象模型的微調,而代表性的工具包括SLAM, BLAST與MOPS,經由這些工具延伸發展出驅動程式驗證(SDV)系統、核心可靠性質的確認、與認證協定(authentication Protocols)的安全確認。其次,將介紹動態模型驗證(explicit model checking),這方面的代表性方法與工具包括DART, CUTE, EXE, SYNERGY與我們所發展的ALERT,經由這些工具有系統地激發潛在的核心錯誤與安全威脅,也將會成為未來確保系統安全(information assurance)的主要驗證工具。 |
本系統中英文摘要資訊取自各篇刊載內容。