原文來自微信公衆号“程式設計語言Lab”：SIG-程式分析技術沙龍回顧｜數值程式分析

# 研究背景 #

很多軟體的代碼裡面都包含了大量的數值運算，如科學計算、金融、機器學習、實體模拟、統計分析等領域的軟體。在嵌入式控制軟體中，往往也會包含大量數值運算，而嵌入式控制軟體在很多安全攸關的領域被大量使用，比如說在航天航空領域 GNC、姿軌控等相關的一些功能實作中都會用到數值運算。

這些軟體數值運算中，用到的數值不像我們傳統了解數學意義下的數，如實數和整數，而都是浮點數和機器整數。此外，在嵌入式軟體設計中，往往會在事先設計時，把存儲區域做一些劃分，用來存一些資料，編寫程式來操作這些存儲區域時，會使用一些指針指向這些區域，然後使用指針算術通路資料。是以，這些軟體中除了傳統的數值運算，還涉及到一些指針算術的運算，當然我們可以把指針算術也看作是整數運算。

# 數值運算舉例 - 求平均數

舉一個簡單的求兩個數平均數的例子，可能大家第一印象會按照數學的模式去寫，先做加法，然後再除以二，這樣很容易就求得了兩個數的平均數。這種在數學上大家肯定覺得沒什麼問題，但是如果在機器裡面寫成程式實作，這時候先做加法的話，x+y 很容易會出現浮點的上溢。而對于這種情況，如果把求平均數表達式稍微變一變，把參數先除以二，然後再做加法，你就會發現基本上就不會導緻浮點上溢。

# 數值相關常見錯誤

正是因為這種數學上的運算，跟我們在機器裡面的浮點數和整數的運算存在差異，有很多實數上的性質，對于浮點運算并不成立。那麼，大家寫程式的時候，可能很容易會導緻一些數值相關的錯誤。有很多很常見的程式錯誤與此相關，比如說除零錯、數組越界，浮點上溢、整數上溢等，還比如指針算術導緻的非法指針通路。另外，程式中有大量的數值運算的話，還可能會導緻一些計算精度的缺陷。

• 除零錯、數組越界、浮點上溢、整數上溢等
• 指針算術導緻的非法指針通路等
• 函數輸入不在定義域内
• 計算精度缺陷

曆史上出現的一些重大事件，比如像愛國者飛彈防禦系統攔截失敗，阿麗亞娜 5 号火箭爆炸，openSSL 心髒滴血等，本質上都是跟數值相關的。有些是因為數值的溢出，有些是因為一些誤差的累計，有些是因為缺少邊界的檢查，等等。

# 數值程式分析的思路

那麼，我們應該如何檢測這種錯誤呢？即通過 數值程式分析 來檢測。

當程式寫好了之後，我們可以通過程式分析的方法來檢測這些錯誤。檢測數值相關的錯誤的時候，最基礎的一步是首先要生成不變式，有了不變式之後，我們再來分析這個程式裡面的一些性質，檢查一些性質是不是成立的，檢測數值相關的缺陷，缺陷檢測出來之後，我們還可以考慮缺陷修複。我們可以沿着這條途徑來檢測和修複數值相關的缺陷。

# 不變式生成

不變式生成 是數值程式分析中最基礎的關鍵技術之一。不變式生成實際上是一個非常經典的課題，關注如何在每一個程式點處自動生成變量之間的不變式。我們關注的是 數值不變式，如下圖紅色标注的注釋，就是不變式。有了不變式後，我們就可以去分析這個程式會不會出現一些數值相關的缺陷。

打個比方，對于上圖這個非常簡單的就一個變量和一個循環的程式。假設我們現在關注程式點 3 處的加法操作，若

x

是整型變量，加

1

會不會出現整數上溢呢？

這個問題實際上是跟

x

的類型有關，如果

x

是

char

類型，也就是

8

位類型的話，我們知道前面的不變式是

[0,255]

，如果再加上

1

，可能就會出現整數的上溢；當然如果

x

是

16

位的或者是

32

位的整型，那麼這個加法操作就不會出現整數上溢問題。

是以，我們需要先拿到不變式，之後就可以檢查程式語句是否滿足數值的一些性質，或者說是否存在數值相關的一些缺陷。這是數值程式分析裡面一個非常關鍵的技術。

業界有很多的方法來生成不變式，簡單分為以下幾類，比如最傳統的 基于抽象解釋 的，也可以用 基于限制求解 的方法來生成，最近幾年也有用 機器學習 的方法來生成不變式，當然還有一些用動态的方法來生成一些 likely 不變式。

• 基于抽象解釋
• 基于限制求解
• 基于學習
• 基于動态方法

