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

蔡昌憲 ； 許立文 ； 吳孟勳 ； 黃世昆

《資訊安全通訊》 14卷2期 (2008/04) Pp. 89-98

https://doi.org/10.29614/DRMM.200804.0005

摘要

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

關鍵字

軟體驗證Software Verification ； 反例引導抽象模型微調CEGAR ； 驅動程式驗證SDV ； 動態模型驗證Explicit Model Checking

參考文獻

Dzintars Avots,Michael Dalton,V. Benjamin Livshits,Monica S.(2005).Lam: Improving software security with a C pointer analysis.ICSE 2005.332-341.

Thomas Ball,Sriram K. Rajamani(2001).Automatically Validating Temporal Safety Properties of Interfaces, SPIN 2001.Workshop on Model Checking of Software, LNCS 2057.103-122.

Thomas Ball,Sriram K. Rajamani.(2002).The SLAM Project: Debugging System Software via Static Analysis.1-3.

B. Beizer(1990).Software Testing Techniques.International Thomson Press.

Dirk Beyer,Adam J. Chlipala,Thomas A. Henzinger,Ranjit Jhala,Rupak Majumdar(2004).Proceedings of the 11th International Static Analysis Symposium (SAS 2004).Springer-Verlag.