江 南，何炎祥，張曉瞳，劉 瑞，沈云飛

1.武漢大學(xué) 計算機(jī)學(xué)院，武漢 430072

2.湖北工業(yè)大學(xué) 計算機(jī)學(xué)院，武漢 430068

3.武漢大學(xué) 軟件工程國家重點(diǎn)實驗室，武漢 430072

Java安全性機(jī)制的形式分析與證明*

江 南1,2+，何炎祥1,3，張曉瞳1，劉 瑞1，沈云飛1

1.武漢大學(xué) 計算機(jī)學(xué)院，武漢 430072

2.湖北工業(yè)大學(xué) 計算機(jī)學(xué)院，武漢 430068

3.武漢大學(xué) 軟件工程國家重點(diǎn)實驗室，武漢 430072

JIANG Nan,HE Yanxiang,ZHANG Xiaotong,et al.Formal analysis and proof of Java security mechanisms. Journal of Frontiers of Computer Science and Technology,2016,10(11):1501-1511.

Java訪問控制一方面提供了語言級的安全性機(jī)制，這種機(jī)制針對程序中所聲明的實體，通過不同的訪問修飾符，向其使用者屏蔽實體的實現(xiàn)細(xì)節(jié)；另一方面，它也導(dǎo)致了該語言規(guī)范的復(fù)雜性和實現(xiàn)的不一致性。分析了Java訪問控制機(jī)制，包括類型、成員變量和成員方法的可訪問性，以及可訪問性與繼承關(guān)系、方法覆蓋、動態(tài)綁定之間的交互；然后使用定理證明助手Isabelle/HOL 2015嚴(yán)格定義了這些語義規(guī)范；最后陳述并證明了這些定義所滿足的性質(zhì)定理，從而表明該形式化定義的正確性。

Java訪問控制；動態(tài)綁定；形式分析；定理證明

1 引言

Java編程語言提供了語言級的訪問控制（access control）機(jī)制，這種機(jī)制針對程序中所聲明的實體，指出它們在哪些程序代碼部分可以通過限定名（qualified name）、成員變量訪問表達(dá)式或成員方法調(diào)用表達(dá)式進(jìn)行訪問，實體使用者無需知道實體的實現(xiàn)細(xì)節(jié)?？稍L問性（accessibility）可在編譯時確定，它取決于被訪問實體的類型、聲明時的訪問控制修飾符（modifier），以及成員訪問表達(dá)式出現(xiàn)在哪個類中，并對Java編程語言的許多關(guān)鍵特性，譬如繼承（inheritance）、方法覆蓋（method overriding）和動態(tài)綁定（dynamic binding）產(chǎn)生影響。下文為了闡述方便，如果成員訪問表達(dá)式出現(xiàn)在方法 f中，方法 f聲明在類C中，則稱C為成員訪問表達(dá)式的訪問類。

訪問控制一方面提供了語言級的安全性機(jī)制，將統(tǒng)一接口提供給使用這些實體的用戶，屏蔽實體的實現(xiàn)；另一方面，它也導(dǎo)致了語言規(guī)范的復(fù)雜性，從而可能導(dǎo)致語言實現(xiàn)與其規(guī)范的不一致。Java語言規(guī)范（Java language specification，JLS）已經(jīng)從1996年的第1版更新到了2014年的Java SE 8[1]，通過詳細(xì)地比較JLS不同版本對訪問控制及其相關(guān)內(nèi)容的描述，發(fā)現(xiàn)：JLS3針對JLS2中的模糊性進(jìn)行了改進(jìn)；JLS SE7與JLS3對訪問控制的描述相同；Java規(guī)范請求（Java specification request，JSR）335（Java語言的Lambda表達(dá)式）對缺省訪問修飾符下的方法覆蓋條件進(jìn)行了更具體的描述，JLS 8與該改進(jìn)一致。從這些變遷發(fā)展可以看出，自然語言描述的語言規(guī)范很可能是不準(zhǔn)確的，由于訪問控制是非常重要的一個語言特性，有必要對其進(jìn)行形式化定義，這就是本文的研究動機(jī)。

許多文獻(xiàn)針對Java或者Java虛擬機(jī)進(jìn)行形式建模[2-9]。其中，針對Java訪問控制的形式化分析成果并不多見，Schirmer做了有意義的研究工作，其針對JLS2和其實現(xiàn)Sun jdk1.3以及IBM的Java編譯器之間的一個不一致問題進(jìn)行了分析[10-11]，該問題就是由規(guī)范中與訪問控制相關(guān)的繼承和方法覆蓋的含糊描述所導(dǎo)致的。Sun將該問題視為編譯器的一個bug，在其實現(xiàn)jdk1.4中進(jìn)行了更正。

本文以JLS和JLS8為參考，代碼段的編譯和運(yùn)行使用jdk1.7和jdk1.8，在定理證明助手Isabelle/ HOL 2015[12-13]的支持下，形式分析了Java訪問控制機(jī)制，以及可訪問性與繼承、方法覆蓋、動態(tài)綁定之間的交互，并使用定理證明助手Isabelle/HOL 2015嚴(yán)格定義了這些語義規(guī)范，通過證明這些定義所滿足的性質(zhì)定理，證明了這些形式化定義的正確性。另外，由于訪問控制是Java一個重要卻又復(fù)雜的語言特性，本文工作表明，形式設(shè)計一門現(xiàn)實的編程語言應(yīng)該是可行的。

