基于CPA的抽象解釋分析方法研究

張弛　黃志球　丁澤文　劉林武

摘要：安全關鍵領域中，如何保證軟件安全性已經(jīng)成為了一個廣受關注的重要課題。確保程序中沒有運行時錯誤，對于軟件安全性的保證十分重要。基于抽象解釋的靜態(tài)分析方法對程序語義進行抽象，是驗證運行時錯誤最合適的形式化方法之一?？膳渲贸绦蚍治觯╟onfigurable program analysis，CPA）是一種適合多種靜態(tài)分析方法的通用分析框架。本文使用CPA對抽象解釋分析方法進行建模，給出了使用基于CPA的抽象解釋方法驗證程序中的運行時錯誤的驗證流程，并用實例說明該驗證方法的有效性。為程序中運行時錯誤的自動化分析和驗證提供了一種可行方案。

關鍵詞：可配置程序分析；抽象解釋；靜態(tài)分析；運行時錯誤驗證

中圖分類號：TP311文獻標識碼：A

Abstract：How to ensure software safety has become an important subject in safety critical domain.Ensuring the absence of runtime errors in the program is very important for the safety of the software.The program semantics was abstracted by the static analysis method based on abstract interpretation，and it is one of the most appropriate formal methods for validating runtime errors.Configurable program analysis is a general analytical framework for a variety of static analysis methods.The CPA is used to model the abstraction analysis method，and the validation process of using CPAbased abstract interpretation method to verify the runtime errors in the program is given.Then the effectiveness of the method is illustrated by an example.This provides a feasible solution for the automatic analysis and verification of runtime errors in the program.

Key words：configurable program analysis；abstract interpretation；static analysis；runtime error verification

1引言

近年來，隨著軟件在醫(yī)療、交通、航空航天等安全關鍵領域的廣泛應用，軟件已經(jīng)成為決定系統(tǒng)安全性的主導因素，如何提高軟件質(zhì)量，保證系統(tǒng)安全性，防止災害事故的發(fā)生，已經(jīng)成為當前工業(yè)界和學術界的重要研究課題[1]。程序作為軟件的核心，對于程序中運行時錯誤的驗證是確保軟件安全重要的一環(huán)。運行時錯誤是一類特定的軟件錯誤，是指程序在運行時或運行后發(fā)生的錯誤，并不是軟件需求和設計階段引入的問題，而是在程序編寫時，由于違反程序語言的安全性規(guī)范而引入的問題[2]。例如程序中出現(xiàn)除數(shù)為零的情況、程序中出現(xiàn)數(shù)組下標越界的情況等等。

工業(yè)界常用的仿真、模擬、測試等手段可以發(fā)現(xiàn)大部分運行時錯誤，但卻無法保證軟件中沒有運行時錯誤[3]。形式化分析與驗證方法是保障軟件安全性和可靠性的一種重要方法。學術界目前主要使用形式化的靜態(tài)分析方法來對運行時錯誤進行分析和驗證。形式化的方法如模型檢測[4]需要窮舉所有狀態(tài)空間，存在狀態(tài)空間爆炸的問題；定理證明[5]需要大量人工參與，難以自動化。抽象解釋對程序語義進行抽象，將程序的具體語義轉(zhuǎn)化到抽象域中對程序的性質(zhì)進行分析[6]。其根據(jù)需求對程序語義進行近似，調(diào)節(jié)靜態(tài)分析的精度和效率，是目前對運行時錯誤進行分析和驗證的主要方法。

可配置程序分析是一個形式化的進行軟件驗證和程序分析的通用框架。旨在用一種通用的形式化體系，通過配置不同的參數(shù)，來設計實現(xiàn)多種靜態(tài)分析方法[7]。因此可以使用基于CPA的靜態(tài)分析框架來對抽象解釋的分析階段進行建模。來對運行時錯誤進行分析和驗證。

本文第2節(jié)簡單介紹抽象解釋中的基本概念和用于之后分析的區(qū)間抽象域。第3節(jié)具體介紹CPA靜態(tài)分析框架的形式化體系表示方法及相應的迭代算法。第4節(jié)給出運行時錯誤的具體驗證流程。第5節(jié)用一個實例來解釋說明如何使用該方法，來對程序中的運行時錯誤進行分析和驗證。第6節(jié)，結(jié)束語。

