1、高鷹 等:基于概率語義的代碼迷惑有效性比較框架7量化的代碼迷惑有效性比較框架* Supported by the National Natural Science Foundation of China under Grant No. 60673126 (國家自然科學(xué)基金) 作者簡介: 高鷹(1980-),男,博士研究生,主要研究方向?yàn)槌绦蛟O(shè)計(jì)語言理論和實(shí)現(xiàn)技術(shù),主機(jī)代碼安全; 陳意云(1946-),男,教授,博士生導(dǎo)師, 主要研究領(lǐng)域?yàn)槌绦蛟O(shè)計(jì)語言理論和實(shí)現(xiàn)技術(shù),形式化方法,軟件安全等.第一作者聯(lián)系方式:Email:ygao4；聯(lián)系地址:安徽省合肥市中國科技大學(xué)西區(qū)8#240；郵編:2300

2、27；聯(lián)系電話鷹1 陳意云1，21(中國科技大學(xué)計(jì)算機(jī)系，合肥230026)2(中國科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)實(shí)驗(yàn)室，北京100080)摘 要：代碼迷惑是一種以增加理解難度為目的的程序變換技術(shù),用來保護(hù)軟件免遭逆向剖析.代碼迷惑是否有效是代碼迷惑研究中的首要解決的問題.而傳統(tǒng)的基于偏序的代碼迷惑有效性比較框架存在著表達(dá)力不足的問題。本文采用基于代數(shù)方法來比較代碼迷惑算法有效性，提出了一種基于緊算子的方式，擴(kuò)展了概率化抽象解釋在有限維下的定義，使得概率化抽象解釋可以適用于無限維的Banach空間。基于Banach空間，就可以定義度量，從而定量地比較代碼迷惑的有效性。關(guān)

3、鍵詞：概率化抽象解釋；程序變換；程序分析；代碼迷惑1 引言代碼迷惑是針對惡意主機(jī)問題而提出的一種保護(hù)客戶代碼的技術(shù)，它通過對代碼進(jìn)行程序變換，提高變換后代碼的理解難度，來達(dá)到保護(hù)客戶代碼的目的。代碼迷惑以前的研究主要集中在構(gòu)造有效的代碼迷惑算法。Collberg1中給出了有關(guān)這方面研究比較完整的綜述，引入了代碼迷惑的定義，代碼迷惑是一種以增加理解難度為目的的程序變換技術(shù)。Wang2建立了針對惡意主機(jī)問題的代碼安全體系，該安全體系的主要部件基于代碼迷惑技術(shù)構(gòu)造，而其中迷惑算法的核心思想是破壞程序的控制信息。Ogiso3推廣了Wang的算法，除了破壞程序控制流信息，進(jìn)一步地破壞程序過程間的調(diào)用信息

4、。Douglas4針對Java語言的特征，通過構(gòu)造復(fù)雜數(shù)據(jù)結(jié)構(gòu)來增加代碼的理解難度。關(guān)于構(gòu)造代碼迷惑算法的研究已經(jīng)比較成熟5。另一個(gè)重要的問題是：構(gòu)造的代碼迷惑算法是否有效。目前關(guān)于代碼迷惑有效性證明的研究有：Wang和Ogiso采用反迷惑算法的計(jì)算復(fù)雜度來證明代碼迷惑的有效性23，Barak6最早從密碼分析的復(fù)雜性角度來分析代碼迷惑的有效性。這些工作只是分析迷惑算法給反迷惑分析算法帶來分析時(shí)間上的影響，類似的，基于密碼理論的迷惑算法有效性研究也只是分析反迷惑算法的分析時(shí)間與所花費(fèi)的空間，而無法從分析的結(jié)果來證明代碼迷惑帶來的影響。針對目前代碼迷惑缺乏基于語義的有效性證明的問題，我們7使用抽象

5、解釋作為統(tǒng)一的框架來表示迷惑算法和模型化攻擊者，從語義的角度建立了代碼迷惑有效性比較框架。許多研究已經(jīng)證明了代碼迷惑作為安全方法的局限性，而我們的工作給出了積極的結(jié)果，為證明限定環(huán)境下的代碼迷惑安全性提供了有益的討論。類似的工作還有89。不過，這種基于偏序的傳統(tǒng)抽象解釋框架存在著表達(dá)力不夠的問題，也就是無法定量地度量代碼迷惑的有效性。針對這樣的問題，我們提出了一種基于緊算子的量化的度量方式。首先擴(kuò)展了概率化抽象解釋在有限維下的定義，使得概率化抽象解釋框架可以適用于無限維的Banach空間；然后，基于擴(kuò)展后的概率化抽象解釋框架，就可以定義出Banach空間中點(diǎn)之間的距離，從而達(dá)到定量地比較代碼迷

