神經(jīng)網(wǎng)絡(luò)化簡非多項式混合布爾算術(shù)表達式

劉彬彬，鳳維杰，鄭啟龍，2，李 京

1(中國科學(xué)技術(shù)大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，合肥 230026) 2(中國科學(xué)技術(shù)大學(xué) 安徽省高性能計算重點實驗室，合肥 230026)

1 引 言

混合布爾算術(shù)(Mixed Boolean-Arithmetic，MBA)表達式[1，2]是指混合使用位運算符(如&，|，～等)和算術(shù)運算符(如+，-，*等)的表達式，如表達式3*(x&y)-y+2.相關(guān)文獻[1，3]給出了混合布爾算術(shù)表達式的形式化定義，并將其分類為多項式和非多項式混合布爾算術(shù)表達式.另外，文獻[1，3]提出多種方法來產(chǎn)生大量的混合布爾算術(shù)恒等式，如x=(x＾y)+y-2*(～x&y).混合布爾算術(shù)表達式主要被用于軟件混淆領(lǐng)域中，其是一種先進的軟件混淆技術(shù)[4，5].混合布爾算術(shù)混淆技術(shù)可以將一個簡單的表達式替換為一個復(fù)雜的但語義等價的表達式，如將x替換為(x＾y)+y-2*(～x&y).因此，混合布爾算術(shù)混淆技術(shù)已經(jīng)被多個學(xué)術(shù)界和工業(yè)界項目所采用[4，6，7-9].

混合布爾算術(shù)表達式的大范圍應(yīng)用促使研究人員探索如何反混淆混合布爾算術(shù)表達式，也就是化簡混合布爾算術(shù)表達式.相關(guān)實驗結(jié)果表明，目前已有的計算數(shù)學(xué)軟件都不能處理混合布爾算術(shù)表達式[10，11].故研究人員提出了多種不同的化簡方法，包括：語義等價變換方法[4，11]，bit-blasting[12]，模式匹配[13]，程序合成技術(shù)[14]，和基于深度學(xué)習(xí)的解決方案[15，16].雖然這些方法都能夠化簡特定形式的混合布爾算術(shù)表達式，但是相關(guān)實驗結(jié)果表明[3，11]，這些方法都不能有效處理非多項式混合布爾算術(shù)表達式.并且，文獻[3]提出使用安全性更高的非多項式混合布爾算術(shù)表達式替代已有的多項式混合布爾算術(shù)表達式.因此，化簡非多項式混合布爾算術(shù)表達式是一個極具挑戰(zhàn)的任務(wù).

為了化簡非多項式混合布爾算術(shù)表達式，本文提出一種字符串到字符串的解決方案NeuSim，該解決方案基于神經(jīng)網(wǎng)絡(luò)模型來自動化學(xué)習(xí)和化解表達式.首先，在序列到序列和圖序列神經(jīng)網(wǎng)絡(luò)架構(gòu)的基礎(chǔ)上，本文構(gòu)造并實現(xiàn)了NeuSim.其次，針對相關(guān)數(shù)據(jù)集匱乏的問題，本文收集并生成一個大規(guī)模的數(shù)據(jù)集，該數(shù)據(jù)集包含1000000條多種形式的非多項式混合布爾算術(shù)表達式.最后，本文在生成的數(shù)據(jù)集上訓(xùn)練NeuSim，并在測試集上進行測試.相關(guān)實驗結(jié)果表明，與已有工具的化簡結(jié)果相比，NeuSim的化簡正確率是已有解決方案的8倍，并且化簡時間可以忽略不計(低于0.01秒).

本文的主要貢獻總結(jié)如下：

1)本文提出一種端到端的解決方案NeuSim來化簡非多項式混合布爾算術(shù)表達式，并且構(gòu)建了相應(yīng)的序列到序列和圖序列神經(jīng)網(wǎng)絡(luò)模型.本文是首個應(yīng)用神經(jīng)網(wǎng)絡(luò)化簡非多項式混合布爾算術(shù)表達式的研究.

2)本文構(gòu)建了業(yè)界第一個大規(guī)模的非多項式多混合布爾算術(shù)表達式數(shù)據(jù)集，其包括各種形式的非多項式混合布爾算術(shù)表達式及其等價的簡單表達式.

3)大規(guī)模的實驗結(jié)果表明，相較于已有的化簡方法，NeuSim的化簡正確率至少提高7倍，并且化簡時間至少快1個數(shù)量級.此外，與本研究相關(guān)的資源(代碼，數(shù)據(jù)集，和神經(jīng)網(wǎng)絡(luò)模型)可在如下網(wǎng)址公開獲?。篽ttps：//github.com/nhpcc502/NeuSim.