今天這個報告，我主要介紹 基于抽象解釋的不變式的生成，以及它在數值程式分析中的應用。

# 抽象解釋 #

接下來，我先介紹一下抽象解釋相關的理論。

# 抽象 & 近似

抽象解釋是 1977 年提出來的 1，它最開始是用來對程式的語義進行 抽象（或近似） 的一種統一的架構。

這裡的定義涉及到兩個關鍵詞，一個叫 抽象，一個叫 近似。我們應該怎麼了解這兩個詞呢？接下來我會通過直覺的例子來解釋，希望能幫助大家了解。

首先，是對于 “近似” 的了解。比如說當我們用一個刻度尺去量一個物體的長度的時候，其實我們不能量出這個物體的精确的長度，但是我們人眼可以看到它大概是 3.4cm 左右，那麼這個值實際上是一種近似。

接着，我們來看對 “抽象” (Abstraction) 的了解。比如說我們現在碰到這樣一個問題，兩個大數加起來之後再乘以一個大數的話，那麼這個結果到底是正的還是負的呢？我們會首先想到先計算加法的結果，實際上這是一個比較大的值，然後再做乘法。如果用筆紙去算的話，那麼需要費些時間才能把最終的值給算出來，并最後發現它是個正數。整個過程的計算代價還是比較大的。其實我們可以發現：如果兩個數都是正數，那麼兩個正數相加的話，依然是個正數，然後再乘以另外一個正數，那麼它的結果肯定也是個正數。這是一些簡單的運算規則，但是根據這些規則計算的話，計算代價是非常低的。将每個數抽象為正負表示，這其實就是一種抽象的思想。通過抽象，我們把一些跟關注的問題本身無關的東西忽略掉。比如我們隻關心這個結果是正的還是負的，而對它本身具體是什麼值，我們并不關心，是以這個時候我們就可以把這個具體的值忽略掉，而隻關心它的正負性，進而可以快速判定結果的正負。這就是抽象思想的展現。

抽象解釋，為靜态分析的設計提供了一個通用的架構，還可以用來自動生成程式的不變式。簡單來講，具體世界的狀态比較多，它的取值的可能性也比較多，而中間的一些計算也比較繁瑣或者代價比較大。那麼我們就希望能通過一種抽象的方法，把它轉到到一個抽象的空間裡面來，使得在這個抽象的空間裡面它的狀态比較少，計算的代價也比較小，這樣的話我們就能快速分析得到這個程式的一些性質。

# 伽羅瓦（Galois）連接配接

抽象解釋裡面最核心的一個概念叫做 伽羅瓦（Galois）連接配接：

( C , ≤ ) ⇌ α γ ( A , ⊑ ) (C, \leq) \xrightleftharpoons[\alpha]{\gamma} (A, \sqsubseteq) (C,≤)γ

α​(A,⊑)

定義如下：

對于給定的兩個偏序集 ( C , ≤ ) (C, \leq) (C,≤) 和 ( A , ⊑ ) (A, \sqsubseteq) (A,⊑)（ C C C 是 Concrete， A A A 是 Abstract），如果存在函數對 α : C → A \alpha:C \rightarrow A α:C→A 和 γ : A → C \gamma:A \rightarrow C γ:A→C 滿足如下性質的話，那麼我們認為這個函數對 ( α , γ ) (\alpha, \gamma) (α,γ) 是具體域 C C C 和抽象域 A A A 之間的 伽羅瓦連接配接。

∀ a ∈ A , c ∈ C : α ( c ) ⊑ a ⇔ c ≤ γ ( a ) \forall a \in A, c \in C : \alpha(c) \sqsubseteq a \Leftrightarrow c \leq \gamma(a) ∀a∈A,c∈C:α(c)⊑a⇔c≤γ(a)

該性質可以如此了解，假設把具體世界裡的一個元素 c c c 抽象化之後得到 α ( c ) \alpha(c) α(c)。 α ( c ) \alpha(c) α(c) 比抽象域裡另一進制素 a a a 要小，當且僅當将抽象元素 a a a 映射回具體世界裡面得到 γ ( a ) \gamma(a) γ(a) 時， c c c 應比 γ ( a ) \gamma(a) γ(a) 要小。這裡所說的 “小”，對應的是一個序關系。

滿足了這個性質後， α \alpha α 和 γ \gamma γ 就構成一個伽羅瓦連接配接。我們把 α \alpha α 叫作從具體世界到抽象世界的抽象化函數，把 γ \gamma γ 叫作從抽象世界到具體世界的具體化函數。我們把左邊這個叫做具體域，右邊叫做抽象域。