6、惑的有效性的目的。本文第2節(jié)概述目前代碼迷惑有效性框架中存在的問題，以及建立量化代碼迷惑有效性比較框架需要擴(kuò)展的部分；第3節(jié)描述了擴(kuò)展概率化抽象解釋使其能夠刻畫無窮維的語義空間的步驟；第4節(jié)基于新的概率化抽象解釋建立量化的代碼迷惑有效性度量；最后給出相關(guān)工作比較和結(jié)論。2 問題的提出關(guān)于代碼迷惑，Collberg1給出了非形式化的定義：定義（代碼迷惑）程序變換tob是代碼迷惑，是指：(1)變換tob保持程序可觀察行為的等價(jià)性；(2)經(jīng)過變換tob后得到的程序具有難以理解的屬性。抽象解釋提供了對不可計(jì)算語義進(jìn)行抽象的理論框架。我們提出了7基于抽象解釋框架的代碼迷惑有效性比較框架。迷惑的有效性比較

7、，按照抽象解釋的觀點(diǎn)，是指程序不同抽象粒度。這樣的抽象粒度可以通過抽象解釋格來給出序的關(guān)系。因此，利用這種偏序關(guān)系，從而達(dá)到比較迷惑算法有效性的目的。反映在下式： <Dôc><D1ôa1><D2ôa2> (1) 在式(1)中，a1是從D到D1的抽象, a2是D1到D2的抽象,則a2g a1是比a1更高粒度的抽象。因此，在此框架之下，要建立兩種代碼迷惑算法的有效性比較，首先需要建立二者間的抽象關(guān)系。而面對種類繁多的迷惑算法，這樣基于序的抽象關(guān)系是較難建立的。于是，基于序的有效性比較框架789在表達(dá)力方面就顯出了一定的局限性。概率化

8、抽象解釋的研究101112從量化的角度為程序的不確定性建立度量提供了啟示。概率化抽象分析框架是針對非確定性系統(tǒng)提出的抽象解釋框架。確定性程序是指程序具有這樣的性質(zhì)：程序的當(dāng)前的狀態(tài)唯一地確定下一個(gè)狀態(tài)。非確定性程序是指程序具有這樣的性質(zhì)：程序的當(dāng)前的狀態(tài)是按照某種概率分布來確定下一個(gè)狀態(tài)。雖然計(jì)算機(jī)是確定性機(jī)器，但是，許多因素都導(dǎo)致運(yùn)行的程序是非確定性的，如：程序的輸入，用戶的交互，外部異步事件。對于存在無法預(yù)測行為的系統(tǒng)，如允許中斷的計(jì)算機(jī)系統(tǒng)，中斷的到來是無法預(yù)測的，概率化系統(tǒng)就是對這類非確定性問題建模。代碼迷惑的目的是降低程序分析的分析精度，通常是在程序中引入不確定的程序結(jié)構(gòu)。一個(gè)例子就

9、是遲鈍斷言的構(gòu)造。遲鈍變量是許多迷惑工具中的基本應(yīng)用。由Collberg在文獻(xiàn)1中提出。如果變量V在程序點(diǎn)p具有某種屬性q，q在迷惑過程中是已知的，但是在分析時(shí)是難以理解的，這樣的表達(dá)式稱為是遲鈍的。遲鈍構(gòu)造的方式有：基于別名的構(gòu)造，在程序中構(gòu)造別名使程序結(jié)構(gòu)變得復(fù)雜。除此以外，并行化變換，將串行程序并行為等價(jià)的程序，我們知道在分析并行程序，需要維護(hù)的狀態(tài)空間是指數(shù)級增長的。對于程序分析來說，這些不確定性都是因?yàn)槌绦蛑性黾恿瞬豢深A(yù)測的因素，導(dǎo)致了程序分析精度的降低。因此迷惑的有效性定義基于對非確定性的刻畫是合理的。本文量化的代碼迷惑有效性框架分為兩個(gè)步驟建立：第一，我們將擴(kuò)展已有的有限維矢量空

10、間下的概率化抽象解釋框架。這需要分為兩步來做：首先，將定義在語義域<D，ôc>上的語義定義提升到基于矢量空間<Dp，>的語義，這里需要保證語義不動(dòng)點(diǎn)的存在性；然后，建立基于拓?fù)淇臻g的具體論域與抽象論域之間的抽象關(guān)系，當(dāng)然需要保證這樣的抽象關(guān)系的存在性。第二，定義了無窮維上的概率化抽象解釋框架，不同的迷惑算法將相同的具體域映射到可度量的矢量空間上，我們將定義距離從而刻畫出迷惑算法的有效性。3 概率化抽象解釋概率化抽象解釋11是抽象解釋針對概率化系統(tǒng)提出的一個(gè)變種，可以為不確定程序建立概率化分析結(jié)果。傳統(tǒng)的抽象解釋框架與概率化抽象解釋最大的不同就是語言域選擇的不同