本文接下來的組織如下：第2部分介紹混合布爾算術(shù)表達式的相關(guān)背景知識；第3部分介紹本文提出的字符串到字符串的解決方案NeuSim；第4部分介紹相關(guān)實驗結(jié)果及其分析；第5部分是本文總結(jié).

2 相關(guān)工作

2.1 混合布爾算術(shù)表達式

文獻[1，2]提出了混合布爾算術(shù)表達式的概念，其是指混合使用位運算符(如&，|，～等)和算術(shù)運算符(如+，-，*等)的表達式，定義1給出了多項式混合布爾算術(shù)表達式的形式化定義.如果一個混合布爾算術(shù)表達式不符合定義1，那么它將屬于非多項式混合布爾算術(shù)表達式[1，3]，這說明多項式和非多項式混合布爾算術(shù)表達式之間是補集的關(guān)系.

定義1.一個多項式混合布爾算術(shù)表達式如公式(1)所示，其中ai為整數(shù)常量，ei，j(x1，…，xt)為n-bit變量x1，…，xt的位運算表達式.

∑i∈Iai(∏j∈Jiei，j(x1，…，xt))

(1)

文獻[1]設(shè)計了一種基于真值表的矩陣乘法方法，并用其來產(chǎn)生大量的多項式混合布爾算術(shù)恒等式.在已有的混合布爾算術(shù)恒等式的基礎(chǔ)上，文獻[3]提出多種形式化的方法來產(chǎn)生眾多的多項式和非多項式混合布爾算術(shù)恒等式.混合布爾算術(shù)恒等式主要被用于軟件混淆(software obfuscation)領(lǐng)域[4，5]，是一種先進的軟件混淆技術(shù).混合布爾算術(shù)混淆技術(shù)可以將一個簡單的表達式等價替換為一個復(fù)雜的等價表達式，并用其來復(fù)雜化程序代碼.

由于混合布爾算術(shù)混淆技術(shù)的理論正確性和使用成本低廉，該技術(shù)已被多個學(xué)術(shù)界和工業(yè)界項目所采納[4，6-9]，其也可被用于算法優(yōu)化中[17].另一方面，研究人員開始探索如何反混淆混合布爾算術(shù)表達式，也就是理解復(fù)雜的混合布爾算術(shù)表達式并還原出一種語義等價的簡單形式.由相關(guān)文獻可知[10，11]，常用的SMT求解器和符號計算軟件都不能化簡混合布爾算術(shù)表達式.因此，研究人員提出多種不同的解決方案來處理混合布爾算術(shù)表達式，包括：基于語義等價變換的技術(shù)[4，11]，bit-blasting[12]，模式匹配[13]，程序合成技術(shù)[14]，和基于深度學(xué)習(xí)的方法[15，16].這些化簡方法都可以處理特定類型的混合布爾算術(shù)表達式，其中基于語義等價變換的方法是最有效的，它們能夠高效處理多項式混合布爾算術(shù)表達式.但是，在面對非多項式混合布爾算術(shù)表達式時，已有的方法都表現(xiàn)出了明顯的不足[3，11].并且，文獻[3]提出使用安全性更高的非多項式混合布爾算術(shù)表達式等價替換已有的多項式混合布爾算術(shù)表達式.

2.2 神經(jīng)網(wǎng)絡(luò)處理數(shù)學(xué)表達式

文獻[15]探索了如何使用神經(jīng)網(wǎng)絡(luò)化簡多項式混合布爾算術(shù)表達式，其提供了一個大規(guī)模的線性混合布爾算術(shù)表達式(多項式混合布爾算術(shù)表達式的特例)數(shù)據(jù)集，并且用該數(shù)據(jù)集訓(xùn)練相關(guān)的序列到序列神經(jīng)網(wǎng)絡(luò)模型，實驗結(jié)果表明其在線性混合布爾算術(shù)表達式上取得了較好的效果.文獻[16]注意到已有的基于序列到序列模型在解決數(shù)學(xué)表達式時存在的潛在不足，進而提出使用圖序列神經(jīng)網(wǎng)絡(luò)來處理數(shù)學(xué)表達式.相關(guān)實驗表明，圖序列神經(jīng)網(wǎng)絡(luò)相較于序列到序列模型，在處理有關(guān)數(shù)學(xué)表達式任務(wù)時具有更高的正確率.

此外，已有多個研究工作使用神經(jīng)網(wǎng)絡(luò)模型來處理數(shù)學(xué)問題.相關(guān)文獻[18，19]使用序列到序列的模型來處理數(shù)學(xué)表達式，如表達式重寫和數(shù)學(xué)表達式問答；文獻[20]使用樹神經(jīng)網(wǎng)絡(luò)來進行邏輯推理.然而，對于本文所研究的非多項式混合布爾算術(shù)表達式化簡問題，目前業(yè)界尚無相關(guān)工作.