區間抽象域的 Galois 連接配接

舉個栗子

接下來，我們通過一個簡單且經典的抽象域 —— 區間抽象域，來給大家介紹抽象域的相關概念。

假設我們的具體域是一個整數集合 Z Z Z 上的幂集 P ( Z ) \mathcal{P}(\mathbb{Z}) P(Z)，那麼它對應的序關系就是集合包含關系。

( P ( Z ) , ⊆ ) ⇌ α γ ( I , ⊑ ) (\mathcal{P}(\mathbb{Z}), \subseteq) \xrightleftharpoons[\alpha]{\gamma} (I, \sqsubseteq) (P(Z),⊆)γ

α​(I,⊑)

我們會把這個幂集映射到區間抽象域上面的一個區間集合，這個抽象域的序關系是區間上的包含關系。即，如果區間較小的話，那麼它的下界要大一點，上界要小一點。同時，我們對區間做了一些擴充，比如它的下界可以取到負無窮大，上界可以取到正無窮大。

I =  def  ( Z ∪ { − ∞ } ) × ( Z ∪ { + ∞ } ) I \stackrel{\text { def }}{=}(\mathbb{Z} \cup\{-\infty\}) \times(\mathbb{Z} \cup\{+\infty\}) I= def (Z∪{−∞})×(Z∪{+∞})

接下來我們來看 α \alpha α 和 γ \gamma γ 怎麼定義。對于具體域上的一個元素，這個元素肯定是這個幂集裡面的一個元素，即整數集合 Z \mathcal{Z} Z 的一個子集，我們把這個整數子集記作 X X X，那麼 α ( X ) \alpha(X) α(X) 會把它映射成一個區間，取這個集合 X X X 裡面最小的整數值作為區間的下界，最大的整數值作為區間的上界，這就是抽象化函數 α \alpha α 的定義。

α ( X ) =  def  [ min ⁡ X , max ⁡ X ] \alpha(X) \stackrel{\text { def }}{=}[\min X, \max X] α(X)= def [minX,maxX]

同樣的反過來，如果給定一個抽象元素，比如說一個區間 [ a , b ] [a,b] [a,b]，我們怎麼把它映射回具體域的元素（即一個集合）呢？ 這個整數集合會包含所有大于等于 a a a 且小于等于 b b b 的整數。

γ ( [ a , b ] ) =  def  { x ∈ Z ∣ a ≤ x ≤ b } \gamma([a, b]) \stackrel{\text { def }}{=}\{x \in \mathbb{Z} \mid a \leq x \leq b\} γ([a,b])= def {x∈Z∣a≤x≤b}

給一個整數的集合 { 0 , 1 , 2 , 5 } \{0,1,2,5\} {0,1,2,5}，我們将其映射到區間抽象域，把它抽象化之後，按照定義，我們會得到區間 [ 0 , 5 ] [0,5] [0,5]。 [ 0 , 5 ] [0,5] [0,5] 這個區間實際上是整數集合 { 0 , 1 , 2 , 5 } \{0,1,2,5\} {0,1,2,5} 一個可靠的 上近似，并且是一個最佳的抽象，也就是說你找不到另外一個比 [ 0 , 5 ] [0,5] [0,5] 要小的，同時還包含 { 0 , 1 , 2 , 5 } \{0,1,2,5\} {0,1,2,5} 這個集合的區間。

a ( 0 , 1 , 2 , 5 ) = [ 0 , 5 ] [0,5]是0,1,2,5的可靠且最佳抽象 a({0,1,2,5})=[0,5] \qquad \text{[0,5]是{0,1,2,5}的可靠且最佳抽象} a(0,1,2,5)=[0,5][0,5]是0,1,2,5的可靠且最佳抽象

反過來，如果把抽象元素 [ 0 , 5 ] [0,5] [0,5] 映射到具體世界裡面，我們需要定義一個 γ \gamma γ 函數。我們知道具體世界裡對應的是一個整數集合，把 [ 0 , 5 ] [0,5] [0,5] 映射回來的話，隻要在 [ a , b ] [a,b] [a,b] 中的整數都需要在這個集合中，那麼結果就是 { 0 , 1 , 2 , 3 , 4 , 5 } \{0,1,2,3,4,5\} {0,1,2,3,4,5}。我們再與原來最開始的具體元素 { 0 , 1 , 2 , 5 } \{0,1,2,5\} {0,1,2,5} 進行比較，你會發現先做抽象，然後再映射回具體世界裡，包含的元素會更多，比如說 { 3 , 4 } \{3,4\} {3,4} 包含進去了。

