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

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

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

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

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

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

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

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

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