面向形式化證明的命令生成技術(shù)①

莫廣帥,熊 焰,黃文超

1(中國科學(xué)技術(shù)大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院,合肥 230027)

2(中國科學(xué)技術(shù)大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院,合肥 230027)

近年來,隨著軟件規(guī)模的快速增大,軟件系統(tǒng)安全問題日益增多.因此,開發(fā)者需要在軟件開發(fā)的過程中減少軟件漏洞,保障軟件安全.形式化證明利用數(shù)學(xué)方法對軟件屬性進(jìn)行建模,驗(yàn)證軟件是否滿足相應(yīng)的安全目標(biāo).形式化方法已成為構(gòu)建高可信軟件系統(tǒng)的有效手段.

通常檢測和分析大規(guī)模軟件系統(tǒng)需要使用具有高階邏輯描述能力的工具,如Coq[1]、Isabelle HOL[2,3].在證明工具中,證明人員使用策略與工具交互證明定理.但是,這種證明方式存在一定局限性,需要消耗證明人員大量的時間和精力.因此,實(shí)現(xiàn)定理證明的自動化是必不可少且有意義的工作.

目前,研究者提出了許多自動化證明工作.Paulson等[4]利用現(xiàn)有的ATP 系統(tǒng)證明定理.Gransden 等[5]從已經(jīng)編譯成功的證明庫中匹配當(dāng)前的上下文狀態(tài).Alemi等[6]第一次將深度學(xué)習(xí)算法應(yīng)用于大規(guī)模的定理證明.但是這些工作存在向量信息不足、命令生成不完備等問題.

現(xiàn)有的自動定理證明工作面臨兩個挑戰(zhàn).1)策略空間大.在Coq中,證明人員需要從221 個策略庫中生成合適的策略.2)參數(shù)結(jié)構(gòu)復(fù)雜.策略參數(shù)可以由全局表達(dá)式、復(fù)雜的代碼行和全局中搜索出的中間引理組成.

針對定理證明工具中的命令生成問題,本文提出了以下工作:1)將機(jī)器學(xué)習(xí)與Coq 結(jié)合,利用LSTM等網(wǎng)絡(luò)預(yù)測證明中的策略和參數(shù).2)結(jié)合注意力機(jī)制,自動關(guān)注在訓(xùn)練過程中起決定作用的特征,捕捉重要的信息,減少無用信息的關(guān)注.

1 相關(guān)工作

本節(jié)介紹近年來自動化證明方面的研究工作.現(xiàn)有的自動化證明工作可以分為結(jié)合自動定理證明和結(jié)合交互式證明兩類.

1.1 結(jié)合自動定理證明

隨著自動化定理證明和機(jī)器學(xué)習(xí)的發(fā)展,在不需要手工設(shè)計特征的情況下,Alemi 等[6]首次證明了神經(jīng)網(wǎng)絡(luò)模型有助于進(jìn)行大規(guī)模自動邏輯推理,并第一次將深度學(xué)習(xí)應(yīng)用于大規(guī)模的定理證明.Wang 等[7]提出了一種基于深度學(xué)習(xí)的前提選擇方法.他們將一個高階邏輯公式表示為一個圖,完全保留語法和語義信息.然后為圖的每個節(jié)點(diǎn)指定一個初始嵌入向量,將所有節(jié)點(diǎn)的嵌入集合起來形成整個圖的嵌入.這種方式提高了前提選擇的準(zhǔn)確性.但是,ATP[8]仍然需要將定理轉(zhuǎn)換為合取范式(CNF),復(fù)雜的軟件系統(tǒng)依舊無法證明.