3 化簡非多項式混合布爾算術(shù)表達式

化簡非多項式混合布爾算術(shù)表達式的目標是給出一個簡單的等價表達式，本節(jié)將詳細介紹一種字符串到字符串的解決方案NeuSim，該方案使用神經(jīng)網(wǎng)絡(luò)來學(xué)習(xí)和化簡非多項式混合布爾算術(shù)表達式.為了橫向?qū)Ρ饶壳皹I(yè)界最為經(jīng)典的各類數(shù)學(xué)表達式計算模型，本文構(gòu)建并實現(xiàn)了兩類神經(jīng)網(wǎng)絡(luò)模型：序列到序列架構(gòu)的模型和圖序列機構(gòu)的模型.由于目前業(yè)界缺乏非多項式混合布爾算術(shù)表達式數(shù)據(jù)集，本文在相關(guān)文獻的基礎(chǔ)上，生成了一個大規(guī)模的非多項式混合布爾算術(shù)表達式數(shù)據(jù)集.

3.1 神經(jīng)網(wǎng)絡(luò)模型結(jié)構(gòu)

本文基于編碼器-解碼器架構(gòu)[21]來實現(xiàn)NeuSim，其結(jié)構(gòu)主要分為兩部分：負責(zé)從輸入表達式中學(xué)習(xí)隱藏模式的編碼器，以及根據(jù)學(xué)到的知識預(yù)測表達式化簡結(jié)果的解碼器，模型結(jié)構(gòu)如圖1所示.NeuSim的輸入是一個以序列形式呈現(xiàn)的、長度可動態(tài)變化的非多項式混合布爾算術(shù)表達式.編碼器通過學(xué)習(xí)輸入數(shù)據(jù)的特征，并輸出一個固定長度的隱藏狀態(tài)向量來表示學(xué)習(xí)到的表達式特征.解碼器是由循環(huán)神經(jīng)網(wǎng)絡(luò)組成，通過預(yù)先設(shè)定的字典，NeuSim可以將解碼器的輸出重構(gòu)成一個簡單的表達式，也就是對應(yīng)的非多項式混合布爾算術(shù)表達式的化簡結(jié)果.

圖1 NeuSim模型結(jié)構(gòu)示意圖Fig.1 Architecture of NeuSim

為了全面比較不同的神經(jīng)網(wǎng)絡(luò)模型之間的性能差異，本文采用兩類不同的神經(jīng)網(wǎng)絡(luò)架構(gòu)來構(gòu)建NeuSim的編碼器：序列到序列的模型和圖序列的模型.其中，構(gòu)建基于長短期記憶網(wǎng)絡(luò)LSTM[22]，門控循環(huán)單元GRU[23]，和注意力機制[24]的序列到序列的模型；同時，構(gòu)建基于圖卷積架構(gòu)[25]的圖序列網(wǎng)絡(luò)模型.在序列到序列的模型中，NeuSim直接將輸入的長度可變的非多項式混合布爾算術(shù)表達式輸出給編碼器.在圖序列模型中，NeuSim首先需要對輸入的非多項式混合布爾算術(shù)表達式進行預(yù)處理(將輸入的表達式轉(zhuǎn)換成有向無環(huán)圖(DAG圖))，然后將DAG圖輸出給圖卷積編碼器.

3.1.1 序列到序列神經(jīng)網(wǎng)絡(luò)模型

混合布爾算術(shù)表達式多以字符串的形式進行保存和處理，故本文首先研究如何構(gòu)造一個基于序列到序列架構(gòu)的NeuSim.在序列到序列的模型中，編碼器和解碼器都由循環(huán)神經(jīng)網(wǎng)絡(luò)組成，其輸入輸出也是由字符組成的、長度可變的字符串.為了對比各種不同的序列到序列神經(jīng)網(wǎng)絡(luò)模型對NeuSim性能的影響，本研究采用3種廣泛使用的循環(huán)神經(jīng)網(wǎng)絡(luò)(長短期記憶網(wǎng)絡(luò)LSTM[22]，門控循環(huán)單元GRU[23]，和注意力機制BERT[24])作為NeuSim編碼器和解碼器的核心構(gòu)件，接下來將詳細介紹這3種神經(jīng)網(wǎng)絡(luò)模型的結(jié)構(gòu).

