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

1(中國科學(xué)技術(shù)大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥 230026) 2(中國科學(xué)技術(shù)大學(xué) 安徽省高性能計(jì)算重點(diǎn)實(shí)驗(yàn)室，合肥 230026)

1 引 言

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

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

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

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

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

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

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

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

2 相關(guān)工作

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

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

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

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

(1)

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

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

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

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

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

3 化簡非多項(xiàng)式混合布爾算術(shù)表達(dá)式

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

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

本文基于編碼器-解碼器架構(gòu)[21]來實(shí)現(xiàn)NeuSim，其結(jié)構(gòu)主要分為兩部分：負(fù)責(zé)從輸入表達(dá)式中學(xué)習(xí)隱藏模式的編碼器，以及根據(jù)學(xué)到的知識(shí)預(yù)測表達(dá)式化簡結(jié)果的解碼器，模型結(jié)構(gòu)如圖1所示.NeuSim的輸入是一個(gè)以序列形式呈現(xiàn)的、長度可動(dòng)態(tài)變化的非多項(xiàng)式混合布爾算術(shù)表達(dá)式.編碼器通過學(xué)習(xí)輸入數(shù)據(jù)的特征，并輸出一個(gè)固定長度的隱藏狀態(tài)向量來表示學(xué)習(xí)到的表達(dá)式特征.解碼器是由循環(huán)神經(jīng)網(wǎng)絡(luò)組成，通過預(yù)先設(shè)定的字典，NeuSim可以將解碼器的輸出重構(gòu)成一個(gè)簡單的表達(dá)式，也就是對應(yīng)的非多項(xiàng)式混合布爾算術(shù)表達(dá)式的化簡結(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]，和注意力機(jī)制[24]的序列到序列的模型；同時(shí)，構(gòu)建基于圖卷積架構(gòu)[25]的圖序列網(wǎng)絡(luò)模型.在序列到序列的模型中，NeuSim直接將輸入的長度可變的非多項(xiàng)式混合布爾算術(shù)表達(dá)式輸出給編碼器.在圖序列模型中，NeuSim首先需要對輸入的非多項(xiàng)式混合布爾算術(shù)表達(dá)式進(jìn)行預(yù)處理(將輸入的表達(dá)式轉(zhuǎn)換成有向無環(huán)圖(DAG圖))，然后將DAG圖輸出給圖卷積編碼器.

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

混合布爾算術(shù)表達(dá)式多以字符串的形式進(jìn)行保存和處理，故本文首先研究如何構(gòu)造一個(gè)基于序列到序列架構(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]，和注意力機(jī)制BERT[24])作為NeuSim編碼器和解碼器的核心構(gòu)件，接下來將詳細(xì)介紹這3種神經(jīng)網(wǎng)絡(luò)模型的結(jié)構(gòu).

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

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

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

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

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

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

綜上所述，本文構(gòu)建并實(shí)現(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ù)來進(jìn)行訓(xùn)練.然而，相關(guān)文獻(xiàn)[3，6，17]只提供了少量非多項(xiàng)式混合布爾算術(shù)表達(dá)式(約1000個(gè)表達(dá)式)示例，這對于訓(xùn)練和測試NeuSim是明顯不足的.為此，本文根據(jù)相關(guān)文獻(xiàn)[3，6]中提出的方法來生成非多項(xiàng)式混合布爾算術(shù)表達(dá)式.這些方法的輸入為一個(gè)簡單的表達(dá)式，輸出為一個(gè)復(fù)雜的等價(jià)非多項(xiàng)式混合布爾算術(shù)表達(dá)式.

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

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

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

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

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

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

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

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

4 實(shí)驗(yàn)與結(jié)果分析

4.1 實(shí)驗(yàn)設(shè)置

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

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

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

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

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

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

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

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

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

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

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

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

4.3 同類化簡工具

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

4.4 評價(jià)標(biāo)準(zhǔn)

本文使用以下3個(gè)指標(biāo)來全面測試非多項(xiàng)式混合布爾算術(shù)表達(dá)式化簡工具的化簡性能：

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

(2)

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

3)求解時(shí)間：該指標(biāo)衡量化簡一個(gè)非多項(xiàng)式混合布爾算術(shù)表達(dá)式所耗費(fèi)的時(shí)間.

4.5 實(shí)驗(yàn)結(jié)果與分析

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

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

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

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

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

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

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

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

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

表6 化簡示例Table 6 Simplification samples

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

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

5 總 結(jié)

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