本文組織結(jié)構(gòu)如下：第2章解析了JLS的訪問控制；第3章對支持包機(jī)制的程序進(jìn)行定義；第4章針對第2章所解析的訪問控制，逐步定義了成員的可訪問性，并進(jìn)一步討論了方法覆蓋和動態(tài)方法查找；第5章是相關(guān)定理，證明了以上形式定義的正確性；最后進(jìn)行了相關(guān)工作分析和總結(jié)。

2 JLS訪問控制解析

Java訪問修飾符包括公有（public）、受保護(hù)的（protected）、缺?。ㄒ卜Q為包package訪問）和私有（private）4種。訪問修飾符作用于不同類別的實體，包括類、成員變量和成員方法等。因此，本部分按類型的可訪問性和成員的可訪問性兩方面展開討論。

2.1 類型的可訪問性

Java中每個類是一種類型，稱為類類型，數(shù)組也是一種類型，它們都稱為引用類型。JLS規(guī)定：一個引用類型是可訪問的，當(dāng)且僅當(dāng)以下條件成立：

（1）一個類若聲明為公有訪問，那么該類類型可以被所有代碼訪問；

（2）一個類若未聲明訪問修飾符，那么在這種缺省情況下默認(rèn)是包訪問，該類類型僅在其聲明所在的包范圍內(nèi)可以訪問；

（3）如果數(shù)組元素的類型是可訪問的，那么該數(shù)組類型是可訪問的。

按照這個規(guī)定，形式定義時首先需要建模包，進(jìn)而定義類和程序，從而可以取出構(gòu)成一個實體的各個部分。由于以上條件約束并不復(fù)雜，直接在相應(yīng)部分進(jìn)行修飾符匹配就可以確定。

2.2 成員的可訪問性

JLS規(guī)定：一個類類型的成員是可訪問的，當(dāng)且僅當(dāng)以下條件成立：

（1）該類類型是可訪問的，如2.1節(jié)所述。

（2）成員訪問修飾符滿足以下條件：如果聲明為私有訪問，則僅在聲明該成員的類體中是可訪問的；如果聲明為缺省訪問，則在聲明該成員的類所在的包范圍內(nèi)是可訪問的；如果聲明為公有訪問，則該成員總是可訪問的；如果聲明為受保護(hù)的訪問，則在以下兩種情況下是可訪問的：

①在成員的聲明類所在的包范圍內(nèi)訪問該成員；

②在成員的聲明類所在的包范圍外訪問該成員時，假定聲明該成員的類是C，受保護(hù)的成員是m，則應(yīng)該滿足的條件是：在C的子類S的類體中訪問該成員，即訪問類是C的子類；如果以Q.m或者Q.m（…）的形式訪問，Q的類型應(yīng)該是S或者S的子類型。

條件（2）中受保護(hù)的訪問復(fù)雜化了成員的訪問控制機(jī)制，如圖1所示。

在圖1（a）中，在包x中聲明了類A，類A聲明了一個受保護(hù)的成員i；在同一個包x中聲明了類B。按照上述條件，類B成員方法f（）中的語句a.i=100是編譯正確的，因為：（1）a的類型是類類型A，類型A聲明為公有，因而A在類B中是可訪問的（A和B同包也是令B可以訪問A的另一理由）；（2）i是受保護(hù)的，i在A中聲明，且A與訪問類B同包，滿足條件①。

在圖1（b）中，由于訪問類B與類A的聲明在不同包中，且B不是類A的子類，因此a.i編譯報錯。

在圖1（c）中，雖然訪問類B是類A的子類，但是表達(dá)式a.i中a的類型是類A，而A不是B，也不是B的子類，因此a.i編譯報錯。

在圖1（d）中，訪問B是A的子類，且c的類型是C，而類C是A的子類，因此a.i編譯正確。

Fig.1 Access to a protected member圖1 受保護(hù)成員的可訪問控制

從上例中可以看出，受保護(hù)的訪問控制規(guī)定了當(dāng)訪問類不與訪問的成員所在的類屬于同一個包時，一定是在其子類中對該成員進(jìn)行訪問。如果將圖1（c）中的a.i換成i，則編譯正確，因為i是this.i的簡寫，而this的類型是B，它是A的子類型；但是若將圖1（b）中的a.i換成i，編譯仍然報錯，因為此時this的類型是B，它并沒有繼承A，類型B沒有一個名為i的成員變量。

訪問修飾符也影響了成員的繼承性和方法覆蓋的定義。按照J(rèn)LS規(guī)范，類B中聲明的方法M覆蓋了類A中聲明的方法N，當(dāng)且僅當(dāng)B是A的子類，并且M和N具有相同的方法簽名，以及滿足以下條件：

