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

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

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

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

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

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

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

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

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

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

Java訪問(wèn)控制；動(dòng)態(tài)綁定；形式分析；定理證明

1 引言

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

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

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

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

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

2 JLS訪問(wèn)控制解析

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

2.1 類(lèi)型的可訪問(wèn)性

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

（1）一個(gè)類(lèi)若聲明為公有訪問(wèn)，那么該類(lèi)類(lèi)型可以被所有代碼訪問(wèn)；

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

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

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

2.2 成員的可訪問(wèn)性

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

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

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

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

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

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

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

在圖1（b）中，由于訪問(wèn)類(lèi)B與類(lèi)A的聲明在不同包中，且B不是類(lèi)A的子類(lèi)，因此a.i編譯報(bào)錯(cuò)。

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

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

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

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

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

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

（2）方法N是缺省訪問(wèn)時(shí)，M覆蓋了類(lèi)C中聲明的方法O，并且O覆蓋了N。

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

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

3 程序的定義

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

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

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

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

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

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

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

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

4 可訪問(wèn)性和動(dòng)態(tài)綁定

4.1 類(lèi)型的可訪問(wèn)性

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

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

4.2 類(lèi)的成員

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

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

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

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

（3）類(lèi)型D對(duì)于類(lèi)型C是可訪問(wèn)的(P?Ref (Class D)acc_in(fst C))。

那么，mmtd是C的成員。

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

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

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

4.3 成員訪問(wèn)修飾符的限制條件

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

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

4.4 成員的可訪問(wèn)性

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

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

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

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

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

其中，inheriteM的定義如式（17）所示，它所使用的各個(gè)定義見(jiàn)式（8）、（9）和（10）。

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

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

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

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

5 定理和證明

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

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

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

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

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

定理2（method_of_Package）

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

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

定理3（ws_cls_induct）

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

定理4（member_method）

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

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

定理5（accM_methd）

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

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

定理6（dynM_C_C）

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

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

定理7（methd_Some_dynM_Some）

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

6 結(jié)束語(yǔ)

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

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

[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]何炎祥,江南,李清安,等.一個(gè)機(jī)器檢測(cè)的Micro-Dalvik虛擬機(jī)模型[J].軟件學(xué)報(bào),2015,26(2):364-379.

[19]江南,何炎祥,張曉瞳.mJava到Micro-Dalvik虛擬機(jī)的編譯驗(yàn)證[J].電子學(xué)報(bào),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ì)算機(jī)專業(yè)獲得碩士學(xué)位，其后留校任教，2009年于美國(guó)佐治亞理工學(xué)院作訪問(wèn)研究，現(xiàn)在武漢大學(xué)計(jì)算機(jī)學(xué)院攻讀博士學(xué)位，CCF會(huì)員，主要研究領(lǐng)域?yàn)樾问交椒?，編程語(yǔ)言，可信軟件等。

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é)、美國(guó)Oregon大學(xué)和武漢大學(xué)獲得計(jì)算數(shù)學(xué)專業(yè)學(xué)士、計(jì)算機(jī)專業(yè)碩士和計(jì)算機(jī)軟件與理論專業(yè)博士學(xué)位，現(xiàn)為武漢大學(xué)計(jì)算機(jī)學(xué)院教授、博士生導(dǎo)師，CCF杰出會(huì)員，主要研究領(lǐng)域?yàn)榭尚跑浖幊陶Z(yǔ)言，軟件工程，分布式計(jì)算等。

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ì)算機(jī)學(xué)院碩士研究生，主要研究領(lǐng)域?yàn)榭尚跑浖?，編程語(yǔ)言等。

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ì)算機(jī)學(xué)院碩士研究生，主要研究領(lǐng)域?yàn)榫幊陶Z(yǔ)言，Web開(kāi)發(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ì)算機(jī)學(xué)院碩士研究生，主要研究領(lǐng)域?yàn)榭尚跑浖?，編程語(yǔ)言等。

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(國(guó)家自然科學(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