摘 要:為滿足大規模軟件開發的需要,自動化成為軟件工程迫切的要求,并貫徹到軟件設計、開發和維護的各個階段。本文提出一種以可計算函數為基礎的程序理解方法,最大程度地識別函數功能、驗證組件的安全屬性,實現對源代碼、二進制代碼的函數理解,以精簡的函數表達式和并發賦值形式展示函數理解結果,提高人工閱讀程序的效率,并且以可計算函數程序理解方法輔助軟件測試用例生成,對軟件安全的屬性進行評估。將軟件工程中的軟件設計規范、軟件產品、安全屬性等轉換成可計算過程實現軟件工程的智能管理。
關鍵詞:可計算函數語言 并發賦值形式 表達式傳播
中圖分類號:TP31文獻標識碼:A文章編號:1674-098X(2011)01(b)-0032-03
軟件開發的復雜性和代價一直以來都是軟件工程中的難題。由于軟件產品中大量的底層代碼細節和交錯的關系迅速超過了理解和記憶的范圍[1-2],復雜性極大地限制了軟件開發規模,成為軟件工程中的固有癥結。特別是在軟件測試過程中,測試人員閱讀所有的設計文檔、使用手冊、甚至源代碼,大量的時間消耗在軟件功能理解上。軟件復雜性也限制了測試工作的效率。軟件開發代價與軟件復雜性密切相關,未能正確地估計軟件的復雜性常常使得軟件開發的開銷超過了預算。在現代軟件工程中軟件開發規模必須加以控制,才能保證軟件的質量。
到21世紀,在開發超大規模軟件的需求下,新一代軟件工程急需要科學的自動化軟件管理工具和技術,貫徹軟件整個生命周期。下一代軟件工程的主要目標是使得軟件工程成為可計算過程。軟件工程的每個過程都應該成為可計算的評估過程,這包括軟件需求說明、軟件設計規范、軟件實現和軟件測試的全過程,可計算過程能夠在系統軟件的控制下,實施精確計算和評估。
近幾年來,人們已經關注到下一代軟件工程理論基礎和技術的研究。Linger、Pleszkoch和Hevner[1-4]等人提出了函數功能自動抽取技術,并應用到對惡意代碼分析中。Function Extraction[8]項目成為Cert軟件安全資助的在研項目之一。Function Extraction技術還被用于軟件驗證[1]、軟件測試[2]和惡意程序輔助理解中[4]。Function Extraction將影響軟件工程的多個方面[3]。
實現計算機對程序的自動理解一直是研究人員追求的目標之一。Pleszkoch提出使用函數抽象方法理解程序的功能[5],認為程序理解的基礎是函數理論[6]。隨著程序理解研究的深入,程序理解已經被應用到軟件智能調試、軟件自動測試和軟件安全漏洞發掘等領域。隨著符號執行和抽象解釋等新方法的引入,程序自動理解將從外部和內部來自動識別程序的運行時的特征。其他的軟件工程使用的技術如基于序列[7]、統計的軟件驗證技術、模型驗證技術、可攜帶證明代碼等都成為當前研究的熱點。
本文主要討論了下一代軟件工程的最新研究領域:程序自動理解技術。函數功能理解是最大限度地理解函數功能、驗證程序的正確性和控制軟件質量。可計算函數程序理解是下一代軟件工程的基礎技術,只有讓計算機從語義上理解了函數功能,才能真正做到軟件工程自動化。
1 并發賦值形式
函數理論觀點為函數功能計算提供了數學基礎。按照可計算函數理論,程序具有普通函數特點,程序將數據從輸入域映射為輸出域,可以認為程序是函數的集合,不管程序處理的何種對象和使用何種編程語言,都是將輸入映射到輸出。函數理論方法的核心是識別程序每個基本結構的功能以及它們的組合關系。
計算機程序是一種典型的序列邏輯,語句的執行有嚴格的序列關系,這種冗長的序列邏輯關系影響了函數功能的理解。計算機程序運行的基本特點是按照指定的序列順序執行,執行的上下文保存在動態內存中,計算機可以絲毫不差的按照程序規定的指令運行。
由于受到人的記憶的限制,程序運行時上下文環境和復雜的邏輯結構是人工程序理解的最大障礙,并發賦值是以并發程序為基礎的程序表示形式,并發語句之間沒有先后次序,每一條語句都是一個獨立的功能單元,并發語句基本形式記做:
[C1→Assign1; C2→Assign2;…;]
并發賦值的函數理解就是將順序執行的函數轉換成并發語句形式,并發語句就是函數的獨立功能,這種轉換的過程就成為函數功能理解的過程之一。
2 可計算程序理解
程序是由多個有限大小的基本結構組成,每個基本結構都可以使用函數的方法表示輸入到輸出的轉換,因而程序可以用函數的集合表示。函數功能理解是新一代軟件工程的基礎技術,只有讓計算機從語義上理解了函數功能,才能真正做到軟件工程的自動化。
可計算程序理解主要過程可以分為程序基本塊計算、表達式傳播和程序理解結果解釋。程序理解結果解釋主要是以合適的方式展示程序理解的結果,是程序理解的后端。
并發賦值程序最大的特點是與過程無關,使用可計算的函數表示軟件的控制流和數據流,提供函數功能理解的基礎。在通用程序設計語言中,順序結構和條件語句結構能夠直接轉換成并發賦值語句;對于循環結構則使用遞歸等式和選擇結構表示。例如在程序P中,條件語句q,分支操作語句分別是g和h,程序P可以轉化成并發賦值程序f。
P: if q then g else h endif
f =T(P)
CCA: f=([q]=true→[g]|[q]=1→[h])
條件選擇程序P轉換成并發賦值程序f,可計算函數f是兩個分別具有條件判斷的并發語句。while語句是循環結構的典型形式,使用可終止遞歸函數表示while語句塊功能[2]。
P1:while q
do g
end while
while循環語句轉換成等價CCA形式程序f:
f=T(P)
CCA: f = [ if q then g; while q do g enddo endif ]
簡單賦值語句是并發賦值程序的基本形式,也是最簡單的函數,是數據從輸入到輸出的不變轉移。表達式傳播是數據經過變換、轉移到達目標變量的過程,傳播的基礎就是并發賦值語句。對于復雜的程序設計結構,如順序和選擇結構的程序可以直接使用函數組合的方法計算程序功能。函數組合使用基本的代數運算符號連接兩個或多個可計算函數,如選擇符號‘|’、并且符號‘’、組合‘o’等等。可計算函數傳播的過程是自底而上逐步構建整個函數樹的抽象過程,程序控制結構最終轉換成與過程無關的并發賦值形式。每一條并發賦值語句都是程序功能的一部分,并發賦值語句直接解釋了程序功能。
3 軟件測試
為保證軟件使用的可靠性,通常在產品發布前要經過多種測試,目前軟件測試的方法主要是黑盒測試、灰盒測試和白盒測試。軟件測試和驗證是既耗時又耗力的過程。無論使用何種軟件測試方法,測試員都需要掌握測試對象的功能。軟件設計和實現文檔可以幫助測試人員了解軟件的基本操作,但是難以提供代碼級別的測試信息,測試員只能通過閱讀源代碼的方法,進一步獲取函數內部功能信息。
因此全面反映程序功能的函數理解技術對軟件測試過程和結果將產生巨大影響。由于軟件測試的主要目標是驗證軟件的功能,可計算函數程序提取函數的語義信息,以增加人們對程序分析、驗證和測試的能力。下面以一個例子闡述可計算函數程序在軟件測試中的應用。
三角形的邊長必須滿足一定的條件才能夠組成三角形,檢查這三個整數的C程序,首先檢查三個整數是否是正數,然后檢查兩邊之和是否大于第三邊。
int triangle(int a,int b,int c)
{
int answer = 1;
if(a<=0|b<=0|c<=0)
answer = 0;
if(a+b<=c|a+c<=b|b+c<=a)
answer = 0;
return answer;
}
經過VC++ 6.0編譯生成可執行文件。在對部分軟件進行功能測試時,無法提供源代碼,對軟件功能的測試只能從二進制文件開始。可計算函數的程序理解可以直接對機器碼進行翻譯并進行功能分析。使用IDA pro對三角形判斷函數反編譯,結果如圖1所示。按照二進制代碼的可計算程序理解方法對IDA 反編譯的結果進行并發賦值語句轉換與表達式傳播計算,程序理解輸出計算后的結果。
[
1. Arg_0:=signed_32(M,4 +d ESP)
2. Arg_4:=signed_32(M,0c +d ESP)
3. Arg_8:=signed_32(M,18 +d ESP)
4. dl:=(Arg_4 +d Arg_8<=Arg_0)
5. bl:=(Arg_0 +d Arg_4<=Arg_8)
6. al:=(Arg_0 +d Arg_8<=Arg_4)
7. (Arg_0<=0|Arg_4<=0|Arg_8<=0) → return 0
8. (al|bl|dl)→ return 0
9. (┒(al|bl|dl| Arg_0<=0|Arg_4<=0|
Arg_8<=0)) → return 1
]
輸出結果的開始部分是函數參數定義,參數Arg_0、Arg_4、Arg_8分別位于函數棧中,signed_32表示參數是雙字大小,+d代表有符號32位整數加法,dl、bl、al保存了比較的結果。下半部分是函數返回時參數需滿足的不同條件:如果任意一個參數小于等于0,則返回結果0;如果任意兩個參數之和比第三個參數小,則返回0,其他情況返回1。相對于軟件IDA pro 反編譯的的代碼,可計算函數分析結果清晰得多,也便于人員理解。
對于函數功能測試,根據可計算程序理解分析結果,在函數功能測試中7、8、9三條CCA語句分別代表了三個測試區域。可計算程序理解將大量的測試用例劃分成三個區域,每個區域只需要選擇代表性的例子就可以覆蓋整個功能測試區域。如果對程序的安全性進行檢查,還能夠發現程序存在整數溢出的可能。例如在語句4,+d表示32位整數加法,實際上是dl:=((Arg_4 +d Arg_8)Mod32<=Arg_0),只要Arg_4、Arg_8之和超過2^32,則發生整數溢出,計算的結果可能不準確,例如參數為2^32-1、2^32-1、100,函數返回0,程序發生整數溢出而出現錯誤。而常規的軟件覆蓋測試,如語句覆蓋、分支覆蓋、和路徑覆蓋等不能發現此類漏洞。
4 總結與展望
函數編程語言、PCF、SSA等可計算函數方法作為計算機程序的形式研究的方法,以數學計算為基礎,體現了數學公式精確、簡潔等特點。可計算函數的程序理解方法將程序看作是一個數學函數,將輸入數據映射為輸出結果,用數學公式表述函數的執行過程,結合控制流圖和表達式傳播計算方法抽象出函數的最終功能,對函數功能按照特征分類存入功能數據庫中。可計算函數的程序理解方法能夠對源代碼程序自動分析,對于二進制代碼程序,需要在反編譯工具的輔助下,直接分析匯編代碼,減輕了軟件維護和軟件測試人員的負擔。
受到人力的限制,下一代軟件工程需要廣泛的自動分析和驗證軟件產品的能力,從軟件規范、設計到軟件實現的各個環節,軟件產品都需要在可控和可計算的范圍內,可計算函數的程序理解以數學理論為基礎,能夠適應源代碼、中間級代碼、匯編代碼等多個層次的對象,成為新一代軟件工程的重要方面。
可計算函數的程序理解方法在新一代軟件工程還能用于軟件質量管理:
(1)軟件組件正確性驗證計算
提高軟件工程中可靠組件的粒度,例如對于上億行代碼的系統,如果每個可靠組件大小是千行,那么系統就包含十萬個單元組件。對于千行左右的組件,使用可計算函數理解的方法,短時間內就能夠驗證組件功能的正確性。
(2)軟件質量屬性計算
軟件工程必須實時估計軟件質量,例如對性能和安全屬性檢查。軟件性能屬性主要表現在算法的時間復雜度和空間復雜度,可計算函數程序理解方法將程序轉換成數學公式形式,容易估算出算法時間和空間的開銷。軟件安全屬性檢查是驗證操作用戶身份、授權,保證程序運行時數據機密性以及不能對其他并行系統造成危害。使用可計算函數理解的方法,短時間內就能夠估算出性能的優劣和安全的級別。
參考文獻
[1]Linger R,Prowell S,Bartholomew R,et al. Function extraction: automated behavior computation for aerospace software verification and certification[C].California:IEEE Computer Society Press, Los Alamitos,2007.
[2]Pleszkoch M,Linger R,Hevner A.Introducing Function Extraction into Software Testing [J].The database for Advances in Information Systems,2008,39(3):41-50.
[3]Pleszkoch M,Linger R. Improving Network System Security with Function Extraction Technology for Automated Calculation of Program Behavior[C].Hawaii USA:IEEE Computer Society Press,Los Alamitos,2004.
[4]Collins R,Hevner A,Walton G, and Linger R.The Impacts of Function Extraction Technology on Program Comprehension:A Controlled Experiment.Information and Software Technology,2008.
[5]Hausler P,Pleszkoch M,Linger R et al.Using Function Abstraction to Understand Program Behavior[J].IEEE Software,1990,7(1):55-63
[6]Pleszkoch M,Hausler P,Hevner A et al.Function-Theoretic Principles of Program Understanding[C].Proceedings of the 23rd Annual Hawaii International Conference on System Science (HICSS35).Hawaii:IEEE Computer Society Press, Los Alamitos,CA,January,1990.
[7]Prowell S,Poore J.Foundations of Sequence-Based Software Specification [J].IEEE Transactions on Software Engineering,2003,29.
[8]Function Extraction Project http://www.cert.org/sse/fxmc.