一些工作將現(xiàn)有的交互式定理證明與自動定理證明結(jié)合,允許用戶直接使用現(xiàn)有的ATP 系統(tǒng).Paulson等[4]將Isabelle 證明助手中的定理轉(zhuǎn)換為一階邏輯,之后使用ATP 分析定理,并將證明轉(zhuǎn)換回Isabelle中,從而證明定理.類似的“理論”也被用于其他證明工具(Kaliszyk 等[3];Urban 等[9];Czajka 等[10]).這種證明方式基本上繞過了交互式證明工具,并將工作外包給外部ATP.然而,這種證明方式最大的缺陷在于定理轉(zhuǎn)化過程中可能會導(dǎo)致屬性的缺失.

ATP 將定理的前提和目標(biāo)轉(zhuǎn)換為合取范式(CNF)中的一階子句,并通過證明一階子句來證明定理.ATP的優(yōu)點(diǎn)在于提高了定理證明過程的自動化程度,缺陷在于它很難完成復(fù)雜軟件系統(tǒng)功能正確性的全部驗(yàn)證.針對軟件系統(tǒng)復(fù)雜的數(shù)據(jù)類型和邏輯,ATP 只能處理有限的情況.

1.2 結(jié)合交互式定理證明

在交互式定理證明中,開發(fā)人員利用證明工具手動編寫證明腳本來完成屬性的驗(yàn)證.交互式定理證明的優(yōu)勢在于工具能夠?yàn)檐浖尿?yàn)證產(chǎn)生證明過程,此外,手動編寫腳本使得復(fù)雜軟件的驗(yàn)證成為可能.但是,交互式定理證明存在自動化程度低、驗(yàn)證代價比較高等缺陷.

機(jī)器學(xué)習(xí)算法的發(fā)展為定理自動證明提供了新的思路.一些工作注重與機(jī)器學(xué)習(xí)的交互:Komendantskaya等[11]側(cè)重于ITP和機(jī)器學(xué)習(xí)接口之間的交互式接口方法.但是這項(xiàng)工作并未嘗試生成證明,就其接口而言,重點(diǎn)在于是使許多沒有機(jī)器學(xué)習(xí)經(jīng)驗(yàn)的用戶可以使用許多簡單但有用的選項(xiàng).同樣的還有Hang 等[12]提供了Coq證明的結(jié)構(gòu)化Python 表示,包括證明中遇到的所有證明狀態(tài)、采取的步驟和表達(dá)式抽象語法樹(ASTs),還支持與Coq的輕量級交互,以便它可以用于動態(tài)構(gòu)建證明.但無法構(gòu)建復(fù)雜的策略以便生成證明.

張恒若等[13]在2017年基于 Z3 設(shè)計了 Coq 自動證明的實(shí)現(xiàn).其將Coq 與Z3 約束求解器結(jié)合在一起,設(shè)計了一個編譯框架,將Coq中的定理翻譯為Z3 可判定的明提.最后在Coq中能夠調(diào)用Z3中的命令進(jìn)行證明演算.

但是,張恒若等人工作缺陷在于:

1)Coq 與Z3的類型系統(tǒng)存在巨大差異,無法準(zhǔn)確轉(zhuǎn)換定理表達(dá)式.

2)Coq中的很多基本類型是開發(fā)者直接利用遞歸定義的,但在Z3中有其提供的基本類型.例如,Int (自然數(shù))在Coq中需要開發(fā)者用遞歸的方式手動定義,但在Z3中提供對應(yīng)的Int 類型.如果將Coq中的類型轉(zhuǎn)換為Z3中的類型,其解析證明的效率將會降低.

另一些工作利用機(jī)器學(xué)習(xí)產(chǎn)生證明選項(xiàng)證明定理:Gauthier 等[14]通過從數(shù)據(jù)集中搜索少量候選策略來生成策略集,這些候選策略根據(jù)當(dāng)前需要證明的定理來生成.每個候選策略視為一個可能的行為,并通過學(xué)習(xí)值函數(shù)和蒙特卡羅樹搜索進(jìn)行評估,最后選出需要的策略.雖然比SEPIA 更具適應(yīng)性,但生成的策略仍然是從一個具有預(yù)定的固定集合中選擇的,并且難以將其推廣到數(shù)據(jù)集外的其他策略.

