GSS 資安電子報0015期【使用程式碼靜態分析建構系統安全 】

所有的軟體專案都脫離不了一個共通特性— 一定得撰寫程式碼。以結構化進行風險分析¹，程式碼檢核是軟體安全最佳範例相當重要的一個手段(圖一)²。我們就來看看如何自動化進行源碼的靜態分析檢測。

自從2000年發表ITS4檢測工具以來，程式碼檢測已行之有年。ITS4這個工具很簡單，基本上掃瞄檔案後，與「規則檔」進行語句比對找出弱點(例如應避免使用strcpy()函式)，並使用更好的程式寫作方式。

開發人員寫程式總是會犯些小錯誤—這邊少一個分號，那邊多一個括號。這些問題多半無傷大雅，編譯器能找出這些問題，開發人員修正錯誤，程式開發持續的進行。這樣的尋找臭蟲過程並不能找出程式碼安全弱點，弱點潛藏越久，修正的代價也越高，而程式開發人員一直在重複這樣的錯誤。靜態分析就是在程式上線前自動找出這些安全弱點。

靜態程式碼分析以靜態方式分析程式碼，不必執行。理論上，即使反組譯的難度比較高，工具還是可以檢查源碼或是編譯過的碼。我們在此討論源碼檢測，因為不需要再額外使用繁瑣的反組譯技術。

人工檢核程式碼也算是一種靜態檢測，但非常耗時。檢核者必須擁有資安相關知識，才有辦法勝任。靜態檢測工具相較之下速度很快，也可以經常使用，操作工具者也不需像人工稽核一般必須擁有相當程度的資安知識。就像是程式設計師倚賴編譯器找出語法的問題，工具操作人員只要具備資安基礎知識就可以輕鬆愉快的檢測。

掃瞄弱點背後運作機制相當複雜，因為程式碼的深度與弱點出現位置都不可預測。靜態分析工具不需要像動態分析勞師動眾使用許多技術，而且可以在程式碼真正撰寫完成，進行密集的測試之前，進行多次的靜態分析檢核。

靜態分析無法解決我們所有問題。新進的廠商把比對模式或規則寫死在程式裡，而比較成熟的工具允許新增規則，倘若沒有新的規則，工具也找不到新的問題。所以要當心某些工具告訴你「沒有找出問題，你的程式目前很安全」這種鬼話，這些話應該要改成「對不起，我們沒能找出其他的問題」。

靜態工具掃瞄的結果仍舊需要人工檢核，工具無法知道問題對你的重要性，也無從判斷哪些問題必須修正，或是可接受的風險。我們都希望軟體的缺點越少越好，即便靜態分析工具可以找出大部分的安全問題，但他仍無法幫助我們設計出更好的軟體。別寄望工具能告訴我們「我發現你安裝了一個轉帳的程式，你應該要檢核使用者輸入密碼的強度與安全」。 

Rice定律提到，任何與程式相關、有意義的問題，可以簡化為halting problem(*註一)。換句話說，靜態分析問題最壞狀況(worst case)是無法產出結果的。Rice定律問題通常解法是，靜態分析工具強迫產出最接近正確的結果。工具也可能產出漏判(工具沒有報出程式存在的問題)或誤判(工具報出不存在於程式的問題)的狀況。分析人員追根究底後看到誤判心情都不會太好，但是比較起來漏判更顯的危險，代表工具對於安全性的敏感度不足。設計考慮周全的工具不應該出現漏判，但有些誤判訊息可能會移至警告訊息類別。太高的誤判率讓分析結果成為笑柄，有可能使得團隊不再使用靜態分析工具，反而造成完全的漏判。

*註一：halting problem以通俗的說法，就是判斷一個程式，是否能在有限的時間內執行完畢。

也許Unix的grep指令是最簡單，也最直覺的靜態分析方法。Grep指令的搜尋字串能力，用來對付程式碼是最好不過。缺點則是grep並不瞭解他掃瞄的是什麼檔案。註解、字串、宣告與函式呼叫也都只是比對的字元一部份而已，比較好的作法是加入程式語言的語彙規則。這樣做工具可以分辨有風險的函式呼叫

gets(&buf); /*註解：千萬不要使用gets()*/

和一行無關的程式碼

int begetsNextChild = 0;