γ ( [ 0 , 5 ] ) = { 0 , 1 , 2 , 3 , 4 , 5 } 把0,1,2,5抽象成[0,5]存在精度損失 \gamma([0, 5]) = \{0,1,2,3,4,5\} \qquad \text{把{0,1,2,5}抽象成[0,5]存在精度損失} γ([0,5])={0,1,2,3,4,5}把0,1,2,5抽象成[0,5]存在精度損失

對應到這個程式分析場景，可以了解成這是一種精度的損失。為什麼會存在這種情況呢？ 因為在具體世界裡面，我們知道 { 3 , 4 } \{3,4\} {3,4} 不在程式狀态 { 0 , 1 , 2 , 5 } \{0,1,2,5\} {0,1,2,5} 裡，但是做了抽象之後雖然能确定 { 6 } \{6\} {6} 不在程式狀态中，但是不能排除 { 3 , 4 } \{3,4\} {3,4} 在程式狀态中。

這個對應到程式分析裡面對應的就是精度的損失。

# 抽象域設計

整個抽象解釋架構，實際上自 1977 年提出來以後發展至今已經比較成熟了，在碰到特定應用場景時，我們需要在這個架構下設計一些新的抽象域。設計新的抽象域時主要考慮兩個方面:

• 域元素：對 程式狀态 進行抽象

  表示方法: 限制形式等，e.g.，區間: a < = x < = b a<=x<=b a<=x<=b

• 域操作：對程式 語義動作 進行抽象
  • 交 (assume 語句)
  • 控制流接合 (if-then-else-endif)
  • 投影（非确定指派，過程間分析）
  • 遷移函數
    • 指派遷移語句 (指派語句)
    • 測試遷移語句 (if 語句)
  • 加寬（循環）

一是我們要考慮應如何表示域裡的元素。我們需要用域元素來對程式的狀态進行描述。最經典的就是用一類限制來表示，比如剛才介紹的區間，我們用的就是變量的上下界的這種形式來對這個程式的狀态進行描述。當然也有複雜點的描述方式，比如多面體抽象域用的是線性不等式限制。

另一方面，除了域元素的表示，我們還需要考慮如何處理程式中的語義動作，比如說指派語句、if 語句等等。對于這些語句，我們需要在抽象域裡面有對應的一個操作來對它進行處理。比如說，設計抽象域的時候，我們需要設計 meet 操作、join 操作。join 指集合或者控制流彙合。簡單來講，就是在 if-then-else-endif 這個地方，我們兩個分支彙合處（即 endif 處）需要一個 join 操作來把程式狀态合并起來。程式裡面有指派語句，是以我們對指派語句需要設計一個抽象遷移函數。對于條件測試語句的話也是類似的。而對于程式裡的循環，我們需要設計加寬的操作來保證程式分析過程中不動點疊代計算可終止。

# 數值抽象域

數值抽象域是一類非常重要的抽象域，它的主要用途是來刻畫程式變量之間的數值關系，即 數值不變式。有了這個數值不變式，我們就可以來檢查數值相關的一些性質或者缺陷。目前已存在 40 種以上的抽象域。經典的抽象域可以簡答劃分成兩類：

• 非關系型的抽象域：例如符号域。就像我們一開始介紹 “抽象” 這一概念的時候，我們隻關心這個變量到底是正的還是負的。除此之外，還有剛才講到的區間的抽象域，還有同餘域
• 關系型抽象域：包括線性等式域、線性不等式抽象域（多面體域）、八邊形域等。八邊形域描述限制表示時，系數隻能是 + 1,-1 或者是 0，且一條限制隻能刻畫兩個變量之間的一個關系。

在我們使用抽象域來進行程式分析時，一般會采用 over-approximation（上近似），也就是說要把程式狀态都包在裡面，以防有所遺漏。我們來直覺解釋下，比如對于下面這個圖，每一個藍色的小十字叉代表了這個程式的一個具體狀态，那用我們剛才列舉的這些抽象域去包住程式狀态時，在幾何上就需要把這些藍色的十字叉給包進來。如果我們用多面體抽象域，那麼對應的二維形狀就是一個多邊形。我們用圖中這個深綠色的多邊形就可以把所有十字叉都包進來。假設圖中外側的紅色的地方表示這個程式會出錯，比如說會出現數組越界、除零、整數上溢等之類的錯誤。我們會發現這個程式的所有的狀态都被這個多邊形包住了，而且這個多邊形跟這個紅色的區域并沒有相交，那也就是說，我們用多面體抽象域證明了在這個程式點處這個程式是不會出錯的。