Yang 等[15]通過與證明助手的交互,為定理證明提供了一個大規(guī)模的數(shù)據(jù)集和學(xué)習(xí)環(huán)境.其所使用數(shù)據(jù)集包括來自Coq 證明助手中的123 個開源軟件項(xiàng)目的71K 人工證明(Barras 等).數(shù)據(jù)集涵蓋了廣泛的應(yīng)用領(lǐng)域,包括數(shù)學(xué),計算機(jī)硬件,編程語言等.Yang 等以抽象語法樹的形式生成策略,可以用來證明以前的自動證明器所不能達(dá)到的新定理.

2 方案設(shè)計

本節(jié)將介紹系統(tǒng)的一些設(shè)計細(xì)節(jié).圖1是預(yù)測命令的框架圖.分為4 個模塊:數(shù)據(jù)提取模塊、向量構(gòu)建模塊、預(yù)測參數(shù)模塊和命令結(jié)合模塊.

圖1 預(yù)測命令框架

本節(jié)針對命令預(yù)測問題進(jìn)行抽象.首先,對于命令預(yù)測,本工作從Coq 證明助手中提取證明數(shù)據(jù),包括前提、目標(biāo)和一些結(jié)構(gòu)化信息.之后,這些前提和目標(biāo)以及其他的特征將被編碼成高維向量,經(jīng)過壓縮降維之后,作為神經(jīng)網(wǎng)絡(luò)模型輸入.機(jī)器學(xué)習(xí)模型將會分別預(yù)測策略和參數(shù).最后,本工作結(jié)合預(yù)測和參數(shù)形成證明命令.

2.1 問題模型

本工作將K[γ]定義為γ 預(yù)測概率,其中,γ 表當(dāng)前的狀態(tài)(當(dāng)前前提、目標(biāo)、策略).R代表狀態(tài)空間.

在證明狀態(tài) γ ∈S,γ-predictor K[γ]

被定義為在γ上預(yù)測的概率的函數(shù),其預(yù)測出的策略或者參數(shù):

預(yù)測器P代表針對下一個證明狀態(tài)的預(yù)測.Γ 代表策略的預(yù)測,Λ 代表參數(shù)的預(yù)測:

本工作的機(jī)器學(xué)習(xí)模型將會對當(dāng)前的狀態(tài)做兩種預(yù)測,一種是策略Ptac,一種是參數(shù)Parg.數(shù)學(xué)表示為:

P(σ) 代表模型預(yù)測的命令,將策略Ptac和參數(shù)Parg結(jié)合在一起.

2.2 信息提取

Coq 將證明邏輯信息放在底層,并不在IDE 顯示.此外,由于定理的結(jié)構(gòu)過于復(fù)雜,其證明信息可能無法直接解析使用.本工作中,神經(jīng)網(wǎng)絡(luò)模型直接提取命令行中的信息構(gòu)建證明.

2.3 向量構(gòu)建

Coq 證明助手以類型為基礎(chǔ),如果直接使用證明工具中的數(shù)據(jù)作為編碼,可能導(dǎo)致數(shù)據(jù)冗余、訓(xùn)練效果差等情況.例如,ComCert 項(xiàng)目中的一個定理:

Theorem identity_fn_applied_twice:

Forall (f:bool->bool),(forall (x:bool),fx=x)->

Forall (b:bool),f(f b)=b.

在證明過程中,存在兩個子目標(biāo):

f (f true)=true

f (f false)=false

兩個子目標(biāo)的證明腳本為:

rewrite <- H.

rewrite <- H.

reflexivity.

如果直接編碼子目標(biāo),由于參數(shù)改變,無法有效學(xué)習(xí)第一個子目標(biāo)中的經(jīng)驗(yàn),利用定理中類型替代參數(shù)是一個有效的選擇.因此,本工作所使用的數(shù)據(jù)特征有定理名稱、定理主體和參數(shù)類型.