11、，傳統(tǒng)抽象解釋的語義域是基于偏序的論域，而概率化抽象解釋是采用矢量空間來表示語義域。對于我們選擇的新的論域，需要知道兩點(diǎn)：(1)對于指稱語義來說，在這樣的論域定義下，是否存在語義不動(dòng)點(diǎn)？(2)基于矢量空間的論域不再適合經(jīng)典的抽象解釋理論。因此，對于抽象解釋來說，在這樣的論域下，是否存在一種關(guān)系是類似伽羅瓦聯(lián)系來聯(lián)系具體域和抽象域? 我們將在下文的定理1和定理2中回答這兩個(gè)問題。下面給出幾個(gè)概率化語義域的基本定義：定義1(矢量空間)：對于集合X，它的矢量空間V(X)，是指X中構(gòu)成的滿足以下兩個(gè)性質(zhì)的集合：1.保矢量加法閉；2. 保數(shù)乘閉。定義2(Banach空間)：Banach空間是指帶有范式定

12、義的完備矢量空間。3.1 傳統(tǒng)抽象解釋框架傳統(tǒng)抽象解釋定義有許多種形式，本文使用與程序分析聯(lián)系比較緊密的伽羅瓦聯(lián)系來描述抽象解釋框架。定義3(伽羅瓦聯(lián)系)：完全偏序集<L,ô>與完全偏序集<L,ô>滿足伽羅瓦聯(lián)系(Galois Connection)，是指存在抽象函數(shù)a：L®L以及具體函數(shù)g：L®L，"XÎL，"XÎL，滿足關(guān)系：a(X)ôXÛ Xôg (X)伽羅瓦聯(lián)系通過刻畫論域之間的聯(lián)系來得到抽象解釋定義。在抽象解釋中，抽象函數(shù)與具體函數(shù)滿足的性質(zhì)是：1ag

13、 g 是 reductive的，即："PÎL，ag g (P) ô P。2gg a 是外延的 ，即："PÎL，gg a (P) õ P。以及偽逆性3ag gg a = a 4gg a g g = g。基于有限維的矢量空間，同樣也存在著這樣類似性質(zhì)的定義4。定義4(Moore-penrose廣義逆)：如果C和D是兩個(gè)有限維矢量空間，A: C®D和G:D®C是一對有界線性算子。稱G是A的Moore-penrose廣義逆是指：當(dāng)且僅當(dāng) Ag G PA 且有G g A PG這里， PA和PG表示A和G范圍上的正交投影。Mo

14、ore-penrose廣義逆具有與伽羅瓦聯(lián)系類似的性質(zhì)：1A g G g A = A 2G g A g G = G3(A g G)* = A g G4(G g A)* = G g A傳統(tǒng)抽象解釋框架的主要思想就是為不可計(jì)算的具體語義建立抽象，是通過一種近似的抽象語義來達(dá)到，具體語義和抽象語義之間則是通過伽羅瓦聯(lián)系來保證可靠性。在下一節(jié)我們將建立概率化抽象解釋框架，其主要步驟是分為兩步：第一，建立概率化語義；第二，利用與伽羅瓦聯(lián)系類似的Moore-penrose廣義逆來建立概率化語義之間的可靠性聯(lián)系。3.2 概率化抽象解釋框架首先，為了定義概率化抽象解釋框架，需要先定義概率化語義。概率化語言的狀

15、態(tài)計(jì)算過程不同于以往其它語言的狀態(tài)計(jì)算，在狀態(tài)轉(zhuǎn)移的基礎(chǔ)上，還擴(kuò)展了量的概念，即加入了不同狀態(tài)轉(zhuǎn)移之間的概率。傳統(tǒng)指稱語義是將程序指稱到具有偏序結(jié)構(gòu)的論域之上，而概率化語義是以矢量空間作為其論域。建立概率化語義的基本做法是在傳統(tǒng)的指稱論域的基礎(chǔ)上，將帶有概率化的狀態(tài)空間提升到矢量空間。指稱語義是賦予程序某種數(shù)學(xué)指稱對象，例如傳統(tǒng)指稱語義下的偏序集，完全格。不是通過對論域的提升。而是通過對狀態(tài)空間的提升。下面我們介紹基于矢量空間的語義是如何建立的。給定傳統(tǒng)的傳遞系統(tǒng)T<S，Si，i>。其中，iÍS×S，表示狀態(tài)sÎS與其可能后繼sÎS的二元傳遞

