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

張弛　黃志球　丁澤文　劉林武

摘要：安全關鍵領域中，如何保證軟件安全性已經成為了一個廣受關注的重要課題。確保程序中沒有運行時錯誤，對于軟件安全性的保證十分重要?；诔橄蠼忉尩撵o態分析方法對程序語義進行抽象，是驗證運行時錯誤最合適的形式化方法之一。可配置程序分析（configurable program analysis，CPA）是一種適合多種靜態分析方法的通用分析框架。本文使用CPA對抽象解釋分析方法進行建模，給出了使用基于CPA的抽象解釋方法驗證程序中的運行時錯誤的驗證流程，并用實例說明該驗證方法的有效性。為程序中運行時錯誤的自動化分析和驗證提供了一種可行方案。

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

中圖分類號：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引言

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

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

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

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

2相關理論

21基于格的抽象解釋

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

定義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*，≤*）之間存在轉化函數α：P→P*和逆向轉化函數Y：P*→P，當對x∈P，x*∈P*，α（x）≤*x*x≤γ（x*）則稱轉化函數構成的函數對（α，γ）為集合P和P*之間的伽羅瓦連接，記作：

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

其中，稱（P，≤）為具體域，（P*，≤*）為抽象域，轉化函數α為抽象函數，轉化函數γ為具體函數。

22區間抽象域

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

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

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

{[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的約束，可以用于與分析變量取值范圍相關的程序屬性驗證，例如除零錯或數組越界的驗證。"

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

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

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

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

31CPA形式化體系

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

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

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

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

e′merge（e，e′）。

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

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

32CPA迭代算法

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

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

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

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

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

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

4CPA的分析實例

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

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

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

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

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

（R，≤）αγ（Itvs，）

其中R是實數域，Itvs是實數域上的區間集合。例如程序具體狀態c（pc=s3，{x=0，y=0}）轉化成的抽象狀態是e（pc=s3，{x∈[0，0]，y∈[0，0]}）。

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

（3）合并操作符merge用以表示兩個抽象狀態的合并，在經典區間抽象域的抽象解釋中，表示兩個區間抽象域的合并，即mergejoin（e，e′）=e∪e′。

兩個區間的合并如下：

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

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

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

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

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

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

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

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

5結束語

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

接下來的工作中，我們將進一步擴展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，Feret 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.