接下來，我們換成區間抽象域，區間抽象域對應地在平面上就是個矩形。這個時候，我們會發現綠色矩形和紅色區域有交集。那麼，程式分析時，我們拿到區間分析的結果就會報警，說這個程式狀态在這個程式點處可能會有錯誤。然而，實際上我們會發現在這個相交的區域裡面，并沒有包括真正的具體程式狀态，也就說藍色的十字叉并沒有出現在紅綠相交區域裡。換而言之，用區間分析得到的這個報警，是一個誤報，是虛假報警，而實際上程式是不會出錯的。是以，用（上近似）抽象解釋做程式分析時，沒有漏報，但是可能會存在誤報。

已有數值抽象域，大部分采用限制的 conjunction（合取） 作為限制表示，都隻能表達幾何上凸的形态，存在凸性局限性（會導緻誤報），不能表達析取性質。但是程式中會有很多的析取的行為。比如，if 本身其實就是一個 disjunction，是以我們用已有的數值抽象域去分析程式的時候，會有很多因為凸性的局限性導緻出現一些誤報。

針對凸性局限性，我們設計并實作了一些 非凸 的數值抽象域，來提高抽象域對析取的表達能力。所謂非凸，如下圖右側所示，在把一個個表示具體狀态的十字叉包住時，我們會發現非凸抽象域的區域比左側用的多面體會小很多，至少我們可以知道原點沒有出現在程式狀态裡。然後，我們用這個非凸抽象域去分析程式的時候，因為域元素包含的面積或體積更小了，分析就更加精确，誤報更少。

這方面工作的主要技術思想是，我們把原來采用的傳統線性不等式，變拓展成了帶區間系數的線性不等式，或者把原來隻關注 x x x， y y y 這些變量間關系拓展為關注 x x x、 ∣ x ∣ |x| ∣x∣、 y y y、 ∣ y ∣ |y| ∣y∣ 之間的關系，即我們利用這種絕對值函數來描述一些非凸的程式行為。

舉個栗子

舉個簡單的例子來講，傳統八邊形抽象域域元素采用的限制形式是 ± x ± y ≤ c \pm x \pm y \leq c ±x±y≤c，即它隻能描述兩個變量 x x x 和 y y y 之間的這種受限形式關系，其中變量系數隻能是 + 1 +1 +1， − 1 -1 −1 或者 0 0 0。那麼，我們可以對它簡單做一些擴充，比如考慮允許其中一個變量帶絕對值的情形，還可以進一步考慮允許兩個變量都帶絕對值的情形。按照這種方式擴充之後，就隻會存在下面所列的這幾種可能的限制表示：

• 八邊形限制： ± x ± y ≤ a \pm x \pm y \le a ±x±y≤a
• 僅含一個變量的絕對值： − ∣ x ∣ ± y ≤ b , ± x − ∣ y ∣ ≤ c -|x|\pm y \le b,\pm x - |y| \le c −∣x∣±y≤b,±x−∣y∣≤c
• 含兩變量的絕對值： − ∣ x ∣ − ∣ y ∣ ≤ d -|x|-|y|\le d −∣x∣−∣y∣≤d

按照這種思路，用擴充之後的限制形式去描述程式的行為，或者作為抽象域的一個域表示，就可以刻畫一些非凸的性質了，而傳統的八邊形域能刻畫的僅是凸的性質。

幾何形态：非凸

簡單而言，在幾何上，“凸” 意味着如果對于上圖中一個圖形綠色區域内的兩個點，其連線上的點也都在這個區域裡面，那麼這個圖形就是一個凸的，這是凸在幾何上的性質。我們可以利用絕對值函數描述一個非凸的區域，比如 − ∣ x ∣ ≤ 1 -|x|\le 1 −∣x∣≤1，即 ∣ x ∣ ≥ 1 |x| \ge 1 ∣x∣≥1，所描述的程式狀态集合，在幾何上就是非凸的。直覺上，抽象域元素對應的程式狀态的面積越小，那麼分析精度就會更高。

# 我們的工作

前面，我們通過一個簡單例子來給大家介紹在設計數值抽象域時，如何面向我們需要解決的問題來設計一些新型的或者是适合這個問題的抽象域。其中，關鍵點是找一種合适的限制表示。

在選擇了特定形式限制之後，接下來要考慮的就是，在這個限制形式上，如何設計比較高效的算法來操縱這種限制。比如說怎麼實作 join，怎麼實作 meet 等等。

我們課題組沿着這個思路，設計實作了一些抽象域，并融到了開源的數值抽象域庫 Apron 的主分支裡面。Apron 庫應該是最早的且開源的數值抽象域庫，裡面包含了很多經典、常見數值抽象域的實作。我們在設計一些基于抽象解釋的程式分析的時候，就可以在 Apron 數值抽象域庫中，選擇并調用對應的抽象域的接口，來實作自己的分析。