16、關(guān)系，<s,s>Îi當(dāng)且僅當(dāng)sÎS(s)，簡記為s¯s。 傳統(tǒng)語義模型的關(guān)系，定義了狀態(tài)與狀態(tài)直接的聯(lián)系：RÍ C×C。在此基礎(chǔ)上，如果再考慮狀態(tài)與狀態(tài)之間轉(zhuǎn)移的概率，s(t) ÎDist(S)。對于每個(gè)二元傳遞關(guān)系，假設(shè)初始的概率是t，那么s 與s的二元傳遞關(guān)系可以記成s¯s(t)s，表示從狀態(tài)s到狀態(tài)s之間的轉(zhuǎn)移發(fā)生的概率是s(t)。這樣就可以定義線性算子：M(R)=給定一個(gè)概率化的傳遞系統(tǒng)X=（V(M)， A ，¯p）。V(M)表示線性算子組成的矢量空間，A是指動(dòng)作集合。于是可以定義它的矩陣或是算

17、子表示，對于每一個(gè)動(dòng)作集合的元素aÎA，都可以建立直和的表示： M(x) = M(¯a)直和的解釋為： M = Mi=下文使用Ma表示動(dòng)作的矩陣表示。即：矢量空間V(State)可以構(gòu)造為狀態(tài)的線性組合：V(State)=構(gòu)造使用狀態(tài)元素作為生成元。注意，依賴于狀態(tài)的勢，可以得到有限或是可數(shù)無限的線性組合。對于有限狀態(tài)集合，矢量空間同構(gòu)于標(biāo)準(zhǔn)實(shí)數(shù)矢量空間，n表示狀態(tài)的勢?？梢孕问降囟x矢量空間V(State)的元素:=。這樣的構(gòu)造能夠被看成是對冪集P(State)的等價(jià)構(gòu)造。對于概率化語義函數(shù)Y：Program´V(State)® V(State)來說，

18、如果從狀態(tài)State提升得到矢量空間是有限維的話。V(State)將可以使用矩陣算子來刻畫。而其語義函數(shù)的不動(dòng)點(diǎn)存在性,只要證明(M-I)X=0是否有解。這對于矩陣(M-I)來說無論其Jordan標(biāo)準(zhǔn)型不為單位矩陣即可（應(yīng)該是兩者之間存在的映射關(guān)系是矩陣）。這在文章11中已經(jīng)完成證明。而如果語義的矢量空間是無限維的，就不能再使用矩陣算子來刻畫。為了保證語義不動(dòng)點(diǎn)的存在，我們引入了采用緊算子組成的空間來刻畫矢量空間的做法。在無窮維的Banach空間中，有一類特殊的線性算子，它的性質(zhì)與有限維中的矩算子陣非常相似，這就是緊算子。定義5（緊算子）C和D 是Banach空間，設(shè)A：C®D線性；

19、稱A是緊算子，如果對于單位球B1，是D中的緊集，那么a是緊算子。C(C , D)表示所有C到D的緊算子。如果C = D，則簡記為C(C)。其實(shí)，有窮維Banach空間和無窮維Banach空間的根本區(qū)別之一是，在有窮維空間中，任意有界的點(diǎn)列必有收斂子列，但在無窮維Banach空間中，是不具備這樣的性質(zhì)的。而緊算子組成的空間重新獲得這樣的性質(zhì)。一個(gè)命題是，如果AäC(C , D)那么任意有界C中的有界點(diǎn)列都存在收斂列。緊算子的許多性質(zhì)都與矩陣類似。定義6(緊算子構(gòu)造的Banach空間)在緊空間C(C , D)上，對于Tä C(C , D)定義范式| T |= 。這樣的構(gòu)造就得到

