Java虛擬機(jī)安全性的形式化分析和驗(yàn)證.pdf

1、本文提出了一種描述Java虛擬機(jī)語(yǔ)義的形式化模型，該模型包含Java虛擬機(jī)安全體系結(jié)構(gòu)中兩個(gè)最重要的特性：字節(jié)碼驗(yàn)證和動(dòng)態(tài)類加載。具體地，本文定義了Java虛擬機(jī)語(yǔ)言(JVML)的一個(gè)子集，給出了該子集的類型系統(tǒng)和操作語(yǔ)義，并根據(jù)操作語(yǔ)義證明了該類型系統(tǒng)的可靠性。因此，該類型系統(tǒng)可保證一個(gè)類型正確的字節(jié)碼程序不會(huì)在運(yùn)行時(shí)出現(xiàn)類型錯(cuò)誤。上述工作的形式化是在交互式定理證明器HOL系統(tǒng)中完成的。本文認(rèn)為，對(duì)于形式語(yǔ)義而言，采用一種機(jī)械化驗(yàn)證工

2、具對(duì)于保證定義的一致性、保證形式化過(guò)程的正確性是十分重要的。為此，本文還分析了HOL系統(tǒng)的實(shí)現(xiàn)，并對(duì)其進(jìn)行了擴(kuò)充。 在字節(jié)碼驗(yàn)證的形式化過(guò)程中，本文分三個(gè)階段研究了三個(gè)復(fù)雜的靜態(tài)分析問(wèn)題：對(duì)象初始化、子例程和鎖原語(yǔ)。 第一階段，本文通過(guò)定義JVML的一個(gè)子集JVML0，來(lái)研究字節(jié)碼的對(duì)象初始化特性。本文證明了Java虛擬機(jī)規(guī)范對(duì)于別名分析算法的約束過(guò)強(qiáng)，這個(gè)結(jié)論表明，當(dāng)前Sun的字節(jié)碼驗(yàn)證程序包含了大量不必要的類型檢查。

3、這里，JVML0的類型系統(tǒng)能夠保證字節(jié)碼程序不會(huì)使用未初始化的對(duì)象。 第二階段，本文將JVML0擴(kuò)充為JVML1，以包含子例程。在類型規(guī)則中，本文引入了一個(gè)跟蹤子例程調(diào)用過(guò)程的活動(dòng)記錄棧，用于記錄程序當(dāng)前所處的調(diào)用位置和子例程訪問(wèn)的局部變量集合。本文為活動(dòng)記錄棧定義了一種偏序關(guān)系，它不允許字節(jié)碼程序遞歸調(diào)用子例程(這種約束與Java虛擬機(jī)規(guī)范是一致的)。實(shí)際上，遞歸調(diào)用不僅增加了Java虛擬機(jī)的復(fù)雜性，而且也沒有為編譯Java程

4、序提供多少幫助。與Java虛擬機(jī)規(guī)范相比，JVML1的類型系統(tǒng)具有更弱的類型約束。例如，通過(guò)在對(duì)象的類型中引入表示子例程調(diào)用地址的信息，本文提出一種與Java虛擬機(jī)規(guī)范不同的別名分析方法。該方法不僅更加簡(jiǎn)單有效，而且能夠接受更多的類型正確的字節(jié)碼程序。Java虛擬機(jī)規(guī)范不允許aloadx指令使用未初始化的局部變量x，而JVML1的類型系統(tǒng)取消了這種約束；Java虛擬機(jī)規(guī)范要求每個(gè)子例程只能有一個(gè)ret指令，而JVML1的類型系統(tǒng)允許子例

5、程有任意個(gè)ret指令。盡管本文減弱了某些類型約束，但是并沒有對(duì)字節(jié)碼程序的類型安全造成任何影響。JVML1的類型可靠性定理保證：(1)子例程能夠以基于調(diào)用棧的方式返回到正確的調(diào)用地址；(2)子例程能夠正確處理別名對(duì)象。 第三階段，本文將JVML1擴(kuò)充為JVML2，以包含鎖原語(yǔ)。JVML2的類型系統(tǒng)是對(duì)當(dāng)前Sun的字節(jié)碼驗(yàn)證的一種擴(kuò)充，因?yàn)镾un的虛擬機(jī)實(shí)現(xiàn)并不對(duì)字節(jié)碼程序進(jìn)行靜態(tài)檢查，來(lái)判斷其是否正確使用了鎖原語(yǔ)。JVML2類型

6、系統(tǒng)通過(guò)引入鎖記錄集合和新的類型，在兼容JVML1類型系統(tǒng)的同時(shí)，能夠靜態(tài)檢查字節(jié)碼程序的結(jié)構(gòu)化加鎖特性，即：(1)無(wú)論方法調(diào)用正常或異常結(jié)束，方法調(diào)用過(guò)程中程序?qū)δ硞€(gè)對(duì)象的加鎖次數(shù)必須等于對(duì)其的解鎖次數(shù)；(2)方法調(diào)用過(guò)程中的任意一點(diǎn)，程序?qū)δ硞€(gè)對(duì)象的解鎖次數(shù)不能超過(guò)對(duì)其的加鎖次數(shù)。JVML2的類型可靠性定理保證類型正確的字節(jié)碼程序不會(huì)在運(yùn)行時(shí)出現(xiàn)結(jié)構(gòu)化加鎖錯(cuò)誤。 類加載器是動(dòng)態(tài)類加載的核心機(jī)制，它在提供較高的程序設(shè)計(jì)靈活性的

7、同時(shí)，還可用于動(dòng)態(tài)隔離不同的應(yīng)用程序。但是，早期的Java版本(JDK1.0和1.1)中，動(dòng)態(tài)類加載存在著一種稱為Saraswat類型欺騙的設(shè)計(jì)錯(cuò)誤。為了修正這種錯(cuò)誤，JDK1.2引入了一種類加載約束機(jī)制。在動(dòng)態(tài)類加載的形式化過(guò)程中，本文的模型不僅包含JDK1.2提出的這種機(jī)制，而且還指出了存在于JDK1.2和JDK1.3中的其它形式的類型欺騙，并為此提出一種稱為子類型約束的解決方法。該方法引入了一個(gè)稱為類型合并集合的新的數(shù)據(jù)結(jié)構(gòu)，并據(jù)

8、此在類型規(guī)則中定義了相應(yīng)的子類型約束條件。為了證明該類型系統(tǒng)的可靠性，本文提出了一種為一個(gè)值指派類型的新方法。另外，本文還對(duì)類文件結(jié)構(gòu)進(jìn)行了形式化，并定義了其上的相應(yīng)操作，使得本文的模型更加符合Java虛擬機(jī)規(guī)范。通過(guò)形式化建模和可靠性證明，本文還分析了字節(jié)碼驗(yàn)證和動(dòng)態(tài)類加載之間的關(guān)系。 綜上所述，本文的主要貢獻(xiàn)是：(1)為Java虛擬機(jī)提供了一種嚴(yán)格、可靠和全面的形式化定義；(2)為研究Java虛擬機(jī)的其它特性提供了一個(gè)統(tǒng)一的