安全移動資源的語義、類型系統(tǒng)及其代數(shù)性質(zhì)的研究.pdf

1、移動資源演算(MR)是一種用于描述攜帶資源的移動系統(tǒng)及其交互的形式化方法，它隸屬于灰箱演算的一支。灰箱演算由Cardelli提出，最初被稱為移動灰箱演算(MA)，本文將絕大部分由灰箱演算發(fā)展而形成的進程代數(shù)系統(tǒng)稱為類灰箱演算。本文以移動資源演算的一個變體——安全移動資源演算(SR)作為研究對象，從操作語義、類型系統(tǒng)、進程等價性和表達能力等方面對其進行了研究。 首先，本文在分析現(xiàn)有移動資源演算及相關的類灰箱演算(諸如移動灰箱MA，

2、安全灰箱演算SA，盒灰箱BA等)不足的基礎上，提出通過增加協(xié)動作并限制協(xié)動作的實施對象來提高安全性的思想，并以此為指導給出SR的語法和歸約語義。 其次，本文研究了SR的類型問題，提出一套可以解決移動資源演算中存在的進程干擾問題的位置類型系統(tǒng)(L-S)。由于在移動資源演算中引入了灰箱路徑作為能力操作對象的語義，因而進程的干擾問題變得更錯綜復雜，而且原先類灰箱演算干擾問題相關研究成果以及解決方法無法妥善地解決基于灰箱路徑的操作語義所

3、帶來的相關問題，進程在不同層次的灰箱結(jié)構(gòu)中對同一灰箱路徑的訪問無法通過已有的系統(tǒng)得到控制。本文利用對攜有灰箱路徑的能力設定相應的位置類型，進而為攜有相關路徑的進程記錄其訪問目的的類型值，配合特殊的位置類型構(gòu)造，表示位于不同的灰箱層次內(nèi)進程的訪問地點的特性，解決了移動資源演算的巢式干擾問題。L-S系統(tǒng)可以有效地追蹤進程的訪問地點，并支持子類型關系，該系統(tǒng)還可以和傳統(tǒng)的類型屬性，如移動性和線程數(shù)，構(gòu)成復合類型系統(tǒng)。 再次，本文參照L

4、evi研究SA，以及Godskesen研究MR等價性使用的方法，對SR進行了類似的研究。首先引入SR進程的標號動作和固化結(jié)果，用于將進程中可能參與歸約的部分與剩余的部分分開。在標號動作和固化結(jié)果的基礎上，按照進程的歸約特性給出SR基于提交關系的標號轉(zhuǎn)移語義，并逐一分析這些規(guī)則與歸約規(guī)則的對應關系，并證明標號轉(zhuǎn)移語義和歸約語義的等價性。在標號轉(zhuǎn)移語義的基礎上，研究了判定進程觀察互模擬等價的一般方法，得出SR進程的觀察互模擬等價關系與標號互

5、模擬等價關系是同一關系的結(jié)論，并給出SR進程與上下文(含路徑上下文)發(fā)生交互的各種可能，作為判定進程等價的一般性結(jié)論。 此后，本文綜合類型系統(tǒng)和等價性判定的結(jié)論，給出用于判定進程等價的一些代數(shù)定律，同時使用這些定律證明移動資源的線性特征和數(shù)字簽名卡例子在給定條件下的正確性。這些例子不僅示意了等價性定律的具體使用方法，同時也體現(xiàn)了SR較之MR在安全性方面的優(yōu)越性。 最后，本文利用上述等價性定律給出并證明了SR演算翻譯π演算

6、的一個方案，彌補了移動資源演算作為灰箱演算的一個分支，到目前為止尚缺乏對表達能力的研究，有力地說明SR在提高安全性的同時，沒有失去灰箱演算應有的表達能力。本文的主要創(chuàng)新性體現(xiàn)在以下幾個方面。 (一)對利用新增的可供三方同步的協(xié)動作，以及相關的能力參數(shù)加強移動資源演算安全性這一命題進行了研究，提出了移動資源演算的變體SR。通過利用協(xié)動作參數(shù)加強交互雙方的彼此控制，SR在安全控制方面比起MR來有一定優(yōu)勢。同時，對協(xié)動作參數(shù)進行控制后

7、，SR并沒有喪失MR所具有的表達能力。 (二)針對移動資源演算中存在的進程干擾問題給出了支持訪問位置類型特性的類型系統(tǒng)L-S。該系統(tǒng)通過區(qū)分不同灰箱層次(即不同灰箱路徑)下進程的位置類型，可以精確地避免不同的進程對同一訪問地點產(chǎn)生非樸素干擾的現(xiàn)象，并支持子類型關系?？紤]到L-S系統(tǒng)的獨立性，L-S在設計時還考慮到和傳統(tǒng)類型屬性整合的可能性，并給出了復合類型系統(tǒng)的框架。 (三)有別于Gordon和Cardelli基于硬化關

8、系的上下文等價方法，本文借鑒Levi和Sangiorgi基于固化結(jié)果和提交關系所引入的標號互模擬等價性，給出了SR中判定進程等價性的一般性方法；同時結(jié)合位置類型系統(tǒng)，證明了在給出的類型環(huán)境Г下SR進程的等價性定律。 (四)本文借助自行推導的SR進程的等價性定律完成對π演算翻譯的代數(shù)方法證明，較之Zimmer的證明方法來得更為簡明。另外，本文將前人對移動資源演算以及相關的類灰箱演算的語義、等價性、表達能力等方面的研究成果結(jié)合本文S