2相關理論

21基于格的抽象解釋

抽象解釋理論是P.Cousot和R.Cousot于1977年提出的對程序語義進行可靠近似理論[8][9]。其基本思想是用抽象語義代替具體語義來描述源程序語言，利用得到的抽象語義來實現(xiàn)具體語義的計算，程序的抽象執(zhí)行的結(jié)果能反映程序真實執(zhí)行的部分信息。抽象解釋本質(zhì)上是一種基于格的程序分析方法，下面給出一些相關的基礎概念。

定義2.1偏序：如果≤是p上的二元關系，如果p中所有元素都具有自反性、傳遞性和反對稱性，則稱≤為p上的偏序關系，稱為一個（p，≤）偏序集。

定義2.2格：對于偏序集（P，≤），若P中任意兩個元素都存在上確界和下確界，則稱（P，≤）是格，為方便，這樣的格稱為偏序格。

定義2.3完備格：對于格（P，≤）如果存在最小元素和最大元素，則稱其為完備格，完備格可以用一個六元組來（P，≤，∪，∩，⊥，T）表示，其中∪表示最小上屆，∩表示最大下界，⊥表示集合P中最小元，T表示集合P中最大元。

定義2.4伽羅瓦（Galois）連接[10]：如果兩個偏序集（P，≤）和（P*，≤*）之間存在轉(zhuǎn)化函數(shù)α：P→P*和逆向轉(zhuǎn)化函數(shù)Y：P*→P，當對x∈P，x*∈P*，α（x）≤*x*x≤γ（x*）則稱轉(zhuǎn)化函數(shù)構成的函數(shù)對（α，γ）為集合P和P*之間的伽羅瓦連接，記作：

（P，≤）αγ（P*，≤*）

其中，稱（P，≤）為具體域，（P*，≤*）為抽象域，轉(zhuǎn)化函數(shù)α為抽象函數(shù)，轉(zhuǎn)化函數(shù)γ為具體函數(shù)。

22區(qū)間抽象域

區(qū)間抽象域在靜態(tài)分析過程中，主要用于表示某程序點處某一變量可能取到的最小值和最大值所構成的區(qū)間來近似[11]。具體域和抽象域之間的關系可以通過下面一個Galois連接來表示：

（R，≤）αγ（Itvs，i）

區(qū)間抽象域可以用一個完備格來表示，即（Itvs，i，∪i，∩i，⊥i，Ti），其中，Itvs是實數(shù)R上的區(qū)間的集合，其形式化的表示為：

{[a，b]|a∈R∪{-∞}，b∈R∪{+∞}，a≤b}∪{⊥i}。

i是Itvs上的偏序關系，形式化定義為：[a，b]i[a′，b′]當且僅當[a，b]=⊥i或者a≥a′^b≤b′，⊥i為集合上的最小元，滿足γ（⊥i）Δ，（-∞，+∞）為集合上的最大元，滿足對I∈Itvs，Ii[-∞，+∞]。通過這樣的方式可以將程序中變量的取值抽象成形如a≤x≤b的約束，可以用于與分析變量取值范圍相關的程序?qū)傩则炞C，例如除零錯或數(shù)組越界的驗證。"

3基于CPA的抽象解釋分析方法

CPA是一個形式化的軟件驗證和程序分析的通用框架，可以通過配置參數(shù)來實現(xiàn)不同靜態(tài)分析方法?；贑PA的抽象解釋靜態(tài)分析方法以程序控制流圖為分析對象，選擇不同抽象精度的抽象域來決定分析過程的抽象層次，選擇不同的merge操作和stop操作來配置不同的迭代分析算法。其配置分析過程如圖1所示。

在CPA配置分析過程中，將程序控制流圖信息結(jié)合抽象域的定義，得到抽象狀態(tài)的遷移關系；根據(jù)抽象域中域操作的定義配置CPA迭代算法中的merge操作和stop操作。根據(jù)抽象狀態(tài)的遷移關系，執(zhí)行CPA迭代算法來求解不動點抽象值，抽象狀態(tài)之間通過merge操作來合并形成新的抽象狀態(tài)，直至stop操作為真，則可判斷沒有新的抽象狀態(tài)產(chǎn)生，迭代結(jié)束。