Apron：https://github.com/antoinemine/apron

我們團隊的工作融合到開源抽象域庫 Apron 主分支

# 數值程式分析 #

# 數值程式分析工具 Numpa

接下來給大家介紹一下，在抽象域設計好後，怎麼實作一些程式分析。

我們課題組實作了一個數值程式分析工具 Numpa。下圖是 Numpa 的架構示意，這同時也是一個典型的抽象解釋工具的架構。很多抽象解釋工具基本上也是采用這種架構。

數值程式分析工具 Numpa 架構

步驟說明

如下所示，對于給定的一個某種語言編寫的 待分析程式（目前我們的這個工具支援 C 程式）：

• 先通過編譯前端将它的表示 轉化為一個中間表示，這個中間表示其實本質上是一個 圖的描述，刻畫的是一個遷移系統，同時也對應到了待分析程式的語義方程。
• 接下來是一個抽象解釋裡面的 不動點疊代求解器，它會不斷 調用抽象域庫（也就是 Apron）裡面的抽象域的一些操作，比如遇到指派語句，就調用抽象域裡面指派語句對應的指派遷移函數，控制流彙合（control-flow join）語句，就調用抽象域裡對應的 join 操作。
• 當分析過程疊代穩定之後，即達到不動點之後，工具就會輸出數值不變式。

當然，為了處理指針，我們也設計了一個 指向抽象域，以得到每個指針變量的指向資訊，包括其基位址資訊，以及關于基位址的偏移量的資訊。利用這些分析資訊，我們可以檢查程式缺陷并報警。

工具支援

我們的工具是面向 C 程式的，支援常見的資料類型和文法結構，如整型、浮點型及之間的類型轉換，數組（一維/二維數組、指針數組）、靜态指針及指針算術，結構體及結構體數組等。當然，也有一些我們目前暫不支援，如函數指針。

同時，我們還考慮了一些特定領域軟體的特點，如嵌入式軟體中常見的中斷分析。

從工具的輸出角度，Numpa 支援輸出：

• 數值不變式，即數值變量間的限制關系，以及變量的取值範圍
• 指針變量的指向資訊：包括可能指向的基位址集合，以及相對于基位址的偏移量
• 報警類型：基于不變式資訊，Numpa 可以檢查一些常見的運作時錯誤，如未初始化、算術溢出、除零錯、數組越界、空指針解引用、死代碼、數學函數輸入不在定義域内（如負數開平方根）等

舉個栗子

如下代碼示例，我們會在進入循環後的程式點 4 處，得出指針變量

p

的基位址是數組

A

的名字，其基位址的偏移量與

x

是兩倍的關系，并分析得到

x

的值範圍是

[0, 99]

。

int A[198];
1 x := 0;
2 p := A;
3 while (x <= 99) do
4   *p := 0; // 數組越界！！！
5   x := x + 1;
6   p := p + 2;
         7
done;
           

這是我們得到的不變式：

p ∈ A , 0 ≤ x ≤ 99 , offset_p = 2 x \begin{aligned} &p \in A, \\ &0 \le x \le 99, \text{offset\_p} = 2x \end{aligned} ​p∈A,0≤x≤99,offset_p=2x​

在這個程式示例的點 4 處，Numpa 可分析得出

x

的值範圍為

[0, 99]

，指針變量

p

關于其基位址（數組

A

）的偏移量是

x

的兩倍，即能取到

198

。按照程式的語義，數組通路下标範圍在

[0,197]

間才不會出錯，而分析得出可能會通路到

198

的下标位置。是以，程式分析工具會報警，認為在程式點 4 處的指派語句可能導緻數組越界。

工具現狀

目前，我們一直在維護這個數值程式分析工具，也在航天等領域中的一些實際程式上開展了實驗。當然，工具本身還有很大的提升空間。

目前，這個工具面臨的主要問題是：

• 誤報相對較多。
• 且，如果我們用非關系型的抽象域，比如用區間，我們分析的規模能夠滿足要求，但是精度就會比較差，誤報也會比較多；但是，當我們用關系型抽象域的時候，一旦變量過多，尤其采用精度較高的過程間分析方法時，工具的可擴充性就會比較差，因為關系型抽象域的可擴充性跟變量的次元緊密相關。
• 另外，當我們使用這個工具來分析一些實際的開源軟體時，會遇到一些比較複雜的資料結構。比如，對于一些指針形态相關的操作，會增加了記憶體模型的複雜性，在分析過程中不易處理。

# 結合抽象域與 SMT 的程式分析