本文構(gòu)建的第1個模型是基于長短期記憶網(wǎng)絡(luò)LSTM[22]的NeuSim.LSTM是自然語言處理領(lǐng)域最為經(jīng)典的神經(jīng)網(wǎng)絡(luò)模型之一，它可以較好地解決長輸入中相同字符相隔較遠導(dǎo)致模型無法捕獲長期依賴的問題.首先，在模型的編碼器中構(gòu)造一個嵌入層作為輸入的非多項式混合布爾算術(shù)表達式接收器，該嵌入層通過獨熱編碼的方式將輸入的表達式向量化.在嵌入層之后，編碼器構(gòu)造了激活函數(shù)為tanh的4層LSTM層.通過時間依賴的迭代學(xué)習(xí)，編碼器可以從輸入的表達式中學(xué)習(xí)到相應(yīng)地隱藏模式，并將這些隱式信息抽象化為一個固定大小的隱藏向量.在解碼器中，其首先構(gòu)造一個嵌入層，該嵌入層以隱藏向量作為輸入，并將其輸出給一個由4層LSTM組成的神經(jīng)網(wǎng)絡(luò).最后，解碼器的輸出向量通過一個全連接層重新編碼成一個新的表達式，該表達式即為對應(yīng)輸入表達式的化簡結(jié)果.為了避免模型訓(xùn)練時的過擬合，本模型采用隨機丟棄策略dropout，該策略可以隨機丟棄神經(jīng)網(wǎng)絡(luò)中的神經(jīng)元，從而避免模型產(chǎn)生過擬合的現(xiàn)象.

本文構(gòu)建的第二個模型是基于門控循環(huán)單元GRU[23]的NeuSim.GRU作為循環(huán)神經(jīng)網(wǎng)絡(luò)的一種變體，它的結(jié)構(gòu)更加緊湊、可學(xué)習(xí)參數(shù)量更少.具體來看，該模型的編碼器首先構(gòu)造一個嵌入層以獨熱編碼方式向量化輸入的非多項式混合布爾算術(shù)表達式，并用dropout策略隨機丟棄該層的神經(jīng)元以控制模型的擬合程度.嵌入層之后連接一個單層的GRU，其被用以學(xué)習(xí)輸入表達式中各個字符之間的隱藏關(guān)系(如相同字符間的時序關(guān)系)，并將這種隱藏關(guān)系抽象為隱藏向量.隨后，該模型將隱藏向量輸出給解碼器.解碼器按序分別由嵌入層、單層GRU以及全連接層構(gòu)建，全連接層依據(jù)字符字典將輸出的向量轉(zhuǎn)換成相應(yīng)的字符串，即輸入表達式的化簡結(jié)果.

本文構(gòu)建的第3個模型是基于注意力機制[24]的NeuSim.注意力機制是目前自然語言處理領(lǐng)域最為有效的方法，其是一種放棄循環(huán)結(jié)構(gòu)、全部采用線性層的模型策略，且能夠?qū)Ρ磉_式序列中有價值的部分賦予更高的注意力(即權(quán)重)，進而使模型學(xué)習(xí)到更有價值的信息.本文復(fù)現(xiàn)了目前業(yè)界最先進的基于注意力機制模型之一的BERT機制，并將其作為編碼器的一部分.在編碼器中，模型首先使用一個嵌入層將輸入的非多項式混合布爾算術(shù)表達式以獨熱編碼方式轉(zhuǎn)換成向量；然后構(gòu)建一個由8頭注意力層和一個位置前饋層組成的基本單元，該基本單元內(nèi)的各個組件之間通過正則化層進行連接；隨后，將該基本單元前后連接若干次(本文使用5個基本單元).編碼器的輸出為一個隱藏向量，并將其輸出給解碼器.解碼器由5個解碼器基本單元組成，每個基本單元由掩碼8頭注意力層、8頭注意力層以及位置前饋層組成，基本單元之間通過正則化層進行連接.最后，解碼器的輸出向量依據(jù)字符字典，通過全連接層轉(zhuǎn)換成一個表達式，也即輸入表達式的化簡結(jié)果.

3.1.2 圖序列神經(jīng)網(wǎng)絡(luò)模型

在序列到序列的模型中，以字符串形式呈現(xiàn)的混合布爾算術(shù)表達式不利于神經(jīng)網(wǎng)絡(luò)學(xué)習(xí)表達式中某些隱藏信息，例如在字符串序列表示中，算符的優(yōu)先級需要通過添加額外的括號來明確化(如表達式x+(3*y)).為了克服序列到序列神經(jīng)網(wǎng)絡(luò)模型在處理數(shù)學(xué)表達式方面的潛在不足，目前已有研究工作應(yīng)用圖序列神經(jīng)網(wǎng)絡(luò)模型處理數(shù)學(xué)表達式.圖序列神經(jīng)網(wǎng)絡(luò)模型通常用于輸入是圖輸出為文本的任務(wù)中，例如視頻標簽生成、圖像分類、蛋白質(zhì)分子分類和化合物生成等任務(wù).為了應(yīng)用圖序列神經(jīng)網(wǎng)絡(luò)模型處理數(shù)學(xué)表達式，首先需要將輸入的表達式轉(zhuǎn)換成圖，如抽象語法樹(AST樹)和有向無環(huán)圖(DAG圖)，該圖在保留表達式相關(guān)語法語義信息的同時，可以丟棄無用的輔助信息(如括號).之后，模型對轉(zhuǎn)換后的圖進行處理，并且輸出相應(yīng)的結(jié)果表達式.