（1）方法N是公有的或者受保護(hù)的，或者缺省訪問且A和B在同一個包中；

（2）方法N是缺省訪問時，M覆蓋了類C中聲明的方法O，并且O覆蓋了N。

在圖2所示的代碼段中，包P中的類A聲明了一個缺省訪問方法 f，同一個包中聲明的類B繼承A，也定義了一個相同簽名的方法 f，因此，根據(jù)上述條件（1），類B中的方法 f覆蓋了其父類A中的缺省訪問修飾符的方法 f。包Q中聲明的類C繼承類B，C中聲明了一個相同簽名的方法 f，因此，同樣根據(jù)上述條件（1），類C中的方法 f覆蓋了其直接父類B中的公有方法 f。但是，類C中的方法 f是否覆蓋了其父類A中的方法 f呢？從測試類TestABC中可以看出，當(dāng)類型為A的引用變量a引用到了子類C的對象，調(diào)用方法 f時，執(zhí)行的是類C中方法 f的方法體，輸出C，顯然虛擬機(jī)運(yùn)行時認(rèn)為類C中的方法f覆蓋了類A中的方法 f。然而按照條件（1），這是不成立的；C.f覆蓋了A.f可由條件（2）推出：因為類C中的 f覆蓋了類B中的 f，且類B中的 f覆蓋了類A中的 f，所以類C中的 f覆蓋了類A中的 f。條件（2）的出現(xiàn)使得方法覆蓋成為一個遞歸描述，在形式化定義時更為復(fù)雜。

Fig.2 Overriding a method with default access圖2 缺省訪問控制下的方法覆蓋

3 程序的定義

為了說明4種訪問修飾符作用在程序代碼的哪些部分，首先需要建模包和定義程序。在Java中，包組織為文件層次結(jié)構(gòu)，這個層次結(jié)構(gòu)僅在包查找時起作用，它與訪問控制本身無關(guān)。因此，可將包名定義為一個字符串類型，將類的簡單名加上包名形成限定名（qualified name）來建模包的概念，即qname= pname×cname。其中，pname和cname都是字符串類型string的別名，下文出現(xiàn)的類名均指類的限定名。式（1）表示，類聲明cdecl是類的限定名與其類體組成的二元組，程序prog由類聲明列表組成。其中，′m是類型參數(shù)，代表方法體；prog既可用于表示Java源程序，又可用于表示虛擬機(jī)字節(jié)碼程序。

4種訪問修飾符定義為一個新的數(shù)據(jù)類型，如式（2）所示。

因此，成員變量fdecl和成員方法mdecl的定義如式（3）所示。

它表示：成員變量聲明是由成員變量名、類型和訪問修飾符所組成的三元組；成員方法聲明是由msig和methd組成的二元組，msig代表方法簽名、描述方法名和形參類型列表，methd是返回值類型、方法體和訪問修飾符組成的三元組。其中。vname和mname均是string的別名。因此，式（1）中的class的定義如式（4）所示。

它表示：類由其直接超類名、成員變量列表、成員方法列表以及訪問修飾符所組成。

元組(x1,x2,x3)視為(x1,(x2,x3))，fst取得元組的第1個分量，snd取得第2個分量，因此，fst(x1,x2,x3)=x1，snd(x1,x2,x3)=(x2,x3)。

式（3）中的ty代表類型，它的定義如式（5）所示。類型包括簡單類型和引用類型，其中簡單類型是布爾類型和整型，引用類型包括類類型和數(shù)組類型以及NT。

P?C?1D表示在程序P中，類C的直接父類是D。P?A?*B定義為直接子類關(guān)系上的傳遞閉包，P?M?*N定義為直接子類關(guān)系上的自反傳遞閉包，下文在闡述時將這兩種關(guān)系都稱為子類關(guān)系。P?S≤T定義為子類型關(guān)系，如式（6）所示，它表示：任意一個類型是其自身的子類型；如果C是D的子類，那么類型Ref(Class C)是類型Ref(Class D)的子類型；引用類型NT是所有引用類型的子類型；如果C是D的子類型，那么Ref(Array C)是Ref(Array D)的子類型；數(shù)組類型是Object類類型的子類型。

4 可訪問性和動態(tài)綁定

4.1 類型的可訪問性

按照第2章的分析，本節(jié)首先定義類型的可訪問性。簡單類型總是可以訪問的，引用類型按照2.1節(jié)的分析，其可訪問性定義如式（7）所示。其中，函數(shù)類型聲明中的括號規(guī)定了調(diào)用函數(shù)的直觀書寫形式，為避免重復(fù)，以下出現(xiàn)的直觀書寫形式不再一一說明。

按照式（5）的定義，ty由簡單類型Prim prim_ty和引用類型Ref ref_ty組成，數(shù)組類型是一種引用類型，它的可訪問性取決于數(shù)組元素的類型，而元素的類型可以是任意ty類型，因此式（7）是互遞歸函數(shù)（mutual recursion）。函數(shù)tyAcc在對簡單類型進(jìn)行判斷時，直接返回真值；在對引用類型進(jìn)行判斷時，調(diào)用函數(shù)rtAcc。函數(shù)rtAcc在對NT類型進(jìn)行判斷時，直接返回真值；在對類類型進(jìn)行判斷時，如果類類型在給定的包范圍內(nèi)聲明，或者該類是公有的，則返回真值；在對數(shù)組類型進(jìn)行判斷時，調(diào)用tyAcc來判定數(shù)組中元素類型的可訪問性。

