透過您的圖書館登入
IP:107.21.176.63
  • 期刊

作業系統核心安全驗證技術探討

摘要


穩定可靠的核心一直都是作業系統設計與實作的主要目標。尤其當核心功能越來越多樣時,龐大的程式碼,造成維護的困難,任何核心程式模組的錯誤,都會造成整個系統的停頓或安全的弱點,這是典型單核心系統(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)的主要驗證工具。

參考文獻


(2006).Jan Tobias Muhlberg and Gerald Luttgen.(Blasting Linux Code, ERCIM Working Group on Formal Methods for Industrial Critical Systems).
A. S. Tanenbaum and Linus Tovalds, Tanenbaum-Torvalds debate
A. Chou,J. Yang,B. Chelf,S. Hallem,D. R. Engler.(2001).In SOSP 2001.ACM Press..
Aaron Tomb, Guillaume Brat,Willem Visser..Variably interprocedural program analysis for runtime error detection.(ISSTA 2007).
B. Beizer(1990).Software Testing Techniques.International Thomson Press.

延伸閱讀