本文構(gòu)建的最后一個模型是基于圖序列神經(jīng)網(wǎng)絡(luò)[25]的NeuSim.首先，NeuSim需要對輸入的非多項式混合布爾算術(shù)表達式進行預(yù)處理.預(yù)處理階段通過遍歷輸入的表達式以生成對應(yīng)的有向無環(huán)圖(DAG圖).基于該DAG圖生成相應(yīng)的特征矩陣和鄰接矩陣，拼接這兩類矩陣后將其送入到模型的編碼器中.編碼器由5層圖卷積神經(jīng)網(wǎng)絡(luò)構(gòu)成，后接一個全局最大池化層，且每層都使用relu作為其激活函數(shù).編碼器的輸出為一個隱藏向量，該隱藏向量將輸入給解碼器.解碼器由嵌入層、GRU以及全連接層構(gòu)成，通過序列化學(xué)習(xí)生成一個輸出向量，并通過字符字典得到輸出向量對應(yīng)的表達式，也即輸入表達式的預(yù)測解.

綜上所述，本文構(gòu)建并實現(xiàn)了兩類共4種不同的神經(jīng)網(wǎng)絡(luò)模型，相應(yīng)的模型層數(shù)和參數(shù)大小如表1所示.

表1 神經(jīng)網(wǎng)絡(luò)模型層數(shù)和大小Table 1 Model layers and size of NeuSim

3.2 數(shù)據(jù)集

為了得到更好的化簡效果，NeuSim需要大規(guī)模的數(shù)據(jù)來進行訓(xùn)練.然而，相關(guān)文獻[3，6，17]只提供了少量非多項式混合布爾算術(shù)表達式(約1000個表達式)示例，這對于訓(xùn)練和測試NeuSim是明顯不足的.為此，本文根據(jù)相關(guān)文獻[3，6]中提出的方法來生成非多項式混合布爾算術(shù)表達式.這些方法的輸入為一個簡單的表達式，輸出為一個復(fù)雜的等價非多項式混合布爾算術(shù)表達式.

通過進一步觀察發(fā)現(xiàn)，文獻[3，6]生成的非多項式混合布爾算術(shù)表達式具有一定的規(guī)律性和一致性[4]，這些特性造成在訓(xùn)練Neusim時的過擬合現(xiàn)象.因此，為了增加非多項式混合布爾算術(shù)表達式的多樣性和隨機性，本文提出如下的表達式等價變換方法(用于替換的等價表達式均由文獻[1]所提出的相應(yīng)方法隨機產(chǎn)生)：

1)變量替換.該方法對(子)表達式中的變量進行等價變換，以期得到一個新的等價表達式，如將(x&y)變換為(((x|y)+(x&y)-y)&y).

2)常量替換.該方法將(子)表達式中的常量替換為一個等價的表達式，如將常量1替換為(x&y)-(x|y)-(～x&～y).

3)子表達式替換.該方法將表達式中的子表達式進行等價替換，如將((x|y)+(x&y))替換為x+y.

4)線性組合.該方法通過對多個表達式的線性組合，來產(chǎn)生一個新的等價表達式，如將表達式x+y+z=((((x|y)+(x&y))|z))+(((x＾y)+2*(x&y))&z)和表達式z=(z|y)-(～z&y)，線性組合為一個新的表達式x+y=((((x|y)+(x&y))|z))+(((x＾y)+2*(x&y))&z)-(z|y)+(～z&y).

綜上所述，本文首先通過文獻[3，6]產(chǎn)生一個原始的非多項式混合布爾算術(shù)表達式，之后使用等價變換方法對生成的原表達式進行隨機處理.從理論上說本研究可以產(chǎn)生無窮多個非多項式混合布爾算術(shù)表達式，但是從訓(xùn)練和測試NeuSim的實際出發(fā)，本文構(gòu)建一個包含1000000條非多項式混合布爾算術(shù)恒等式的數(shù)據(jù)集.文獻[10]指出，在實際的軟件混淆場景下使用的都是3變量及其以下變量的混合布爾算術(shù)表達式.因此，數(shù)據(jù)集中包含800000個3變量及其以下變量的的非多項式混合布爾算術(shù)表達式，200000個多變量非多項式混合布爾算術(shù)表達式.

