Java安全性機制的形式分析與證明*

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

1.武漢大學 計算機學院，武漢 430072

2.湖北工業大學 計算機學院，武漢 430068

3.武漢大學 軟件工程國家重點實驗室，武漢 430072

Java安全性機制的形式分析與證明*

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

1.武漢大學 計算機學院，武漢 430072

2.湖北工業大學 計算機學院，武漢 430068

3.武漢大學 軟件工程國家重點實驗室，武漢 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訪問控制一方面提供了語言級的安全性機制，這種機制針對程序中所聲明的實體，通過不同的訪問修飾符，向其使用者屏蔽實體的實現細節；另一方面，它也導致了該語言規范的復雜性和實現的不一致性。分析了Java訪問控制機制，包括類型、成員變量和成員方法的可訪問性，以及可訪問性與繼承關系、方法覆蓋、動態綁定之間的交互；然后使用定理證明助手Isabelle/HOL 2015嚴格定義了這些語義規范；最后陳述并證明了這些定義所滿足的性質定理，從而表明該形式化定義的正確性。

Java訪問控制；動態綁定；形式分析；定理證明

1 引言

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

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

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

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

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

2 JLS訪問控制解析

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

2.1 類型的可訪問性

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

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

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

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

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

2.2 成員的可訪問性

JLS規定：一個類類型的成員是可訪問的，當且僅當以下條件成立：

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

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

①在成員的聲明類所在的包范圍內訪問該成員；

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

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

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

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

在圖1（c）中，雖然訪問類B是類A的子類，但是表達式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 受保護成員的可訪問控制

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

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

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

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

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

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

3 程序的定義

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

4種訪問修飾符定義為一個新的數據類型，如式（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）所示。類型包括簡單類型和引用類型，其中簡單類型是布爾類型和整型，引用類型包括類類型和數組類型以及NT。

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

4 可訪問性和動態綁定

4.1 類型的可訪問性

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

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

4.2 類的成員

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

由于類的成員可由其父類繼承得到，判斷是否是類的成員應該是遞歸方式的。不同類中可以定義相同簽名的方法或相同變量名的變量，因此下文形式定義中使用了一個新的結構：由聲明類和聲明本身組成的二元組mmtd::(qname×′m mdecl)。式（8）定義了一個歸納謂詞（inductively defined predicate）method::′m prog?(qname×'m mdecl)?qname?bool。它的定義體現了遞歸性：按照ImmediateM規則，如果mmtd的聲明類是C，且該聲明是類C中一個方法，則mmtd是類C的一個成員方法，即本類中聲明的方法是本類的合法成員方法；繼承得到的成員由歸納規則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）所示，表達的意思是：私有成員不可繼承；受保護的和公有成員可以繼承；對于包訪問修飾符的成員：如果該成員的聲明類是定義在包P中的，則可以繼承。

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

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

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

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

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

4.4 成員的可訪問性

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

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

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

現在解釋式（13）的推導過程。首先，在當前類型環境E下，計算得到表達式e的類型，設為引用類型Ref statT。計算實際參數對應的類型列表，設為pTs'。使用max_spec找出可訪問的最特定方法，其核心調用函數就是accM:

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

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

4.5 方法覆蓋和動態方法查找

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

于是，動態方法查找dynM的定義如式（20）所示，它表示：如果引用變量的靜態類型為statT，其所指向對象的類名為dynC，根據方法簽名查找得到對應的方法。

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

5 定理和證明

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

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

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

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

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

定理2（method_of_Package）

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

描述同一主題的的歸納謂詞和普通函數之間應該存在等價關系，如果能夠證明這種等價性，即這些復雜的定義滿足期望的性質，就能夠充分證明定義的正確性。首先是method_of和methd之間的等價性。從定義上看，歸納謂詞method_of判斷mmtd是否是類C的成員，它用于編譯時的可訪問性檢查。methd P C得到一個偏函數，該偏函數將C的成員方法簽名映射到成員方法的聲明類與成員聲明所組成的二元組，它作為運行時動態方法查找的一個輔助函數。從直觀上理解，這兩者應該存在等價關系：如果(fst m，(sig，snd m))是類C的一個成員，那么類C的成員方法中，簽名是sig的方法就是m。由于methd使用class_rec定義，而class_rec是沿類的繼承層次關系向上遞歸定義，它以到達Object類為終止。為了證明methd_of與methd之間的等價性，需要一個限制條件：程序P中類的定義不會出現循環繼承關系，ws_prog P定義了這個限制，因此可以證明一個歸納規則ws_cls_induct。如定理3所述：當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）

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

接下來，證明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的證明并不復雜，它需要使用一個filter_map函數的性質定理(filter_。于是，將filter_map_SomeI作為推出規則，運用auto證明方法定理5得證。 □

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

定理6（dynM_C_C）

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

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

定理7（methd_Some_dynM_Some）

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

6 結束語

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

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

[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.

附中文參考文獻：

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

[19]江南,何炎祥,張曉瞳.mJava到Micro-Dalvik虛擬機的編譯驗證[J].電子學報,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年于湖北工學院計算機專業獲得碩士學位，其后留校任教，2009年于美國佐治亞理工學院作訪問研究，現在武漢大學計算機學院攻讀博士學位，CCF會員，主要研究領域為形式化方法，編程語言，可信軟件等。

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—），男，湖北應城人，1975年、1986年和1999年分別在武漢大學、美國Oregon大學和武漢大學獲得計算數學專業學士、計算機專業碩士和計算機軟件與理論專業博士學位，現為武漢大學計算機學院教授、博士生導師，CCF杰出會員，主要研究領域為可信軟件，編程語言，軟件工程，分布式計算等。

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—），男，湖北武漢人，武漢大學計算機學院碩士研究生，主要研究領域為可信軟件，編程語言等。

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—），男，湖北武漢人，武漢大學計算機學院碩士研究生，主要研究領域為編程語言，Web開發等。

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—），男，湖北武漢人，武漢大學計算機學院碩士研究生，主要研究領域為可信軟件，編程語言等。

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(國家自然科學基金).

Received 2016-06,Accepted 2016-09.

CNKI網絡優先出版:2016-09-08,http://www.cnki.net/kcms/detail/11.5602.TP.20160908.1045.014.html