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

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

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

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

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

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

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

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

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