4.2 類的成員

為了對成員的可訪問性進(jìn)行形式規(guī)范，首先要判定哪些成員是給定類的合法成員。一個類類型（非Object）的成員包括：聲明在本類中的成員和從直接父類（或父接口）繼承得到的成員。一個類從它的直接父類或父接口繼承到非私有的、且未被覆蓋和隱藏的成員。

由于類的成員可由其父類繼承得到，判斷是否是類的成員應(yīng)該是遞歸方式的。不同類中可以定義相同簽名的方法或相同變量名的變量，因此下文形式定義中使用了一個新的結(jié)構(gòu)：由聲明類和聲明本身組成的二元組mmtd::(qname×′m mdecl)。式（8）定義了一個歸納謂詞（inductively defined predicate）method::′m prog?(qname×'m mdecl)?qname?bool。它的定義體現(xiàn)了遞歸性：按照ImmediateM規(guī)則，如果mmtd的聲明類是C，且該聲明是類C中一個方法，則mmtd是類C的一個成員方法，即本類中聲明的方法是本類的合法成員方法；繼承得到的成員由歸納規(guī)則InheritedM判定，如果類C的直接父類是D，mmtd是D的成員，并且同時滿足以下繼承條件：

（1）mmtd對于類C而言是可繼承的(P?mmtd inheritableM_in(fst C))；

（2）類C中沒有聲明與其簽名相同的方法(P?fst(snd mmtd)undeclM_in C)；

（3）類型D對于類型C是可訪問的(P?Ref (Class D)acc_in(fst C))。

那么，mmtd是C的成員。

條件（1）的定義如式（9）所示，表達(dá)的意思是：私有成員不可繼承；受保護(hù)的和公有成員可以繼承；對于包訪問修飾符的成員：如果該成員的聲明類是定義在包P中的，則可以繼承。

條件（2）的定義如式（10）所示，其中，getMethod-MapP C=(case map_of P C of None?empty|??c?map_ (fst(snd(snd c))))。判斷一個方法是否未聲明在某個類中時，判斷的是方法簽名，即方法名和參數(shù)類型。

根據(jù)成員變量名判斷是否在一個類中聲明了該成員變量，類的成員變量的判定與成員方法的判定幾乎相同，為避免重復(fù)，在此省略。條件（3）類型的可訪問性在4.1節(jié)已經(jīng)定義。

4.3 成員訪問修飾符的限制條件

成員訪問修飾符的限制條件與訪問類相關(guān)，如式（11）所示。

上式表示：類C的成員方法mmtd是否允許從訪問類accCls中進(jìn)行訪問。其中，getAccM取方法聲明中的最后一個分量，代表該方法的訪問修飾符。當(dāng)訪問修飾符是Private時，判斷是否在方法聲明所在的類中對該方法進(jìn)行訪問；當(dāng)訪問修飾符是Package時，判斷fst(fst mmtd)是否與訪問類在同一個包；當(dāng)訪問修飾符是Public時，返回值為真；當(dāng)訪問修飾符是Protected時，如果方法的聲明類與訪問類同包，則返回值為真，或者如果訪問類是方法聲明類的子類，并且類C是訪問類的子類或者就是訪問類本身。

4.4 成員的可訪問性

完成了4.1至4.3節(jié)的定義后，就可以給出成員可訪問性的完整定義。函數(shù)P?mmtd of X accM_ from accCls判斷X的成員mmtd是否可以從訪問類accCls中進(jìn)行訪問，它的定義如式（12）所示。

設(shè)方法調(diào)用表達(dá)式為e.m{accC statT pTs}(ps)，其中e代表調(diào)用方法的對象，m是方法名，ps是實參，大括號中accC、statT和pTs不是程序本身的代碼，accC是訪問類。式（13）給出了方法調(diào)用表達(dá)式的類型規(guī)則，如果滿足這個規(guī)則，方法調(diào)用是合法的，它用于編譯時和字節(jié)碼驗證器的可訪問性檢查。由這個類型規(guī)則推導(dǎo)得到的statT和pTs將用于運(yùn)行時的動態(tài)方法查找。

其中，E::env是類型環(huán)境，它的完整定義如式（14）所示。因此，E是程序、類名和方法本地變量環(huán)境lenv組成的三元組，lenv是變量到其類型的映射。

現(xiàn)在解釋式（13）的推導(dǎo)過程。首先，在當(dāng)前類型環(huán)境E下，計算得到表達(dá)式e的類型，設(shè)為引用類型Ref statT。計算實際參數(shù)對應(yīng)的類型列表，設(shè)為pTs'。使用max_spec找出可訪問的最特定方法，其核心調(diào)用函數(shù)就是accM:

式（15）表示：給定方法簽名，accM得到的從訪問類accCls中可以訪問到的類C的成員方法。filter_map是一個映射過濾函數(shù):filter_map f m=(λa.(case m a of None?None|?x」?if f a x then?x」else None))，因此通過調(diào)用式（12）從（methd P C）中過濾出那些可從訪問類accCls中訪問的C的成員方法。函數(shù)methd如式（16）所示。

其中，inheriteM的定義如式（17）所示，它所使用的各個定義見式（8）、（9）和（10）。

4.5 方法覆蓋和動態(tài)方法查找

由于一個父類引用可以指向一個子類對象，當(dāng)父類引用調(diào)用覆蓋方法時，將執(zhí)行子類中的覆蓋方法，除此之外，該引用仍是一個父類型，它只可調(diào)用父類中的可訪問的方法，不可調(diào)用子類中新定義的方法。如果一個引用指向本類型對象，則調(diào)用本類中的方法。這種在運(yùn)行時的動態(tài)綁定復(fù)雜化了運(yùn)行時的方法查找，因此動態(tài)方法查找涉及引用的靜態(tài)類型、運(yùn)行時的引用對象類型和方法覆蓋。按照2.2節(jié)對方法覆蓋的分析，定義方法覆蓋為一個歸納謂詞，其中Direct規(guī)則給出了條件（1）陳述的覆蓋條件，Indirect規(guī)則對應(yīng)條件（2），給出了缺省訪問修飾符下覆蓋的傳遞性，分別如式（18）和（19）所示。

于是，動態(tài)方法查找dynM的定義如式（20）所示，它表示：如果引用變量的靜態(tài)類型為statT，其所指向?qū)ο蟮念惷麨閐ynC，根據(jù)方法簽名查找得到對應(yīng)的方法。