2.4 預(yù)測策略

為了預(yù)測策略,本工作收集現(xiàn)有的Coq 證明庫和常見的項(xiàng)目組成數(shù)據(jù)集.為反應(yīng)策略預(yù)測的側(cè)重點(diǎn),本工作主要使用以下幾個數(shù)據(jù)特征:

1)當(dāng)前需要證明的目標(biāo);很多策略往往是根據(jù)目標(biāo)具體選擇的.例如,如果定理以forall 開頭,那么下一個策略可能是intro 或induction.

2)上一步的策略;定理證明中策略的使用具有空間局部性.一些策略之后往往使用相同的策略.例如,如果前一個策略是intro,后面經(jīng)常使用auto;而inversion經(jīng)常在subset 后使用.

3)當(dāng)前上下文中的前提.策略的局部參數(shù)存在當(dāng)前的上下文參數(shù)中.因此,當(dāng)前的前提需要作為預(yù)測策略的特征.考慮到下面的前提:

H:is_path(cons (pair s d) m)

這種情況下,機(jī)器學(xué)習(xí)模型可能預(yù)測inversion H或者rewrite->H,H 代表上下文中的假設(shè).

所有的這些特征被編碼成一個高維的向量后,經(jīng)過PCA 降維成一個128 維的向量,然后送入一個每層擁有128 個節(jié)點(diǎn)的完全連接的3 層前饋神經(jīng)網(wǎng)絡(luò)(feed-forward neural network),計算策略的概率分布.圖2是針對策略的預(yù)測模型,目的是找出策略在策略分布圖中的權(quán)重.

圖2 預(yù)測策略框架

用于計算節(jié)點(diǎn)的前饋神經(jīng)網(wǎng)絡(luò)有3 層:輸入層,隱藏層與輸出層.

對于給定的參數(shù)集合W,b,輸出層的輸出h為:

其中,a1,a2,a3與輸入向量有關(guān).前饋神經(jīng)網(wǎng)絡(luò)的計算節(jié)點(diǎn)為GRU,相較于LSTM,GRU的模型計算效率更高.本工作只生成原子策略,而不包括“tac1;tac2”等復(fù)合策略.因?yàn)樗械亩ɡ矶伎梢栽跊]有復(fù)合策略的情況下完成.

2.5 預(yù)測參數(shù)

圖3是預(yù)測參數(shù)的總體框架.將相應(yīng)的特征編碼為向量后,送入到機(jī)器學(xué)習(xí)模型中后,訓(xùn)練得到命令的分布.

圖3 預(yù)測參數(shù)框架

深度學(xué)習(xí)模型預(yù)測3 種參數(shù):1)假設(shè)中參數(shù);2)目標(biāo)中參數(shù);3)中間定理.

預(yù)測參數(shù)模型使用以下幾個特征:1)預(yù)測的策略;2)當(dāng)前子目標(biāo);3)當(dāng)前前提.

與預(yù)測策略相比,預(yù)測參數(shù)模型并沒有使用前一步策略這個特征.基于觀察,當(dāng)前使用的參數(shù)與上一步使用的命令并不存在關(guān)聯(lián).此外,當(dāng)前使用的參數(shù)與當(dāng)前的策略存在一定關(guān)聯(lián)性.

例如,如果是原子性策略,那么策略就不需要模型預(yù)測參數(shù);intro 與rewrite 使用不同的參數(shù).因此,預(yù)測參數(shù)模型使用了當(dāng)前策略這一特征.

與預(yù)測策略相似,將當(dāng)前特征編碼為128 維的向量表示.經(jīng)過PCA 降維之后,送入到神經(jīng)網(wǎng)絡(luò)中訓(xùn)練.最后對當(dāng)前狀態(tài)進(jìn)行預(yù)測,得到當(dāng)前參數(shù)的分布.