數(shù)據(jù)集中的每一條數(shù)據(jù)都是一個二元組(Eg，Ec)，Eg表示一個簡單的表達式，Ec表示相應(yīng)等價的非多項式混合布爾算術(shù)表達式，相關(guān)表達式示例如表2所示.為了保證數(shù)據(jù)集中的每一個等式的正確性(Eg≡Ec)，本文使用Z3求解器[26]對其進行驗證，并且保證數(shù)據(jù)集中的每一條數(shù)據(jù)都通過了該驗證.考慮到非多項式混合布爾算術(shù)表達式的復(fù)雜度和實用性，數(shù)據(jù)集共使用了10個不同的變量名.數(shù)據(jù)集中的表達式都是以字符串的形式進行保存，并且產(chǎn)生的表達式字符長度介于20到300之間.據(jù)本文所知，這是第一個大規(guī)模的非多項式混合布爾算術(shù)表達式數(shù)據(jù)集.

表2 數(shù)據(jù)集中的表達式示例Table 2 Samples in the dateset

4 實驗與結(jié)果分析

4.1 實驗設(shè)置

本文方法的實驗環(huán)境為：實驗操作系統(tǒng)為64-bit Ubuntu 20.04.4，CPU型號為Intel(R)Core(TM)i9-10980XE @ 3.00GHz，內(nèi)存為64GB DDR4.本文實驗使用2塊NVIDIA GeForce RTX 3090 GPU訓(xùn)練相關(guān)的神經(jīng)網(wǎng)絡(luò)模型.本實驗使用Python3編程語言，基于PyTorch框架以及PyTorch Geometric庫實現(xiàn)本文所提出的相關(guān)神經(jīng)網(wǎng)絡(luò)模型，同時使用Python AST庫實現(xiàn)圖序列模型中的預(yù)處理操作.

針對3.1節(jié)中所描述的神經(jīng)網(wǎng)絡(luò)模型，本文使用相同的實驗配置分別進行訓(xùn)練.首先，都對這些模型進行1000次的迭代訓(xùn)練，并將每次迭代的批次大小設(shè)置為128.同時在迭代過程中使用早停技術(shù)，該技術(shù)監(jiān)控驗證集損失下降程度來判斷是否需要提前終止訓(xùn)練過程，進而避免資源浪費.其次，本文使用Adam優(yōu)化器來學(xué)習(xí)神經(jīng)網(wǎng)絡(luò)模型中的參數(shù)，模型的初始學(xué)習(xí)率設(shè)置為1e-3，并在模型迭代的過程中使用ReduceLROnPlateau策略來動態(tài)調(diào)整學(xué)習(xí)率.最后，在模型預(yù)測階段，本文使用Z3求解器來判斷模型的輸出與輸入的表達式是否語義等價.

4.2 數(shù)據(jù)集設(shè)置

本實驗依據(jù)概率隨機抽樣法從3.2節(jié)生成的數(shù)據(jù)集中隨機采樣100000條樣本用以訓(xùn)練NeuSim的4個不同的神經(jīng)網(wǎng)絡(luò)模型，其中90%的數(shù)據(jù)作為模型的訓(xùn)練集，10%的數(shù)據(jù)作為模型的驗證集.實驗用的測試集是單獨重新生成的，以確保每一個測試樣本都不會出現(xiàn)在訓(xùn)練集中，測試集共含有10000個非多項式混合布爾算術(shù)表達式及其對應(yīng)的等價簡單表達式.

為了度量表達式的復(fù)雜度，本文使用以下3個指標來測量非多項式混合布爾算術(shù)表達式的復(fù)雜度，指標數(shù)值越大，也就意味著該表達式越復(fù)雜.

1)表達式中變量出現(xiàn)的次數(shù).在一個表達式中，所有的變量重復(fù)出現(xiàn)的總次數(shù).

2)表達式中操作符的個數(shù).在一個表達式中，布爾操作符和算術(shù)操作符重復(fù)出現(xiàn)的總次數(shù).

3)表達式長度.將一個表達式看成是一個字符串，該字符串的長度即為表達式的長度.

訓(xùn)練集和測試集中表達式復(fù)雜度的統(tǒng)計結(jié)果如表3所示，從表中均值一行可知，與簡單的表達式相比，相應(yīng)的非多項式混合布爾算術(shù)表達式的復(fù)雜度在幾乎每一個指標上都上升一個數(shù)量級.訓(xùn)練集中的非多項式混合布爾算術(shù)表達式的概率分布圖如圖2所示.

表3 數(shù)據(jù)集復(fù)雜度統(tǒng)計結(jié)果Table 3 Statistic of the datasets′ complexity

圖2 訓(xùn)練集中復(fù)雜表達式的分布Fig.2 Distribution of the complex expression in the training dataset