20、了緊算子空間組成的Banach空間。這個(gè)空間將可以刻畫映射空間C是無窮維的情況，而比較矩陣算子只能刻畫映射空間為有限維矢量空間。下面我們需要證明當(dāng)語義域變成緊算子組成的拓?fù)浣Y(jié)構(gòu)時(shí)，概率化語義函數(shù)的定義是仍然有意義的，大致敘述如下：定理1 (語義不動(dòng)點(diǎn)存在性）在緊算子組成的Banach空間上的構(gòu)造的概率化語義存在著不動(dòng)點(diǎn)。這樣就確保了在緊算子定義的Banach空間的語義定義是有意義的。圖1說明了概率化語義建立的過程。對于傳統(tǒng)指稱語義而言，指稱語義將程序指稱到具有偏序結(jié)構(gòu)的具體域上。概率化語義則把這種序關(guān)系提升到矢量空間V(D)上，而為了刻畫無窮維狀態(tài)的情況，我們使用緊算子組成的空間C(D)作為概

21、率化語義的論域。 圖2 概率化抽象解釋關(guān)系圖下面給出概率化抽象解釋的基本框架，對于傳統(tǒng)的抽象解釋框架，抽象函數(shù)a和具體函數(shù)g建立了具體域<D，ôc>到抽象域<A，ôa>的正確性聯(lián)系。類似地，對于提升后的矢量空間論域V(D)和V(A)，也可以建立提升的抽象函數(shù)a和具體函數(shù)gat類似的正確性聯(lián)系。概率化抽象解釋中的具體域和抽象域都是矢量空間。只是對于有限維的是同構(gòu)于Rn,對于無窮維的矢量空間，我們采用基于由緊算子C組成的Banach空間來刻畫。對于傳統(tǒng)抽象解釋的具體域來說，其元素組成的空間通常都是無窮維的，例如把變量映射到值的狀態(tài)。而對于抽象域來說，通常

22、都是有限維的，例如符號分析時(shí)，所采用的論域是由3個(gè)元素組成的完全格。即:（，0），分別表示值的屬性是大于0，小于0和等于0。也就是說抽象狀態(tài)可能是由有限維元素組成的。概率化空間下使用Moore-penrose廣義逆來表示抽象域之間抽象聯(lián)系的，具與伽羅瓦聯(lián)系具有同構(gòu)的性質(zhì)。定義7 假設(shè)C和D分別是兩個(gè)概率論域，A: C®D和G:D®C是一對有界線性算子。如果滿足G是A的Moore-penrose廣義逆，那么就稱(C,A,G,D)組成概率化抽象解釋。按照這樣的構(gòu)造，(C,A,G,D)將被實(shí)例化為矢量空間V(C)和V(D).顯然，定義距離的矩陣算子屬于Banach空間。M(X,Y

23、)表示全體從X到Y(jié)上的矩陣算子。4的工作就是提出了X Y為有限維矢量空間時(shí)抽象解釋框架定義的有效性。如下： 定理(有限維矢量空間Moore-penrose廣義逆存在性) 對于任意有限維矢量空間中的元素總存在Moore-penrose廣義逆。對于有限維論域來說的如<，0>，它是有限維的我們可以構(gòu)造它的論域?yàn)椋簣D1 概率化語義定義a1=(1,0,0) ；a2=(0,1,0); a3=(0,0,1)但是，對于無窮維的語義論域來說，就無法使用這樣的辦法來構(gòu)造了。本文要研究的其實(shí)就是兩個(gè)Banach空間之間算子的性質(zhì)，下面我們會(huì)證明,只要是緊算子就一定能夠建立與有限維矢量空間上的等價(jià)的概率化

24、抽象解釋框架，即可以建立Banach空間之間存在Moore-penrose廣義逆組成的概率化抽象解釋。定理2 (Moore-penrose廣義逆的存在性）如果算子a是Banach空間C和D之間的緊算子，那么存在Moore-penrose廣義逆。這就保證了抽象a:C®D能構(gòu)造一個(gè)提升后的抽象a:V(C)®V(D)，而且這樣的構(gòu)造是保證了廣義逆的存在性。因此，根據(jù)Moore-penrose廣義逆的存在性定理，概率化抽象解釋框架是有意義的。 圖2說明了概率化抽象解釋與傳統(tǒng)抽象解釋之間的關(guān)系。傳統(tǒng)抽象解釋是基于伽羅瓦聯(lián)系來建立基于偏序的具體域和抽象域之間的聯(lián)系。為了針對無窮維的論域

25、，我們使用擴(kuò)展了概率化抽象解釋框架，使用緊算子組成的空間來作為具體域和抽象域，采用Moore-penrose逆建立具體域C(D)和抽象域C(A)之間的聯(lián)系。4 量化的代碼迷惑有效性對于程序p和迷惑后的程序tob (p)來說，在傳統(tǒng)的抽象解釋比較框架下，是需要找到某個(gè)有序論域下的偏序關(guān)系，使得存在關(guān)系：S§p¨ ôS§ tob(p)¨，其中S是指在該語義論域中定義的語義函數(shù)。這樣就能夠說明迷惑后的程序tob (p)是有效的代碼迷惑。這樣做的原因是，抽象解釋框架是基于指稱語義的，語義論域之間的關(guān)系刻畫了狀態(tài)與狀態(tài)之間定性的關(guān)系。而只要通過我們建立的

26、概率化抽象解釋框架，就可以建立語義論域之間的基于概率的量化關(guān)系。從而得到量化的代碼迷惑有效性比較框架。下面，基于上文推廣得到的Banach空間上的論域，給出評價(jià)迷惑算法有效性的量化尺度。設(shè)X(V(M)，A，¯p)是概率化傳遞系統(tǒng)。設(shè)X和Y分別是各自的算子表示，可以定義算子X和Y之間的距離為，| PTXP-Y | ，記為D(X, Y) 。如果對應(yīng)的域是不可計(jì)算的，就建立到可計(jì)算抽象域上的概率化抽象解釋框架(V(C),A,G,V(D)。我們知道G g X g A屬于抽象域?qū)?yīng)的Banach空間上。于是，可以通過不同的距離的變種來刻畫迷惑算法的有效性。命題1 D(tob (X), X) =