2.6 注意力網(wǎng)絡(luò)

為解決自動定理證明中的策略參數(shù)預(yù)測問題,本工作引入注意力機(jī)制,注意力機(jī)制可以自動關(guān)注在訓(xùn)練過程中起決定作用的特征,捕捉重要的信息,減少無用信息的關(guān)注.

注意力機(jī)制包含兩部分結(jié)構(gòu):編碼部分(encoder)和解碼部分(decoder).本工作選取encoder和decoder都為LSTM.這是因?yàn)?相較于RNN,LSTM 采用一個cell state 來保存長期記憶,再配合門機(jī)制對信息進(jìn)行過濾,從而達(dá)到對長期記憶的控制.

在編碼部分,h代表各個時刻的隱藏層狀態(tài).將隱藏層狀態(tài)匯總,生成編碼向量T.q代表對應(yīng)的權(quán)重.

在解碼部分,h1～ht代表編碼器隱藏層狀態(tài),Si-1代表解碼器隱藏層狀態(tài).WaUa代表對應(yīng)神經(jīng)網(wǎng)絡(luò)層的權(quán)重,eij代表h1～ht與Si-1的相關(guān)程度.

其中,αij表示第i個輸出中前一個隱藏層狀態(tài)Si-1與第j個輸入隱層向量hj之間的相關(guān)性.αij可以由eij傳入到對應(yīng)函數(shù)歸一化權(quán)重值得到.

對h1～ht進(jìn)行加權(quán)求和得到此次解碼所對應(yīng)的輸出 (x1,x2,x3,···,xt)的編碼向量Ci.

有了Ci之后,根據(jù)編碼向量Ci進(jìn)行解碼,先計算解碼器i時刻的隱藏層狀態(tài)Si,再計算解碼器i時刻的輸出Yi計算如下:

2.7 結(jié)合策略和參數(shù)

在預(yù)測策略和參數(shù)之后,本工作結(jié)合策略和參數(shù)形成證明命令.

現(xiàn)有的工作使用貪婪搜索結(jié)合策略和命令.在這種結(jié)合方式將選擇概率最高的預(yù)測策略做證明.同樣,機(jī)器學(xué)習(xí)模型選擇概率最高的參數(shù).算法可以通過賦予第一個參數(shù)較高的權(quán)重來實(shí)現(xiàn)這種選擇.但是,這種方法的缺陷在于策略的最終選擇沒有考慮到參數(shù)與策略是否匹配.例如,預(yù)測模型可能會預(yù)測rewrite,但卻發(fā)現(xiàn)沒有合適的前提可以用來作為參數(shù).

本工作并沒有將策略和參數(shù)的概率進(jìn)行標(biāo)準(zhǔn)化等處理,而是直接選出評分較高的策略,依據(jù)策略選擇最高概率的參數(shù).這種方式提供了策略和參數(shù)的平衡,將兩者都考慮在內(nèi).此外,可以根據(jù)策略的類型,來判斷是否使用相應(yīng)的參數(shù),進(jìn)行一些后期的選擇處理.本部分的實(shí)驗(yàn)將會在ComCert 項(xiàng)目上進(jìn)行實(shí)驗(yàn).這部分會在相應(yīng)的實(shí)驗(yàn)章節(jié)展示.

3 實(shí)驗(yàn)分析

本工作利用機(jī)器學(xué)習(xí)與Coq 進(jìn)行信息交互,實(shí)現(xiàn)了在交互式定理證明工具中自動生成證明命令的框架.CompCert是驗(yàn)證C 語言編譯器安全屬性的形式化項(xiàng)目.本小節(jié)預(yù)測CompCert 項(xiàng)目中的命令,測試本系統(tǒng)的生成命令的準(zhǔn)確率.