JLS規(guī)定了方法覆蓋時，子類方法修飾符不得小于被覆蓋方法的訪問修飾符，并且方法的返值類型應(yīng)該更特定于被覆蓋方法，被覆蓋方法不可以是private訪問修飾符，這些條件在程序的良構(gòu)性規(guī)則中規(guī)定，如式（21）所示。

5 定理和證明

下面證明以上定義所滿足的性質(zhì)，從而證明這些定義的正確性。

定理1（method_of_declC）如果mmtd是類C的成員，那么snd mmtd一定聲明在類fst mmtd中。

證明 定理1澄清了mmtd的含義。式（8）中的ImmediateM規(guī)則規(guī)定：如果mmtd的第1個分量就是類C，并且類C中聲明了方法簽名為snd mmtd的方法時，這個歸納定義的判斷結(jié)束，返回布爾值真；若類C中未定義方法簽名為snd mmtd的方法，則類C必須繼承其直接父類D中的該成員，才能返回布爾值真。在這種情況下，P?mmtd method_of D應(yīng)該返回布爾值真。按照這種類的層次關(guān)系遞歸向上判斷，如果最終結(jié)束判斷時，P?mmtd method_of C返回布爾值真，那么一定是按照Immediate規(guī)則，mmtd是某個C的父類中聲明的成員，并且該成員被類C所繼承。于是可知snd mmtd一定聲明在類fst mmtd中。

按照以上分析，在定理證明助手Isabelle/HOL中，定理1的證明使用一個特殊的規(guī)則，即歸納規(guī)則，每個歸納定義的謂詞都暗含了一個歸納規(guī)則。對于式（8），產(chǎn)生的歸納規(guī)則名為method.induct，通過使用歸納證明方法induct，再使用auto，定理1得到證明，因此Isabelle/HOL中的證明腳本為：

包訪問修飾符的成員訪問應(yīng)該滿足一個性質(zhì)：如果mmtd是類C的成員方法，mmtd被聲明為包訪問修飾符，那么該方法的聲明類一定與類C在同一個包下，如定理2所述。

定理2（method_of_Package）

