Java虛擬機安全性的形式化分析和驗證.pdf

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

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

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

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

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

6、系統(tǒng)通過引入鎖記錄集合和新的類型，在兼容JVML1類型系統(tǒng)的同時，能夠靜態(tài)檢查字節(jié)碼程序的結構化加鎖特性，即：(1)無論方法調用正?；虍惓＝Y束，方法調用過程中程序對某個對象的加鎖次數必須等于對其的解鎖次數；(2)方法調用過程中的任意一點，程序對某個對象的解鎖次數不能超過對其的加鎖次數。JVML2的類型可靠性定理保證類型正確的字節(jié)碼程序不會在運行時出現結構化加鎖錯誤。 類加載器是動態(tài)類加載的核心機制，它在提供較高的程序設計靈活性的

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

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