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

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

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

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

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

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

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

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

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