證明 按照式（8）的定義，歸納證明方法induct作用在歸納規(guī)則method.induct上會產(chǎn)生兩個證明子目標(biāo)：（1）對于任意某個確定的m和類C，如果snd m聲明在類C中，并且 fst m=C，在 getAccM(snd m)= Package的前提下，fst(fst m)=fst C成立。證明是相當(dāng)直接的，由 fst m=C，可得 fst(fst m)=fst C。（2）對于任意某個確定的m、類C和類D，如果P?m inheritableM_in(fst C)以及其他假定成立（這些歸納假定省略，當(dāng)前證明不需要這些額外的歸納假定），那么getAccM(snd m_=Package?fst(fst m)=fst C，因此得證，對應(yīng)的Isabelle/HOL證明腳本為：

描述同一主題的的歸納謂詞和普通函數(shù)之間應(yīng)該存在等價關(guān)系，如果能夠證明這種等價性，即這些復(fù)雜的定義滿足期望的性質(zhì)，就能夠充分證明定義的正確性。首先是method_of和methd之間的等價性。從定義上看，歸納謂詞method_of判斷mmtd是否是類C的成員，它用于編譯時的可訪問性檢查。methd P C得到一個偏函數(shù)，該偏函數(shù)將C的成員方法簽名映射到成員方法的聲明類與成員聲明所組成的二元組，它作為運(yùn)行時動態(tài)方法查找的一個輔助函數(shù)。從直觀上理解，這兩者應(yīng)該存在等價關(guān)系：如果(fst m，(sig，snd m))是類C的一個成員，那么類C的成員方法中，簽名是sig的方法就是m。由于methd使用class_rec定義，而class_rec是沿類的繼承層次關(guān)系向上遞歸定義，它以到達(dá)Object類為終止。為了證明methd_of與methd之間的等價性，需要一個限制條件：程序P中類的定義不會出現(xiàn)循環(huán)繼承關(guān)系，ws_prog P定義了這個限制，因此可以證明一個歸納規(guī)則ws_cls_induct。如定理3所述：當(dāng)ws_prog P是布爾真，類C是程序P中的一個類，如果Object是程序P中的一個類，Object滿足某個謂詞p；并且對于程序P中的任意一個非Object類，如果其超類名也滿足該謂詞p，能夠推出類名C滿足謂詞p。那么，類名C滿足謂詞p。

定理3（ws_cls_induct）

于是，method_of和methd之間的等價性陳述如定理4所述。

定理4（member_method）

證明 為了證明這個定理，首先歸納在歸納規(guī)則ws_cls_induct上，產(chǎn)生兩個證明子目標(biāo)。子目標(biāo)1可以直接證明，在子目標(biāo)2上按method_of定義的兩個規(guī)則進(jìn)行cases分析，再次產(chǎn)生兩個子目標(biāo)，它們分別可以得到證明。 □

接下來，證明accM和methd之間的等價性：如果從訪問類accC中可以訪問到類C的簽名為sig的方法為m，那么由methd查找到的類C的簽名為sig的方法一定也是m，并且類C的成員(fst m,(sig,snd m))一定能從accC中訪問到。反之也成立，如定理5所述。

定理5（accM_methd）

證明 由于accM就是基于methd定義的，它僅僅使用了filter_map過濾，因此定理5的證明并不復(fù)雜，它需要使用一個filter_map函數(shù)的性質(zhì)定理(filter_。于是，將filter_map_SomeI作為推出規(guī)則，運(yùn)用auto證明方法定理5得證。 □

最后，證明兩個與動態(tài)方法查找有關(guān)的性質(zhì)。第一個性質(zhì)如定理6所述：如果類C是程序P中的一個類，且滿足ws_prog P，那么當(dāng)靜態(tài)類型和運(yùn)行時對象類名均為C時，即不存在動態(tài)綁定，動態(tài)方法查找等價于一個類名C的靜態(tài)查找。

定理6（dynM_C_C）

證明 式（20）對dynM的定義蘊(yùn)含了一個性質(zhì)dynM_rec，這個性質(zhì)定理是一個等式，使用方法簽名調(diào)用dynM，得到按照dynM的定義所規(guī)定的方法。該性質(zhì)定理的證明首先也歸納在ws_cls_induct上，產(chǎn)生兩個子目標(biāo)；然后在子目標(biāo)1上先后對“Object是否是statC的子類”和“methd P statC sig是否可以查找到方法”執(zhí)行cases分析，在子目標(biāo)2上先后對“dynC是否是statC的子類”和methd P statC sig是否可以查找到方法”進(jìn)行cases分析，證明腳本較為冗長。于是，利用dynM、is_class的定義和dynM_rec性質(zhì)定理，定理6得證。 □

當(dāng)靜態(tài)類型和運(yùn)行時對象類型不相同時，可以證明：如果e表達(dá)式的靜態(tài)類型名為statC，在這個類的成員方法中，簽名為sig的方法映射到statM，dynC是statC子類，滿足ws_prog P，那么一定存在dynM，使得運(yùn)行時動態(tài)方法查找的結(jié)果是dynM，如定理7所述。

定理7（methd_Some_dynM_Some）

證明 首先仍然歸納在歸納規(guī)則ws_cls_induct上，產(chǎn)生兩個證明子目標(biāo)。對于子目標(biāo)1，可以推得statC是Object，于是依據(jù)定理6可知dynM P C C sig=methd P C sig，子目標(biāo)1得證。對于子目標(biāo)2，按引用變量指向本類型對象和引用變量指向子類對象兩種情況進(jìn)行cases分析，再次產(chǎn)生兩個子目標(biāo)，它們都主要使用了定理6中所述的性質(zhì)定理dynM_rec而得到證明。 □

6 結(jié)束語

許多文獻(xiàn)針對Java或者Java虛擬機(jī)進(jìn)行形式建模[2-9]，這些早期的研究工作忽略了訪問控制，但正是因為有這些成果為基礎(chǔ)，使得后來的研究者們能更好、更全面地分析Java編程語言。Klein和Nipkow在Isabelle/HOL中給出了一個形式統(tǒng)一模型[14]，在這個統(tǒng)一模型的支持下，定義了Java子集、Java虛擬機(jī)子集、編譯器和字節(jié)碼驗證器，并證明了編譯的正確性，這個子集不包括訪問控制和數(shù)組，沒有建模動態(tài)綁定。文獻(xiàn)[15]形式化了Android Dalvik虛擬機(jī)子集，但是作者指出其忽略了方法查找的定義，僅說明這是一個標(biāo)準(zhǔn)方法。建立在文獻(xiàn)[4]的基礎(chǔ)上，Schirmer定義了Java訪問控制，特別針對JLS2和其實現(xiàn)Sun jdk1.3以及IBM的Java編譯器之間的一個不一致問題進(jìn)行了討論。在這個形式化定義中，為了與jdk1.3保持一致，方法的可訪問性判斷使用的是一個歸納謂詞，不過正如文章中指出的，Sun將其視為編譯器的一個bug，在其后的版本中已經(jīng)進(jìn)行了修正。Bogdanas等人給出了一個非常完整的Java語義模型[16]，并在文獻(xiàn)[17]中對方法調(diào)用所涉及的動態(tài)方法查找的實現(xiàn)進(jìn)行了詳細(xì)闡述，他們使用的是稱為K框架（K framework）的工具。使用K工具對語言進(jìn)行形式定義非常不同于Isabelle/HOL，鑒于定理證明助手Isabelle/HOL的開發(fā)相對更成熟，我們更傾向于使用Isabelle/HOL進(jìn)行形式化研究。

本文的工作是實現(xiàn)Java子集到Micro-Dalvik虛擬機(jī)編譯正確性研究的一部分[18-19]，即主要研究分析了Java訪問控制機(jī)制，以及可訪問性與繼承、方法覆蓋、動態(tài)綁定之間的交互，并使用Isabelle/HOL2015嚴(yán)格定義了這些語義規(guī)范，通過證明這些定義所滿足的性質(zhì)定理，證明了這些形式化定義的正確性。下一步研究工作將是驗證這個支持訪問控制機(jī)制的Java子集編譯到Micro-Dalvik虛擬機(jī)的語義保持性。

[1]Gosling J,Joy B,Steele G,et al.The Java language specification Java SE 8 edition[M].Boston:Addison Wesley,2015.

[2]Schirmer N.Analysing the Java package/access concepts in Isabelle/HOL[J].Concurrency&Computation Practice& Experience,2004,16(7):689-706.

[3]Alves-Foss J.Formal syntax and semantics of Java[M]. New York:Springer-Verlag.1999.

[4]Von Oheimb D.Analyzing Java in Isabelle/HOL:formalization,type safety and Hoare logic[D].Technology of University at Munchen,2001.

[5]Pusch C.Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL[C]//LNCS 1579:Proceedings of the 5th International Conference on Tools and Algorithms for the Construction andAnalysis of Systems,Amsterdam,Mar 22-28,1999.Berlin,Heidelberg:Springer,1999: 89-103.

[6]Stata R,Abadi M.A type system for Java bytecode subroutines[J].ACM Transactions on Program Language and System,1999,21(1):90-137.

[7]Freund S N,Mitchell J C.A formal framework for the Java bytecode language and verifier[C]//Proceedings of the 14th ACM SIGPLAN Conference on Object-Oriented Programming,Systems,Languages,and Applications,Denver,USA, Nov 1-5,1999.New York:ACM,1999:147-166.

[8]Coglio A,Goldberg A,Qian Zhenyu.Toward a provablycorrect implementation of the JVM bytecode verifier[C]// Proceedings of the 2000 DARPA Information Survivability Conference and Exposition,Hilton Head,South Carolina, Jan 25-27,2000.Washington:IEEE Computer Society,2000: 403-410.

[9]Qian Zhenyu.Standard fixpoint iteration for Java bytecode verification[J].ACM Transaction on Program Language and System,2000,22(4):638-672.

[10]Wrong implementation of definition of override[EB/OL]. (2003-03-20)[2016-05-26].http://bugs.java.com/view_bug. do?bug_id=4485402.

[11]Wrong implementation of inheritance and accessibility of methods[EB/OL].(2002-02-28)[2016-05-26].http://bugs. java.com/view_bug.do?bug_id=4493343.

[12]Nipkow T,Klein G.Concrete semantics with Isabelle/HOL [M].Berlin:Springer-Verlag,2015.

[13]Isabelle[EB/OL].(2016-02-28)[2016-05-26].http://isabelle. in.tum.de/.

[14]Klein G,Nipkow T.A machine-checked model for Java-like language,virtual machine and compiler[J].ACM Transactions on Programming Languages and Systems,2006,28 (4):619-695.

[15]Jeon J,Micinski K K,Foster J S SymDroid:symbolic execution for Dalvik bytecode,CS-TR-5022[R].Department of Computer Science,University of Maryland,College Park, 2012.

[16]Bogdanas D,Grigore U.K-Java:a complete semantics of Java[C]//Proceedings of the 42rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages,Mumbai,India,Jan 12-18,2015.New York:ACM, 2015:445-456.

[17]Bogdanas D.K-Java:runtime semantics for method invocation and object instantiation[J].Pattern Recognition&ImageAnalysis,2014,18(2):300-308.

[18]He Yanxiang,Jiang Nan,Li Qing?an,et al.A machinechecked Micro-Dalvik virtual machine[J].Journal of Soft-ware,2015,26(2):364-379.

[19]Jiang Nan,He Yanxiang,Zhang Xiaotong.Formal verification of mJava compiler targeting Micro-Dalvik virtual machine[J].Chinese Journal of Electronics,2016,44(7):1619-1629.

附中文參考文獻(xiàn)：

[18]何炎祥,江南,李清安,等.一個機(jī)器檢測的Micro-Dalvik虛擬機(jī)模型[J].軟件學(xué)報,2015,26(2):364-379.

[19]江南,何炎祥,張曉瞳.mJava到Micro-Dalvik虛擬機(jī)的編譯驗證[J].電子學(xué)報,2016,44(7):1619-1629.

JIANG Nan was born in 1976.She received the M.S.degree in computer science from Hubei University of Technology in 2003,and she has been a full-time teacher there since 2003.In 2009 she worked as a visiting scholar at Georgia Institute of Technology.Now she is a Ph.D.candidate at Wuhan University,and the member of CCF.Her research interests include formal methods,programming language and trustworthy software,etc.

江南（1976—），女，湖北武漢人，2003年于湖北工學(xué)院計算機(jī)專業(yè)獲得碩士學(xué)位，其后留校任教，2009年于美國佐治亞理工學(xué)院作訪問研究，現(xiàn)在武漢大學(xué)計算機(jī)學(xué)院攻讀博士學(xué)位，CCF會員，主要研究領(lǐng)域為形式化方法，編程語言，可信軟件等。

HE Yanxiang was born in 1952.He received the B.S.degree in mathematics,M.S.and Ph.D.degrees in computer science from Wuhan University in 1975,University of Oregon in 1986 and Wuhan University in 1999,respectively. Now he is a professor and Ph.D.supervisor at Wuhan University,and the senior member of CCF.His research interests include trustworthy software,programming language,software engineering and distribution computing,etc.

何炎祥（1952—），男，湖北應(yīng)城人，1975年、1986年和1999年分別在武漢大學(xué)、美國Oregon大學(xué)和武漢大學(xué)獲得計算數(shù)學(xué)專業(yè)學(xué)士、計算機(jī)專業(yè)碩士和計算機(jī)軟件與理論專業(yè)博士學(xué)位，現(xiàn)為武漢大學(xué)計算機(jī)學(xué)院教授、博士生導(dǎo)師，CCF杰出會員，主要研究領(lǐng)域為可信軟件，編程語言，軟件工程，分布式計算等。

ZHANG Xiaotong was born in 1989.He is an M.S.candidate at Computer School of Wuhan University.His research interests include trustworthy software and programming language,etc.

張曉瞳（1989—），男，湖北武漢人，武漢大學(xué)計算機(jī)學(xué)院碩士研究生，主要研究領(lǐng)域為可信軟件，編程語言等。

LIU Rui was born in 1991.He is an M.S.candidate at Computer School of Wuhan University.His research interests include programming language and Web developing,etc.

劉瑞（1991—），男，湖北武漢人，武漢大學(xué)計算機(jī)學(xué)院碩士研究生，主要研究領(lǐng)域為編程語言，Web開發(fā)等。

SHEN Yunfei was born in 1992.He is an M.S.candidate at Computer School of Wuhan University.His research interests include trustworthy software and programming language,etc.

沈云飛（1992—），男，湖北武漢人，武漢大學(xué)計算機(jī)學(xué)院碩士研究生，主要研究領(lǐng)域為可信軟件，編程語言等。

FormalAnalysis and Proof of Java Security Mechanisms?

JIANG Nan1,2+,HE Yanxiang1,3,ZHANG Xiaotong1,LIU RUI1,SHEN Yunfei1
1.Computer School,Wuhan University,Wuhan 430072,China
2.Computer School,Hubei University of Technology,Wuhan 430068,China
3.State Key Laboratory of Software Engineering,Wuhan University,Wuhan 430072,China
+Corresponding author:E-mail:nanjiang@whu.edu.cn

Java access control is designed to provide security mechanisms on programming language level which prevent the users of an entity declared in a program from depending on unnecessary details of the implementation of this entity with different access modifiers.On the other hand,this design leads to the complexity of the semantics described in the Java language specification,and even the inconsistency between the specification and its implementation.After analyzing the Java access control mechanism which includes the accessibilities of class type,member invariables and member methods and the interactions between accessibility and inheritance,method overriding and dynamic binding,this paper gives strict definitions of these semantics in Isabelle/HOL 2015.Finally,this paper states and proves the properties that these definitions satisfy,which shows that this formalization is correct.

Java access control;dynamic binding;formal analysis;theorem proving

10.3778/j.issn.1673-9418.1606039

A

TP312

*The National Natural Science Foundation of China under Grant No.61373039(國家自然科學(xué)基金).

Received 2016-06,Accepted 2016-09.

CNKI網(wǎng)絡(luò)優(yōu)先出版:2016-09-08,http://www.cnki.net/kcms/detail/11.5602.TP.20160908.1045.014.html