從圖2可知，表達式的復(fù)雜度分布基本都符合正態(tài)分布，這說明本文生成的數(shù)據(jù)集具有無偏性和隨機性.

4.3 同類化簡工具

從2.2節(jié)中可知，目前最先進的混合布爾算術(shù)表達式化簡工具有：MBA-Blast，MBA-Solver，SSPAM，和Syntia.本研究從Github上獲取了這些化簡工具的源碼，并在測試集中對其進行測試并記錄相關(guān)實驗結(jié)果.MBA-Blast可以高效化簡2-變量的混合布爾算術(shù)表達式，但是MBA-Solver可以化簡多變量的混合布爾算術(shù)表達式，它們都是一種語義等價的變換方法.SSPAM是一種模式匹配的化簡方法，其通過一個混合布爾算術(shù)表達式規(guī)則庫來進行表達式的替換和化簡.Syntia是一種基于程序合成技術(shù)的化簡方法，其通過學(xué)習(xí)混合布爾算術(shù)表達式的語義，產(chǎn)生一個語義等價但更簡單的表達式.

4.4 評價標準

本文使用以下3個指標來全面測試非多項式混合布爾算術(shù)表達式化簡工具的化簡性能：

1)正確率：經(jīng)過相關(guān)工具化簡之后，化簡結(jié)果與原表達式語義相等即為化簡正確.本研究對化簡結(jié)果通過Z3求解器進行驗證，以確定其與原表達式是否語義等價，如果等價則記為Ceq.正確率的計算方法如公式(2)所示.

(2)

2)復(fù)雜度：該指標用于衡量化簡后的表達式的可讀性，復(fù)雜度越高意味著其可讀性越低.本研究采用4.2節(jié)中的3個指標來測量化簡前后表達式的復(fù)雜度.

3)求解時間：該指標衡量化簡一個非多項式混合布爾算術(shù)表達式所耗費的時間.

4.5 實驗結(jié)果與分析

基于以上的實驗配置，本研究在訓(xùn)練集上分別訓(xùn)練NeuSim的各個模型，并通過網(wǎng)格搜索的方法使每個神經(jīng)網(wǎng)絡(luò)模型達到最佳性能表現(xiàn).然后在同一個測試集上對各個模型的化簡性能進行詳細測試，并且與同類工具的化簡結(jié)果進行比較.

本研究首先橫向比較各種工具的化簡結(jié)果正確性，所有化簡結(jié)果都通過Z3求解器進行驗證，驗證時間閾值設(shè)置為1小時，對所有在時間閾值內(nèi)無法給出結(jié)果的樣本判定為無法求解，相關(guān)實驗結(jié)果如表4所示.

表4 測試集上的化簡結(jié)果Table 4 Simplification results on the test dataset

實驗結(jié)果表明，已有的化簡工具都不能有效處理非多項式混合布爾算術(shù)表達式(化簡正確率都低于10%).其中，MBA-Blast和MBA-Solver的化簡有效性依賴于對輸入表達式中的子表達式求解：在化簡表達式時，這兩種方法首先需要識別表達式中可以被其處理的子表達式部分，然后通過化簡子表達式來處理輸入的表達式，最后處理表達式的其余部分，并給出最終的化簡結(jié)果.然而，非多項式混合布爾算術(shù)表達式中的子表達式通常具有隨機性和不確定性，在表達式中自動識別和正確處理相關(guān)的子表達式是極具技巧性的工作，而這導(dǎo)致MBA-Blast和MBA-Solver并不能很好處理非多項式混合布爾算術(shù)表達式.相比較于MBA-Blast，MBA-Solver能處理更多的表達式，這是因為MBA-Solver能夠化簡少量含有多變量的表達式.SSPAM在化簡表達式時，其遍歷該表達式與模式庫中的規(guī)則是否匹配，若匹配則進行替換和化簡.由于SSPAM中的模式庫僅包含少量多項式混合布爾算術(shù)規(guī)則，其在匹配和替換非多項式表達式時可能會產(chǎn)生錯誤的結(jié)果.Syntia在化簡表達式時首先進行表達式語義的輸入-輸出對采樣，之后根據(jù)采樣結(jié)果合成出一個語義等價的簡單表達式.而非多項式混合布爾算術(shù)表達式具有形式多樣性和語義復(fù)雜性的特點，這導(dǎo)致基于蒙特卡洛樹搜索進行表達式合成的方法(Syntia)并不能有效輸出語義等價的表達式.