下面介紹CPA的形式化體系的表示方法和相應的CPA迭代算法。

31CPA形式化體系

CPA形式化定義為ID=（D，∽，merge，stop）， 其中包括抽象域D，抽象狀態(tài)遷移關系∽，合并操作merge，終止判斷操作stop。 CPA通過配置這四部分來完成一次靜態(tài)分析的分析階段，通過選擇不同的配置來實現(xiàn)不同精度和效率的靜態(tài)分析。下面具體說明這四部分

（1）抽象域D=（C，ε，[·]），其中C為程序具體狀態(tài)的集合，其中一個具體狀態(tài)c為程序運行到某一狀態(tài)時變量在不同程序結(jié)點處的實際值，即X∪{Pc}，其中X為變量集合，{Pc}為程序結(jié)點集合。ε是用于描述抽象環(huán)境的完備格ε=（E，，∩，∪，⊥，T），其中E是抽象狀態(tài)集合，E×E是抽象狀態(tài)間的偏序關系，∩表示最大下界，∪表示最小上界，⊥∈E表示集合中的最小元素，T∈E 表示集合中的最大元素。具體化方法[·]：E→2c賦予抽象狀態(tài)其對應的具體狀態(tài)集，即一個抽象狀態(tài)可能對應多個具體狀態(tài)。為了保證分析可靠性（soundness），我們要求[T]=C，[⊥]=；e，e′∈E，[e∪e′][e]∪[e′]。

（2）抽象狀態(tài)遷移∽E×G×E其中E是抽象狀態(tài)集合，G是控制流圖的邊的集合?！妆硎疽粋€抽象狀態(tài)e通過一個CFG的邊g到達一個新的抽象狀態(tài)e′記為e∽e′。為了保證分析過程的可靠性，我們要求e∈E：e′∈E：e∽e′，e∈E，g∈G：Uegete′[e′]UC∈[e]{C′|CgC′}。

（3）合并操作符merge：E×E→E將兩個抽象狀態(tài)的信息進行合并。為了保證分析的可靠性，我們要求

e′merge（e，e′）。

（4）終止判斷操作stop：E×2E→B表示某一個抽象狀態(tài)是否被一個抽象狀態(tài)集合所覆蓋，為了保證分析的可靠性，我們要求

stop（e，R）=true→[e]∪e′∈R[e′]。

32CPA迭代算法

CPA的迭代算法是可達性計算算法。其輸入為一組配置完成的CPAID=（D，∽，merge，stop），以及一個初始抽象狀態(tài)e0∈E，其中E是抽象域D中的抽象狀態(tài)的集合。CPA執(zhí)行算法不斷更新兩個存放抽象狀態(tài)的集合。一個是reached集合，用來存放所有可以到達的抽象狀態(tài)。一個是waitlist集合，用來存放所有還未被執(zhí)行過的抽象狀態(tài)。對于某一狀態(tài)e，根據(jù)抽象狀態(tài)遷移關系∽可以找到其對應的一個或多個后繼結(jié)點，對于任意后繼結(jié)點e′，用其與目前reached集合中所有的抽象狀態(tài)進行merge操作。然后判斷是否有新的結(jié)點產(chǎn)生，即是否沒有被reached集合中所有抽象狀態(tài)所覆蓋。如果產(chǎn)生新的抽象狀態(tài)，則將其加入reached集合和waitlist集合中。重復執(zhí)行算法，直至所有的抽象狀態(tài)進行merge操作后都無法找到新的結(jié)點，即此時找到的程序的不動點。具體的執(zhí)行算法流程詳見表1。

4程序運行時錯誤的驗證方法

圖2給出了一個基于CPA的抽象解釋方法的分析框架，用于對程序的運行時錯誤進行分析和驗證。該過程主要分為三個階段：預處理階段、分析階段和驗證階段。

在預處理階段。由于抽象解釋方法是一個基于狀態(tài)遷移系統(tǒng)的分析方法，因此需要在預處理階段，將待分析系統(tǒng)轉(zhuǎn)化成與之等價的抽象表示，即通過詞法分析和語法分析器得到其抽象語法樹，然后轉(zhuǎn)化成便于進行分析的狀態(tài)遷移系統(tǒng)。之后，我們將狀態(tài)遷移系統(tǒng)轉(zhuǎn)化到程序控制流圖（control-flow graph，CFG）[12]。