為了彌補 抽象解釋分析精度不足 的問題，我們一個簡單的想法是 利用 SMT 公式來提高分析精度，結合抽象域和 SMT 來開展分析。

抽象域 vs SMT

我們知道，SMT 公式的表達能力比較強，尤其是它能表達析取，當然它的計算代價也比較高。另外一個問題是，用 SMT 來分析程式的時候，如何處理循環？當然，一個簡單政策時是循環展開，但是我們不知道循環應該展開多少次才能覆寫全程式行為。目前，在 SMT 上面沒有特别合适的加寬算子，使得在抽象解釋架構下在 SMT 公式表示的程式狀态上開展不動點疊代，難以保證不動點疊代的終止性。

抽象域	可滿足性模理論（SMT）
表達能力（精度）	受限，尤其析取表達能力不足	SMT 公式表達能力強（析取，量詞等）
計算代價	低	高
疊代收斂性（處理循環）	加寬/變窄算子	尚無合适的加寬/變窄算子

具體方法

為了将 SMT 和抽象域結合起來開展程式分析，我們借鑒了軟體模型檢驗中 程式分塊編碼技術，開展塊級程式分析 2。

• 首先，我們對程式進行了分塊。即，每個程式塊作為一個單獨的遷移函數；
• 在程式塊内采用 SMT 來刻畫公式（塊内精度比較高）；在程式塊間或者遇到循環的時候，将 SMT 公式轉化為抽象域表示（循環體會被看做一個程式塊，采用 SMT 編碼；在循環頭處會将 SMT 轉化為抽象域表示。進而，在循環頭處，我們可以利用抽象域上的加寬操作，來保證不動點疊代的終止性）。

通過上述這種方法，我們可以提高程式分析的精度，但其中用到了一個關鍵技術：SMT-opt。我們将 SMT 公式轉化為抽象域表示時，SMT 公式裡面是帶析取的，但是抽象域表示中是沒有析取的，是以我們需要 符号化抽象技術，将 SMT 公式轉換為抽象域表示。

我們可以用類似線性規劃的 SMT 規劃技術（或者叫 SMT 最優化技術），将一個 SMT 公式轉化為一個帶模闆的抽象域的表示。

如下圖示，我們目前用的是 SMT 求解器 Z3 中的 vZ 子產品，它可以支援 SMT 規劃。但這個方法的計算代價還是挺大的，會影響到程式分析效率。

這一方面最新的研究進展，是姚培森博士等人發表在 OOPSLA 2021 上的工作 3，提出了一種更高效的符号化抽象技術。

# 數值程式分析應用 #

基于數值程式分析技術，除了利用數值程式分析技術來檢查運作時錯誤，我們還可以做一些應用分析。

# 軟體資源使用情況分析

關注的問題

比如分析 程式中資源使用量的上界。程式在運作過程中，會使用到很多類型的軟體資源（堆記憶體、檔案句柄、網絡套接字、使用者自定義資源等）。

資源消耗量上界分析的結果，有助于在資源受限的條件下（如在嵌入式系統中），幫助指導軟體的設計、部署、配置；同時，我們也可以利用資源消耗量上界分析技術來檢測，未受控資源消耗缺陷等資源使用相關缺陷。實際上，有不少 CWE 跟資源使用相關：

– CWE-400: Uncontrolled Resource Consumption

– CWE-769: File Descriptor Exhaustion

– CWE-774: Allocation of File Descriptors or Handles Without Limits or Throttling

– CWE-775: Missing Release of File Descriptor or Handle after Effective Lifetime

技術途徑

我們分析資源消耗量上界的主要思路是 4，把資源使用量上界分析問題轉化成數值程式分析問題，如下圖所示：

簡單來講，對于給定的待分析程式，

STEP 1：首先，對源程式進行 插樁轉換，通過引入一些輔助整型變量來模組化資源的消耗情況；

STEP 2：接下來，因為我們關注的其實就是新引入的這些輔助變量的值範圍，而程式中有很多代碼跟資源使用無關，是以我們可以拿着這些變量去 對程式切片；

STEP 3：最後，基于抽象解釋技術來分析 被提取出來的數值程式，可以得到一些描述資源使用量的輔助變量間的數值關系，進而獲得資源使用量上界的估計。

# 神經網絡架構中的數值缺陷檢測

關注的問題

現在也有不少工作用抽象解釋來做神經網絡的驗證，我下面介紹的這個工作其實不是來做神經網絡模型層面驗證的，而是依然屬于程式層面的。

我們用深度學習架構（如 Tensorflow）寫的程式中會包含大量數值運算，其中可能存在數值缺陷，進而需要相應的檢測技術。