與已有方法形成鮮明對比的是，本文所提出的字符串到字符串的解決方案NeuSim能夠正確化簡超過一半的非多項式混合布爾算術(shù)表達式，其中基于LSTM架構(gòu)的神經(jīng)網(wǎng)絡(luò)模型的化簡正確率超過66%，至少是已有工具化簡正確率的8倍.同時，與現(xiàn)有工具的化簡時間相比，NeuSim的平均化簡時間為0.01秒，這比現(xiàn)有工具至少快1個數(shù)量級.此外，對于一個輸入表達式，NeuSim的輸出是一個語法正確的表達式，而不是無規(guī)則的隨機字符串.從表4可知，基于GRU的模型相比于LSTM模型，其正確率稍有下降.這是因為基于GRU的NeuSim模型參數(shù)量只有基于LSTM模型的一半(表1可知)，更少的模型參數(shù)量往往意味著更低的學(xué)習(xí)能力，但更少的模型參數(shù)量也表示更少的顯存占用以及更短的訓(xùn)練時間.基于BERT的神經(jīng)網(wǎng)絡(luò)模型一般在海量數(shù)據(jù)的條件下會取得非常好的效果，但是本實驗訓(xùn)練數(shù)據(jù)量有限(10萬)，這造成基于BERT模型的化簡效果較差.另外，本文所研究的非多項式混合布爾算術(shù)表達式在表示成圖后，圖表示的復(fù)雜性將大幅高于相應(yīng)的字符序列表示方式，這大幅提升了圖序列神經(jīng)網(wǎng)絡(luò)學(xué)習(xí)非多項式混合布爾算術(shù)表達式語義的難度，進而造成圖序列神經(jīng)網(wǎng)絡(luò)模型較難化簡非多項式混合布爾算術(shù)表達式.

本文的第2個實驗測試相關(guān)工具化簡非多項式混合布爾算術(shù)表達式的化簡效果，即比較表4中的正確化簡結(jié)果在化簡前后表達式的復(fù)雜度，實驗結(jié)果如表5所示.

表5 化簡結(jié)果的復(fù)雜度Table 5 Complexity of the simplification results

從表5可知，對于所有能正確化簡的樣本，各種方法化簡后的表達式復(fù)雜度都有明顯的降低，比如其表達式平均長度這一指標被控制在10個字符左右.但是，SSPAM的化簡效果表現(xiàn)最差，這是因為該方法依賴模式庫中的規(guī)則，對于不在模式中的規(guī)則其化簡效果有限.相比于NeuSim，相關(guān)工具(MBA-Blast，MBA-Solver，和Syntia)的化簡結(jié)果更為簡潔.這主要是因為現(xiàn)有工具只能處理一些簡單和規(guī)則的非多項式混合布爾算術(shù)表達式，而NeuSim可以處理更復(fù)雜多樣的表達式，表6給出了一個具體的化簡示例.

從表6可知，已有工具在面對表中的復(fù)雜表達式時，通常不能輸出化簡結(jié)果或者輸出一個錯誤的化簡結(jié)果.而在NeuSim的輸出結(jié)果中，基于LSTM和GRU的模型輸出正確的化簡結(jié)果，基于BERT的模型輸出語義正確但形式上稍顯不同的結(jié)果，而圖序列模型給出了一個錯誤的化簡結(jié)果.

表6 化簡示例Table 6 Simplification samples

最后，本文橫向?qū)Ρ然诓煌窠?jīng)網(wǎng)絡(luò)模型的NeuSim訓(xùn)練時間，實驗結(jié)果如表7所示.從表中可知，基于圖序列的神經(jīng)網(wǎng)絡(luò)模型訓(xùn)練時間最短，為1.0秒每批次，這得益于其模型參數(shù)較少，且非循環(huán)結(jié)構(gòu)有利于模型的并行化處理，從而加速模型的訓(xùn)練進程.

表7 神經(jīng)網(wǎng)絡(luò)模型的訓(xùn)練時間Table 7 Training time of NeuSim

5 總 結(jié)

混合布爾算術(shù)表達式是指混合使用位運算符和算術(shù)運算符的表達式，它已經(jīng)被多個軟件混淆項目所采用.目前已有的反混淆方法都不能有效化簡非多項式混合布爾算術(shù)表達式，針對該挑戰(zhàn)，本文提出一種端到端的解決方案NeuSim.并且分別構(gòu)建基于序列到序列架構(gòu)和圖序列架構(gòu)的神經(jīng)網(wǎng)絡(luò)模型，并用這些模型來學(xué)習(xí)和化簡非多項式混合布爾算術(shù)表達式.同時，本研究收集并構(gòu)建了一個包含1000000條非多項式混合布爾算術(shù)表達式的數(shù)據(jù)集，并將其用于神經(jīng)網(wǎng)絡(luò)模型的訓(xùn)練.相關(guān)實驗結(jié)果表明，NeuSim化簡非多項式混合布爾算術(shù)表達式的的正確率大幅領(lǐng)先于已有的解決方案，并且其化簡時間可以忽略不計.