分析階段是抽象解釋理論表現(xiàn)的主要階段。在這個階段，CPA靜態(tài)分析框架需要以程序控制流圖、抽象域的域元素、配置的merge操作和配置的stop操作為輸入。其中程序控制流圖由預處理階段生成。其中抽象域中的域元素以完備格的形式提供輸入，在相應的域操作中提取merge操作和stop操作，以完成CPA形式化體系的輸入。相應的CPA迭代算法運用抽象解釋中的迭代策略，計算程序控制流圖中所有結(jié)點的不動點抽象值，從而完成分析。

在驗證階段，將得到的程序結(jié)點上的不動點抽象值轉(zhuǎn)化為程序具體的變量約束關系，根據(jù)系統(tǒng)的需求文檔和設計說明文檔對程序的變量數(shù)值性質(zhì)進行分析，判斷變量的數(shù)值性質(zhì)是否滿足規(guī)約，得到分析結(jié)果，從而完成整個抽象解釋靜態(tài)分析的過程。圖3以除零錯為例，說明如何對運行時錯誤進行驗證。根據(jù)分析階段得到的不動點抽象值，結(jié)合源程序中與除數(shù)變量相關的代碼，得到變量的約束關系，然后判斷在各個程序結(jié)點，是否存在除數(shù)為零的情況，完成分析驗證。

4CPA的分析實例

本章用一個實例來說明如何使用可配置程序分析CPA來對基于抽象解釋的靜態(tài)分析的分析階段進行建模。以圖4中代碼為例，使用區(qū)間抽象域進行分析，以期得到各個程序結(jié)點處變量的取值范圍。

根據(jù)第四章分析框架，首先在預處理階段，根據(jù)相關詞法分析和語法分析，將源程序轉(zhuǎn)化到其控制流圖，轉(zhuǎn)化結(jié)果如圖5所示。

在分析階段，根據(jù)程序控制流圖和抽象域的定義，配置CPAID=（D，∽，merge，stop），即分別配置抽象域D，抽象狀態(tài)遷移關系∽，抽象狀態(tài)的合并操作merge，終止判斷操作stop。下面給出具體過程：

（1）配置抽象域D=（C，ε，[·]）為區(qū)間抽象域。其中C為程序具體狀態(tài)的集合C{pc，x}，其中pc∈{s1，s2，…，s11}，X={x，y}；描述抽象環(huán)境的完備格

ε=（E，，∩，∪，⊥，T），其中E是抽象狀態(tài)集合，具體狀態(tài)和抽象狀態(tài)通過一個Galois連接彼此關聯(lián)

（R，≤）αγ（Itvs，）

其中R是實數(shù)域，Itvs是實數(shù)域上的區(qū)間集合。例如程序具體狀態(tài)c（pc=s3，{x=0，y=0}）轉(zhuǎn)化成的抽象狀態(tài)是e（pc=s3，{x∈[0，0]，y∈[0，0]}）。

（2）抽象狀態(tài)遷移關系∽，一個抽象狀態(tài)通過圖2程序控制流圖上連通的一邊到達一個新的狀態(tài)。例如抽象狀態(tài)e（pc=c，i∈[1，1]）通過邊（pc=c，i=i+1，pc′=d）到達抽象狀態(tài)e′（pc=d，i∈[2，2]）；抽象狀態(tài)e（pc=c，i∈[1，11]通過邊（pc=b，assume（i<=10），pc′=c）到達抽象狀態(tài)e′（pc=c，i∈[1，10]）。以此類推來遍歷尋找所有可能達到的抽象狀態(tài)。

（3）合并操作符merge用以表示兩個抽象狀態(tài)的合并，在經(jīng)典區(qū)間抽象域的抽象解釋中，表示兩個區(qū)間抽象域的合并，即mergejoin（e，e′）=e∪e′。

兩個區(qū)間的合并如下：

例如抽象狀態(tài)e（pc=s3，{x∈[0，0]，y∈[0，0]}）與抽象狀態(tài)