神經網絡訓練或推斷過程中可能會産生數值計算缺陷（“NaN”, “INF”）

技術途徑

下面介紹的是我和北大的熊英飛老師、謝濤老師和他們的團隊，還有港科大的張成志老師一起合作的一項工作：張量抽象 & 數值抽象 5。

用 Tensorflow 寫的程式，會要拿很多的資料來進行訓練，而在訓練的過程中也執行很多數值運算，其中也會調用很多數值函數。那麼，數值運算過程中可能會出現一些如 “NAN” 或 “INF” 值，這些值往後傳播可能導緻程式缺陷。

我們這項工作大體的思路還是用 抽象解釋 來做分析。因為這類程式裡面有很多數值運算，是以我們可以做 數值抽象，進而獲得程式中變量的值範圍。但，因為這類程式裡面涉及很多的張量（張量可以簡單了解為傳統程式裡面的數組，或者說高維的數組），我們就需要對這些數組或者張量做一些特殊分析和處理。

我們用的方法是 基于張量劃分的張量抽象技術。數值抽象用的是比較簡單的抽象域，我們用了區間域和線性等式域，這兩個數值抽象域都是經典的抽象域，相對來說也是比較輕量級的數值抽象域，進而得到變量值的範圍：

• 張量抽象（張量劃分）
• 數值抽象（結合區間抽象與線性等式抽象）

我們的方法将張量抽象和數值抽象結合起來，比如，可以得到張量劃分後的每一部分的取值範圍。

# 總結 #

今天，一方面給大家介紹了用抽象解釋怎麼來生成數值不變式。因為抽象解釋架構本身比較成熟了，其中最重要的就是設計比較适合目标問題的數值抽象域。我們用抽象域來進行程式分析的時候，可能會碰到一些問題，比如說誤報比較多。那麼怎麼來提高分析的精度呢？結合例子，我給大家簡單介紹了下我們結合 SMT 和抽象域來提高分析精度的思路。

另一方面，基于數值程式分析，我們可以開展一些應用分析。除了缺陷檢測，我們可以基于數值程式分析來分析程式資源的使用量上界（類似于 WCET 分析）。此外，除了傳統的程式（如 C 程式），深度學習相關程式代碼也包含大量的數值運算，也可能出現一些數值缺陷，那麼怎麼用抽象解釋來檢測這一類程式的缺陷呢？除了數值不變式，這類程式還涉及到一些新的結構，如張量，這就需要一些新的抽象技術。

• 基于抽象解釋的數值不變式生成
  • 數值抽象域的設計
• 數值程式分析
  • 結合數值抽象域與SMT的塊級程式分析
  • 軟體中資源使用量上界分析
  • 神經網絡架構中的數值缺陷檢測

相關論文推薦

數值程式分析：

• Tengbin Wang, Liqian Chen, Taoqing Chen, Guangsheng Fan, Ji Wang. Making Rigorous Linear Programming Practical for Program Analysis. In CP 2021.
• Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang. Hierarchical Analysis of Loops With Relaxed Abstract Transformers. IEEE Transactions on Reliability. 2020.

數值程式驗證：

• Pengfei Yang, Jianlin Li, Jiangchao Liu, Cheng-Chao Huang, Renjue Li, Liqian Chen, Xiaowei Huang, Lijun Zhang. Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation. Formal Aspects of Computing, 2021.
• Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang, Patrick Cousot. Verifying Numerical Programs via Iterative Abstract Testing. In SAS 2019.
• Jiangchao Liu, Liqian Chen and Xavier Rival. Automatic Verification of Embedded System Code Manipulating Dynamic Structures Stored in Contiguous Regions. IEEE TCAD, 2018.

參考

1. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press, New York, NY. ↩︎
2. Jiahong Jiang, Liqian Chen, Xueguang Wu and Ji Wang.Block-wise abstract interpretation by combining abstract domains with SMT. In VMCAI 2017. ↩︎
3. Program Analysis via Efficient Symbolic Abstraction. Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang. The 36th ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages, and Applications, OOPSLA 2021. ↩︎
4. Guangsheng Fan, Taoqing Chen, Banghu Yin, Liqian Chen, Tengbin Wang, Ji Wang. Static Bound Analysis of Dynamically Allocated Resources for C Programs. In ISSRE 2021. ↩︎
5. Yuhao Zhang, Luyao Ren, Liqian Chen, Yingfei Xiong, Shing-Chi Cheung, Tao Xie. Detecting Numerical Bugs in Neural Network Architectures. In FSE 2020. (ACM SIGSOFT Distinguished Paper Award). ↩︎