C程式中正負整數轉換錯誤之偵測

Abstract

每天都有新弱點被發佈，其中有些惡名昭彰的弱點是多數程式員所熟悉的，例如，錯誤使用未限制的複製函數、或接受格式字串的函數。近幾年來，一種稱為整數錯誤的新型態程式弱點被發掘，許多重要的應用程式都有這樣的程式弱點，例如Microsoft Internet Explorer 以及 PHP等系統。這種弱點是由於整數溢位後，被運用於配置記憶體。因為整數溢位，配置的記憶體將少於所預期的數量，因而也造成記憶體溢位問題。正負整數轉換是所有整數問題的一部分，我們將在論文中探討、偵測此類問題的方法。

在論文中，我們提出一種偵測技術，以檢驗正負整數轉換相關運算，找出Ｃ程式可能的錯誤。此方法是基於程式控制流、與實際/符號混合測試技術(Concolic testing)。當測試到潛在問題時，我們使用總體特性檢查 (Universal Property Checking)，更進一步驗證常見、且已知軟體的弱點，判斷是否會引發正負整數轉換問題。

我們提出的方法，已在linux2.6.17平台上評估，對幾個有代表性的程式類型進行測試。這些類型分別為：(1)正號整數轉負號整數、(2)負號整數轉正號整數、(3)以及語意錯誤。對於真實案例評估，我們也偵測到qemu 0.8.2中的程式錯誤。

New vulnerabilities in software come out every day. Some of them are so infamous that most programmers are familiar with, e.g. misuse of unbounded copy functions or format string functions. A new type of vulnerability, called integer errors, emerges in recent years. Many major applications suffer from this kind of vulnerability, for example, Microsoft Internet Explorer and PHP. The vulnerability is caused by integer overflow and the integer is then used as size field to allocate heap memory. Because of the integer overflow, the allocated heap space is far less than what the programmers expect, thereby causing heap overflow then.

We have developed a technique that aims at finding integer signedness bugs in C programs. This technique is based on CONCOLIC-testing (CONCrete and symbOLIC) and control-path analysis. The control path analysis of the target program will help us identify the program input data which cause a suspicious integer conversion. This suspicious integer conversion may turn to integer signedness bugs by some rare input data. Then we use concolic testing and universal checking to verify whether there is a feasible bug that will be caused by this suspicious integer conversion.

The proposed method, called reflter algorithm, has been evaluated in Linux 2.6.17 with several representative program examples, including signed-to-unsigned and unsigned-to-signed conversions, along with semantic bugs. This method also detects a real bug in qemu 0.8.2.