基本的語彙分析能力已實作在分析工具的先期分析過程，包括ITS4、FlawFinder
(www.dwheeler.com/flawfinder/)與RATS (www.securesoftware.com)等工具，將程式碼轉為符記(token，這也是編譯器進行編譯的第一步)，再讓符記與弱點函式庫進行比對。更早之前，Matt Bishop與Mike Dilger寫了一支檢查TOCTOU(time-of-check與time-of-use)專用的語彙分析工具³。

即使語彙分析工具比grep指令強了許多，因為沒有針對語意進行分析，誤報率也很高。轉譯為符記比起直接將程式碼載入要來的好，但是要瞭解程式碼運作仍有一大步要走。有些高安全風險的程式碼辨視度很高，不需要再進行語意分析就可正確判斷，但大部分都不是這麼好判斷。
為了提高精確度，分析工具必須採用許多編譯器的技術，例如將源碼編譯為AST(abstract syntax tree)檔這種語意分析技術就會納入。

有了AST技術，下一步要決定分析範圍。Local analysis一次檢查一個函式，不考慮函式之間的關係。Module-level analysis檢查一個類別，或整個編譯單元，所以要考慮同一編譯單元函式之間的關係，但是不檢查跨模組之間的函式關係。Global analysis必須分析整支程式，所以必須考慮所有函式之間的關係。

上下文的關連性(context)分析也必須在分析範圍裡決定。若要減少誤判，要檢查的上下文關連性的範圍勢必變大，但是得花很多計算時間。

研究人員研究出許多語意判斷的方法，有些很好，有些則否；有些是偵測特定的類別語意，有些則很彈性的能偵測多種語意。我們來看看這些工具：

• BOON能偵測整數範圍分析，檢查C程式的變數長度是否超出陣列範圍⁴。他能做到許多語意分析工具無法分析的錯誤，不過準確度卻不太夠，他會略過程式碼的先後順序，也不能找出不同函式呼叫之間的關係，也找不出有別名的指標所形成的注入問題(injecction)。
• 以Perl的taint mode為發想，CQual使用型別辨識子(type qualifier)進行C語言的變數污染分析(taint analysis)⁵。CQual需要程式設計師標出一些被污染或未污染的變數(搭配系統函式庫)，以利辨識子進行傳遞(qualifier propagate)。一旦傳遞完成，工具便可偵測字串格式，以型別檢查方式找出安全弱點。
• Xg++工具在編譯器裡結合樣版方式(template driven)，在Linux與OpenBSD裡找出kernel的弱點⁶。他找出kernel裡何處使用未經驗證，不被信任的資料，或使用者呼叫的方法沒有正確釋放記憶體，或使用者導致kernel產生死結(deadlock)。
• Eau Claire工具使用theorem prover組成檢核架構，尋找C語言的弱點⁷。他可以找到像是緩衝區溢位、檔案存取的資源競爭(race-condition)、與字串格式等臭蟲。程式設計師可以使用這個工具確保程式如預期般的執行。
• MOPS工具使用model-checking技術檢驗程式碼是否違反安全屬性⁸。開發人員能對安全屬性進行塑模(modeling)，其他人員可以檢驗特殊權限管理問題、Linux上面chroot jail的不正確設定、檔案存取的資源競爭、或ill-conceived temporary file schemes。
• Splint將lint觀念延續至資安領域⁹。程式開發人員可利用這工具找出abstraction violations、全域變數的unannounced modifications、和可能發生的use-before-initialization錯誤。Splint還可以找出變數是否超過陣列範圍。目前靜態分析技術很多，但是跟資安有關的卻不多。其中值得一提的是ESP(一種大規模驗證的技術)¹⁰，還有像是SLAM與BLAST可做model checker(使用predicate abstraction技術檢驗程式的安全屬性)¹¹,¹²，還有FindBugs(一個頗受好評的輕量級檢查工具，可找出Java程式碼一般的問題)¹³。

許多商用軟體工具廠商也開始重視靜態分析，亦採用了上面所提到的檢測技術，並漸漸成為主流技術。

即使對非資安背景人員，好的靜態檢測工具應該要能容易上手。這表示產出的結果應該讓一般不是很瞭解資安的開發人員也能容易搞懂，並且能教育開發人員什麼是安全的開發方式。另一個重要的功能是工具擁有的規則資料庫，規則資料庫的比對能力不應該被神話。