實(shí)驗(yàn)的環(huán)境配置是Intel Broadwell E5-2660V4 2.0 GHz CPU,128 GB的內(nèi)存,4 根1080Ti的GPU,操作系統(tǒng)是Ubuntu 16.04 LTS.

本工作通過訓(xùn)練來自CompCert的162 個文件的證明數(shù)據(jù)并以其中13 個文件作為測試集.測試集包含501 個證明腳本,一共13 867 個證明命令,如表1.

表1 預(yù)置文件

在所有的證明命令中,本工作能夠預(yù)測28.31%(3926/13 867)的命令,而在proof 證明命令中,本工作能夠預(yù)測41.6% (3 968/9 537)的命令.證明命令包含策略和參數(shù).與其他工作相比,本工作命令準(zhǔn)確率提高2%.結(jié)合注意力機(jī)制,本工作對證明信息的向量構(gòu)建更豐富,機(jī)器學(xué)習(xí)模型更合適.

3.1 策略預(yù)測結(jié)果

在預(yù)測策略時,本工作測試了原始證明中的證明策略在前3 個預(yù)測和前5 個預(yù)測中出現(xiàn)的頻率.如表2.對于測試集證明中的策略,在前3 個預(yù)測中存在正確的策略占58.4%,在前5 個預(yù)測中存在正確的策略占65.6%.此外,從表中可以得知,一些常用的策略如intros,simpl 等預(yù)測的較為準(zhǔn)確,但是一些比較復(fù)雜的策略inversion 預(yù)測效果較差.簡要分析,有兩個方面的原因,一是這些策略使用的目標(biāo)場景復(fù)雜.二是訓(xùn)練集中這些策略較少.

表2 預(yù)測策略

表3為預(yù)測全部策略的次數(shù)的百分比以及正確的概率,表中為真實(shí)策略、策略的預(yù)測次數(shù)占比以及正確的百分比.例如simpl 策略在所有的預(yù)測數(shù)量中占10%,正確的概率為7%.

表3 策略預(yù)測正確率

3.2 參數(shù)預(yù)測結(jié)果

在預(yù)測命令時,本工作預(yù)測了測試集中28.31%的命令.當(dāng)本工作預(yù)測策略正確時,命令中29.5%的參數(shù)是錯誤的.然而,需要注意的是,許多常見的策略沒有任何參數(shù),這些策略在證明的過程中占據(jù)了很大一部分比例.

在交互式定理證明工具中,策略參數(shù)由中間定理、前提和一些復(fù)雜表達(dá)式組成.例如命令destruct(zie (pos0 + typesize ty0) pos),策略參數(shù)為zie (pos0 +typesize ty0) pos.這種復(fù)雜表達(dá)式組成的參數(shù)和當(dāng)前上下文環(huán)境和目標(biāo)定理有關(guān),現(xiàn)有的工作暫時無法生成.此外,這種形式的參數(shù)在手工定理證明中使用的較少,機(jī)器學(xué)習(xí)模型預(yù)測效果較差.復(fù)雜參數(shù)的一個處理方式是將對應(yīng)的參數(shù)加載到當(dāng)前證明的前提中,以上下文參數(shù)的方式處理中間定理,這些工作將會在未來的研究中探討.

4 結(jié)論與展望

本文將機(jī)器學(xué)習(xí)與定理證明工具Coq 結(jié)合,分別預(yù)測策略和參數(shù),提高命令預(yù)測的準(zhǔn)確度.本文首先提取Coq中證明信息,這些信息包括前提、目標(biāo)和一些結(jié)構(gòu)化數(shù)據(jù).然后,將這些前提和目標(biāo)以及其他的特征編碼成高維向量,作為神經(jīng)網(wǎng)絡(luò)模型的輸入.本文預(yù)測了測試集中28.31%的命令,驗(yàn)證了本工作框架的有效性.在未來的研究中,本工作將會根據(jù)預(yù)測的命令形成完整的證明,提高證明的效率.