27、 | tob (X) - X |可以用來刻畫迷惑算法tob對程序迷惑的有限性。命題2 D(tob (X), tob (Y)=| G gtob (X)g A - G g tob (Y) g A |不同的迷惑算法作用于相同的程序,這兩個(gè)定義要求比較空間具有相同的階。命題3 對于不同的程序而言，可以通過對某個(gè)程序組成的矢量空間做投射，投射到具有相同維數(shù)的空間上來做比較，從而可以化歸到情況(1) (2)。這里的tob不是指傳統(tǒng)的代碼迷惑變化，是指改變量化狀態(tài)的代碼迷惑變換。一個(gè)例子：下面將使用一個(gè)具體的例子，來說明基于抽象解釋框架存在的問題以及在我們量化比較框架下是如何解決的。關(guān)于這個(gè)迷惑算法在流圖語

28、言下的形式定義，請參考文章7。FL1是指針對單語句級別上的壓平，我們又定義迷惑算法FL2，它是在雙語句級別上的壓平，即，壓平的最小單位是兩條連續(xù)的語句。我們來看FL1和FL2的意義。假定有程序P=(p1=1，s1)e( p2=1，s2)e( p3=1，s3)e( p4=1，s3)，經(jīng)過flattening算法FL1變換以后，可以得到變換后的程序FL1(P)。FL1 (P)= (p1=1/4，s1)|( p2=1/4，s2) | (p3=1/4，s3)e( p4=1/4，s4)。經(jīng)過flattening算法FL2變換以后可以得到。FL2 (P)= (p1=1/2，s1) e( p2=1，s2)|

29、 (p3=1/2，s3)e( p4=1，s4)。具體的效果圖見圖3。圖3 flattening后的控制流圖根據(jù)概率化語義到矢量空間的提升，可得到幾個(gè)矩陣:其中有A(P)= ；A(FL1(P)= 以及A(FL2(P)= 。顯然有：A(P), A(FL1(P), A(FL2(P)äV(Z)。根據(jù)命題1，要比較FL1和FL2的有效性，只要比較D(A(FL1(P),A(P)與D(A(FL2(P),A(P)的值即可。經(jīng)過計(jì)算：(1) D(A(FL1(P),A(P)=| A(P)-A(FL1(P) | =|1.231(2) D(A(FL2(P),A(P)=| A(P)-A(FL2(P) | =|

30、0.763在這里，就量化地反映出了不同的代碼迷惑算法FL1和FL2對程序不確定性的影響。FL1對不確定性的影響要比FL2的影響要大，也就迷惑的效果要比較好。而如果使用我們以前提出的傳統(tǒng)抽象解釋框架，對于不同的代碼迷惑算法，則建立FL1和FL2對于原程序的抽象函數(shù)，然后還需要建立這兩個(gè)抽象函數(shù)之間的偏序關(guān)系。而本文給出的量化的方法，相比之下具有明顯的簡潔性。5 相關(guān)工作比較我們的工作主要分為兩個(gè)部分：擴(kuò)充了概率化抽象解釋框架和將概率化抽象解釋應(yīng)用于評估代碼迷惑的有效性。因此，我們將分為兩個(gè)部分來做相關(guān)性比較。目前還缺乏基于代數(shù)方法來比較代碼迷惑算法有效性的工作。我們7和Dalla89 是從基于偏

31、序的語義域來對代碼迷惑進(jìn)行比較，為代碼迷惑有效性比較建立了形式化的語義基礎(chǔ)。但是這樣的工作存在著描述力不豐富的問題，并不能對于所有的迷惑算法實(shí)例之間都建立一種偏序的關(guān)系。而代數(shù)的方法可以量化迷惑算法之間的數(shù)值關(guān)系，而且我們能夠證明能夠用序的關(guān)系來定義的有效性，一定可以通過量化的有效性比較框架來表示。最初提出概率化抽象解釋框架的是11的工作，他們采用線性映射也就是Moore-penrose逆，定義了安全可靠的不動(dòng)點(diǎn)語義。Pierro等人的工作10以代數(shù)的方式為概率化語言建立程序狀態(tài)的轉(zhuǎn)移。他們同樣是將程序的狀態(tài)提升到矢量空間之上，然后對應(yīng)于傳統(tǒng)的操作語義函數(shù)的定義，將C*代數(shù)中的元素看作是，C*

32、代數(shù)是帶有底域K的矢量空間。下面將證明本文在無窮維矢量空間上擴(kuò)展的工作同樣也滿足他們的結(jié)論。C*代數(shù)是一種Banach算子，它具有滿足以下性質(zhì)的算子*：(x*)* = x，x*y* =(yx)*，x*+y*= (x+y)* (cx)*=cx*，其中c是c的復(fù)共軛且他們的范式滿足性質(zhì)：| x x* | = | x |2。C*代數(shù)是具有環(huán)的矢量空間。需要注意的是矩陣代數(shù)是屬于C*代數(shù)。我們將證明使用緊算子構(gòu)成的Banach空間與這個(gè)結(jié)論是等價(jià)的?？梢宰C明，緊算子組成的拓?fù)淇臻g也是屬于C*代數(shù)。也就是以下定理。定理3 C (V)´ C*(X,Y)。證明：根據(jù)我們緊算子構(gòu)成Banach空間的

33、構(gòu)造（定義6）：在緊空間C(C , D)上，對于Tä C(C , D)定義范式| T |=對于緊算子的范式| T |，其復(fù)共軛| T* |=| T |,，因此會(huì)有| x x* | = | x |2，因此，緊算子組成的空間也是屬于C*代數(shù)的。6 結(jié)論本文的工作為證明限定環(huán)境下的代碼迷惑安全性提供了有益的討論。以前的基于偏序的代碼迷惑有效性比較框架在表達(dá)力方面具有一定的局限性，無法為各種代碼迷惑算法都建立有效性比較，本文從概率化抽象解釋框架出發(fā)，建立了對程序不確定性的量化比較關(guān)系，從而達(dá)到量化比較代碼迷惑有效性的目的。7 附錄(定理證明)在證明定理1之前，首先引入文10定義的語言和其對應(yīng)

34、的語義。A := b 基本動(dòng)作 | p: A 加權(quán)語句 | g® A guarded statement | 序列組合| 選擇| proc 函數(shù)調(diào)用圖1. 概率通用語言的語法概率語言是指從語法上區(qū)分符號與數(shù)值(概率)的終結(jié)符，主要是研究語句在量上的性質(zhì)。§ b ¨ B 基本動(dòng)作 | p: A 加權(quán)語句 | g® A guarded statement | 序列組合| 選擇| proc 函數(shù)調(diào)用圖2. 概率通用語言的語義g表示guard ，p表示量化信息，這里表示的概率如前文所述，概率語言是指從語法上區(qū)分符號的和數(shù)值(概率)的終結(jié)符，主要是研究語句在量上的

35、性質(zhì)。定理1 (語義不動(dòng)點(diǎn)存在性）采用緊算子構(gòu)造出的Banach空間下也是存在不動(dòng)點(diǎn)的。證明：根據(jù)泛函分析中的賦范定理，不動(dòng)點(diǎn)語義Y:A® C (V)：Y§ b ¨ = B 基本動(dòng)作Y§ p: A ¨ = p§A¨ 加權(quán)語句Y§ g® A¨ = G§A¨ guarded statementY§¨ = 序列組合Y§¨ = 選擇Y§ proc ¨ = §A¨ 函數(shù)調(diào)用圖3. 概率通用語言的不動(dòng)點(diǎn)語義引

36、理1設(shè)C是B*空間X中的一個(gè)閉凸子集，T：C®C連續(xù)且T(C)列緊，則T在C上必有一個(gè)不動(dòng)點(diǎn)。這個(gè)引理描述了賦泛空間上一個(gè)閉凸子集之上的算子的不動(dòng)點(diǎn)存在性，通常的語義函數(shù)都是連續(xù)的，還需要兩點(diǎn)來保證不動(dòng)點(diǎn)的存在。1 語義函數(shù)在語義域上是列緊的2 緊算子構(gòu)成的Banach語義域是閉凸的。根據(jù)文章10中4.2.2節(jié)中提到的命題4.15，可以知道不動(dòng)點(diǎn)語義函數(shù)Y是列緊的。因此，只要我們能夠證明基于拓?fù)涞恼Z義域是閉凸的即可。引理2緊算子構(gòu)成的Banach語義域是閉凸的。(1)有界性。證明：如果AäC(V)，因?yàn)閥®|y|是連續(xù)的，有： M =<¥Þ

37、;£M|x|(2)閉性。即：A，BäC(V)，a,bäV，則 aAbBä C(V)證明： 設(shè) Tn ä C (V)，n=(1,2,)，且®0，要證明的是：Tä C (V)，也就是收斂列也是閉的。 "e>0，取näN，使得<e/2，對 取有窮e/2網(wǎng)，設(shè)為y1 ,y2,yn，則有Ì，從而有有窮e網(wǎng)，由緊算子定義，得到為緊。結(jié)合引理1，引理2，就可以得到不動(dòng)點(diǎn)語義Y在緊算子構(gòu)造的論域上存在不動(dòng)點(diǎn)。定理2 (Moore-penrose廣義逆的存在性）如果算子A是Banach空間C和D之間的

38、緊算子，那么存在Moore-penrose廣義逆。 證明：需要證明對于任意AäC(V)，從它的一切非0本征值l1,l2,都可以找到對于的Jordan標(biāo)準(zhǔn)型。這樣就可以證明算子A存在一個(gè)G使得AoG是一個(gè)投影。（1）N(Tp)Ç R(Tp)=q。如果有yäV，使得y= Tpx.且有Tpy=q，從而 Þ xä N(Tp) Þ Tpy=q(2) V= N(Tp)Å R(Tp). 因?yàn)閷τ?quot;xäV 都有Tpxä R(Tp)= R(T2p)。定義y= Tpuä R(Tp).因?yàn)門py=Tpx，于

39、是得z=x-yä N(Tp)，從而 Þx=y+z (y ä R(Tp) ;y ä N(Tp) )（ 其中 R(T)=T(V)；N(T)=xäV | Tx=q） 因此，緊算子能夠得到其對應(yīng)的Jordan標(biāo)準(zhǔn)型。從而得證。References：1. C Collberg,C Thomborson and Douglas Low. Taxonomy of Obfuscating Transformations. Technical Report #148, Department of Computer Science, the University

40、of Auckland,Dec,19972. Chenxi Wang. A security Architecture for survivability Mechanisms. PhD thesis, University of Virginia, Department of Computer ,20023. T.Ogiso, Y.Sakabe. Software obfuscation on a theoretical basis and its implementation. IEEE trans,Fundmentals,20024. Douglas Low. Protecting Ja

41、va code via code obfuscation , ACM Crossroad, Spring issue 1998,4(3):21235. Li YX, Chen YY. Technique of Code Obfuscation Based on Function Pointer Array. Chinese Journal of Computers 2004,27(12):1706-1711.(in Chinese)(李永祥,陳意云.基于函數(shù)指針數(shù)組的代碼迷惑技術(shù).計(jì)算機(jī)學(xué)報(bào).2004,27(12):1706-17)6. B.Barak, O.Goldreich, R.Impa

42、gliazzo, S.Rudich, A.Sahai, S.P.Vadhan, and K.Yang. On the (im)possibility of obfuscating programs, in Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology (CRYPTO '01), J. Kilian, Ed. Santa Barbara, California: Springer-Verlag, Aug. 19-23 2001, pp. 1187.

43、Gao Y, Chen YY. A comparable code obfuscation frame work measuring efficiency based on abstract interpretation. Chinese Journal of Computers. Accepted.(in Chinese)(高鷹,陳意云.基于抽象解釋的代碼迷惑有效性比較框架.計(jì)算機(jī)學(xué)報(bào),已錄用)8. M.Dalla Preda and R.Giacobazzi. Semantic-based code obfuscation by abstract interpretation. In Pr

44、oc. ICALP, 20059. M.Dalla Preda and R.Giacobazzi. Control code obfuscation by abstract interpretation. In Proc. SEFM, 200510. Di Pierro and H. Wiklicky. Operator Algebras and the Operational Semantics of Probabilistic Languages. Electronic Notes in Theoretical Computer Science. Volume 161, 2006.11.

45、Di Pierro and H. Wiklicky. Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. In M.Gabbrielli and F.Pfennning, editor. In: Proceedings of PPDP00, Monteeal, Canada. 200012. Di Pierro and H. Wiklicky. Linear Structure for concurrent programming languages. In M.Gabbrielli

46、 and F.Pfennning, editor. In: Proceedings of PPDP00, Monteeal, Canada. 200113. Edalat, P.Shunderhauf. Computable banach spaces via domain theory. In: Theoretical Computer Science 1999,219(1-2), 169184A quantitative comparable framework measuring code obfuscation efficiency GAO Ying1), CHEN Yi-Yun1),

47、 2)1) (Department of Computer Science & Technology, University of Science & Technology of China, Hefei, 230026)2) (Laboratory of Computer Science, Institute of software, Chinese Academy of Sciences, Beijing, 100080)Abstract：Code obfuscation, which is an effective program transformation, can

48、obscure the program understanding and thus protect the program from reverse engineering. The efficiency of code obfuscation is of prime importance in the research field. However, the existing comparable framework based on partial order cannot measure the efficiency between any code obfuscations. In this paper, we propose a mathematical comparable framework measuring obfuscation efficiency, which provides a quantitative approach for measuring the efficiency. We extend the probabilistic abstract interpretation b