e′（pc=s3，{x∈[1，1]，y∈[1，1]}）進行merge操作形成新的新的抽象狀態(tài)

e″（pc=s3，{x∈[0，1]，y∈[0，1]}）。

（4）終止判斷操作stop用以判斷某一個抽象狀態(tài)是否被一個抽象狀態(tài)集合所覆蓋，在區(qū)間抽象域的抽象解釋中表示是否產(chǎn)生了之前所達到的抽象狀態(tài)集合沒有覆蓋到的抽象狀態(tài)，即程序是否到達了不動點，如果經(jīng)過所有的遷移關系，都沒有新抽象狀態(tài)的產(chǎn)生，則整個抽象解釋的分析就到達不動點。其配置為

stopjoin（e，R）=e∪e′∈Re′。

在完成配置CPA之后，執(zhí)行CPA迭代算法。算法輸入ID=（D，∽，merge，stop），初始狀態(tài)

e0=（pc=s1，{x=⊥，y=⊥}），經(jīng)過表1的CPA的迭代算法之后，各個程序結(jié)點處的不動點抽象值如表2所示：

根據(jù)算法結(jié)果，得到變量x和變量y在全部程序結(jié)點處的取值范圍，可以對一些變量數(shù)值相關的運行時錯誤進行分析和驗證。證明了該分析方法的有效性和可行性。

5結(jié)束語

針對程序中的運行時錯誤，本文提出了一種基于CPA的抽象解釋的分析方法。首先介紹了一種支持抽象解釋的靜態(tài)分析框架，即可配置程序分析；然后給出了具體的靜態(tài)分析流程，如何從源程序出發(fā)，轉(zhuǎn)化成與之等價的控制流圖，再轉(zhuǎn)化到CPA形式化體系中進行迭代計算，最后根據(jù)得到的不動點抽象值進行相關運行時錯誤的分析驗證；最后給出一個實例的分析過程，說明該靜態(tài)分析方法的可行性和有效性。

接下來的工作中，我們將進一步擴展CPA支持的抽象域，如八邊形抽象域、多面體抽象域，甚至一些非凸抽象域。并給出一個自動化的對運行時錯誤進行分析和驗證的工具，來對研究工作進行完善。

參考文獻

[1]黃志球，徐丙鳳，闞雙龍，等.嵌入式機載軟件安全性分析標準、方法及工具研究綜述[J].軟件學報，2014，25（2）：200-218.

[2]DELMAS D，SOUYRIS J.Astrée：from research to industry[C]//International Static Analysis Symposium.Springer Berlin Heidelberg，2007：437-451.

[3]計算機科學技術百科全書 ：選編本[M].北京：清華大學出版社，2002.

[4]CLARK E M，GRUMBERG O，PELED D.Model checking[M].MIT press，1999.

[5]L Hai，S Jigui，Z Yimin.Theorem Proving Based on the Extension Rule.[J].Journal of Automated Reasoning，2003，31（1）：11-21.

[6]COUSOT P，COUSOT R.Basic concepts of abstract interpretation[M]//Building the Information Society.Springer US，2004：359-366.

[7]BEYER D，HENZINGER T A，Théoduloz G.Configurable Software Verification：Concretizing the Convergence of Model Checking and Program Analysis[C]// International Conference on Computer Aided Verification.2007：504-518.

[8]COUSOT P，COUSOT R.Abstract Interpretation：A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.[C]// ACM SigactSigplan Symposium on Principles of Programming Languages.1977：238-252.

[9]COUSOT P，COUSOT R，F(xiàn)eret J，et al.The ASTRE Analyzer[J].Lecture Notes in Computer Science，2005，3444：140-140.

[10]COUSOT P，COUSOT R.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[C]// Programming Language Implementation and Logic Programming，International Symposium，Plilp92，Leuven，Belgium，August 26-28，1992，Proceedings.1992：269-295.

[11]COUSOT P，COUSOT R.Static determination of dynamic properties of programs[J].Proceedings of the Second International Symposium on Programming，1976.

[12]HARROLD M J，MALLOY B，ROTHERMEL G.Efficient Construction of Program Dependence Graphs[J].Acm Sigsoft Software Engineering Notes，2000，18（3）：160-170.