最後，好的靜態檢測工具可以協助點出並消除一般常見的安全問題，這對已經有很大的比對規則資料庫的C語言特別重要。靜態分析技術應成為程式開發流程的一部份，以降低風險。

1. D. Verndon and G. McGraw. “Risk Analysis in Software Design,” IEEE Security & Privacy, vol. 2, no. 5,
2004, pp. 79–84.
2. G. McGraw, “Software Security,” IEEE Security & Privacy, vol. 2, no.2, 2004, pp. 80–83.
3. M. Bishop and M. Dilger, “Checking for Race Conditions in File Accesses,” Computing Systems, vol.
9, no. 2, 1996, pp. 131–152.
4. D. Wagner et al., “A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities,”
Proc. 7th Network and DistributedSystem Security Symp. (NDSS2000), Internet Soc., 2000, pp. 3–17.
5. J. Foster, T. Terauchi, and A. Aiken, “Flow-Sensitive Type Qualifiers,” Proc. ACM Conf. Programming
Language Design and Implementation (PLDI2002), ACM Press, 2002, pp. 1–12.
6. K. Ashcraft and D. Engler, “Using Programmer-Written Compiler Extensions to Catch Security
Holes,” Proc. IEEE Symp. Security and Privacy, IEEE CS Press, 2002, pp. 131–147.
7. B. Chess, “Improving Computer Security using Extended Static Checking,” Proc. IEEE Symp. Security
and Privacy, IEEE CS Press, 2002, pp. 118–130.
8. H. Chen and D. Wagner, “MOPS: An Infrastructure for Examining Security Properties of Software,”Proc. 9th ACM Conf. Computer and Communications Security (CCS2002), ACM Press, 2002, pp. 235–244.
9. D. Larochelle and D. Evans, “Statically Detecting Likely Buffer Overflow Vulnerabilities,” Proc.
10th Usenix Security Symp. (USENIX’01), Usenix Assoc., 2001, pp. 177–189.
10. M. Das, S. Lerner, and M. Seigle, “ESP: Path-Sensitive Program Verification in Polynomial Time,”
Proc. ACM Conf. Programming Language Design and Implementation (PLDI2002), ACM Press, 2002,
pp. 57–68.
11. T. Ball and S.K. Rajamani, “Automatically Validating Temporal Safety Properties of Interfaces,”
Proc. 8th Int’l SPIN Workshop on Model Checking of Software, LNCS 2057, Springer-Verlag, 2001, pp.
103–122.
12.T.A. Henzinger et al., “Software Verification with Blast,” Proc. 10th Int’l Workshop Model Checking of
Software, LNCS 2648, Springer-Verlag, 2003, pp. 235–239.
13. D. Hovemeyer and W. Pugh, “Finding Bugs is Easy,” to appear in Companion of the 19th Ann. ACM
Conf. Object-Oriented Programming, Systems, Languages, and Applications, ACM Press, 2004.

Brian Chess是Fortify Software首席科學家。他的研究領域包括程式碼靜態分析、缺失塑模(defect modeling)與布林可滿足性(Boolean satisfiability)。他在University of California, Santa Cruz獲得博士學位。可利用電子郵件brian@fortifysoftware.com與他聯絡。

Gary McGraw是Cigital的首席科學家。他在大型軟體公司累積許多實際顧問經驗。同時他也是Exploiting Software (Addison-Wesley, 2004), Building Secure Software (Addison- Wesley, 2001), Java Security (John Wiley & Sons, 1996), 與其他四本書的共同作者。他在維吉尼亞大學獲得哲學碩士學位，隨後在印第安那大學取得電腦科學與認知科學雙博士學位。可利用電子郵件gem@cigital.com與他聯絡。

Fortify公司是軟體安全市場的領導者。我們的產品—Fortify Source Code Analyzer、Fortify PTA與Fortify RTA—
提供最準確、最完整的可信賴安全解決方案，供業界保護重要的應用程式。我們提供您在軟體生命開發週期最高等級的自動防護措施，降低組織的成本與風險。

我們頂尖的資安專家，與導入財星前100大企業的業界最佳範例，證明我們為資安業界頂尖廠商。我們保護全美前10大中的9家銀行，政府機關、通訊業、電子商務業者、出版業、保險業、系統整合業與資訊管理業間大型、重要的應用系統。

歡迎瀏覽我們的網站www.fortifysoftware.com 。