導(dǎo)航：安全管理網(wǎng)>> 安全論文>> 綜合安全論文>>正文

互斥協(xié)議的安全性分析

文檔作者：趙夢(mèng)龍１唐鄭熠２萬(wàn)良3 韋立４文檔來(lái)源：１．貴州職業(yè)技術(shù)學(xué)院信息技術(shù)系２．福建工程學(xué)院 3．貴州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院４．貴州師范大學(xué)數(shù)學(xué)與計(jì)算機(jī)科學(xué)學(xué)院		點(diǎn) 擊數(shù)：	更新時(shí)間： 2022年04月11日
下載地址：點(diǎn)擊這里	文件大小： 812.40 KB 共3頁(yè)	文檔格式： PDF	下載點(diǎn)數(shù)： 1 點(diǎn)（VIP免費(fèi)）

全屏查看

內(nèi)容預(yù)覽 [文件共3頁(yè)]

本文件共3頁(yè)，如需編輯使用，請(qǐng)下載。

注：預(yù)覽效果可能會(huì)出現(xiàn)部分文字亂碼（如口口口）、內(nèi)容顯示不全等問(wèn)題，下載是正常的。

	文件大?。?12.40 KB 共3頁(yè) 文件格式：PDF 下載點(diǎn)數(shù)：1 點(diǎn)（VIP會(huì)員免費(fèi)）

下一篇：基于LEACH協(xié)議的安全節(jié)能路由算法研究

上一篇：基于匹配策略的安全協(xié)議重構(gòu)分析

文本預(yù)覽

僅提取頁(yè)面文字內(nèi)容，供快速閱讀使用。

收稿日期： ２0１４-0４-１１; 修回日期： ２0１４-06-09　　基金項(xiàng)目： 國(guó)家自然科學(xué)基金資助項(xiàng)目(6１30900);貴州省自然科學(xué)基金資助項(xiàng)目( Ｊ
［２0１１］２3２８);福建工程學(xué)院科研啟動(dòng)基金資助項(xiàng)目(GＹ-Ｚ１3１１２)
作者簡(jiǎn)介：趙夢(mèng)龍(１9８１-),男(通信作者),河南駐馬店人,講師,碩士,主要研究方向?yàn)樾问交椒ā⑿畔踩? ｈａppｙboｙｚ＿ｈａo@１２6．coｍ);
唐鄭熠(１9８４-),男,福建福州人,講師,博士,主要研究方向?yàn)樾问交椒ā⒎?wù)計(jì)算;萬(wàn)良(１9７４-),男,貴州貴陽(yáng)人,副教授,博士(后),主要研究方
向?yàn)樾问交椒?、信息安?韋立(１9８１-),男,廣西都安人,副教授,博士,主要研究方向?yàn)榭捎?jì)算性與計(jì)算復(fù)雜性．
互斥協(xié)議的安全性分析*
趙夢(mèng)龍１, 唐鄭熠２, 萬(wàn)　良3, 韋　立４
(１．貴州職業(yè)技術(shù)學(xué)院信息技術(shù)系, 貴陽(yáng)5500２3; ２．福建工程學(xué)院信息科學(xué)與工程學(xué)院, 福州350１１８; 3．貴
州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院, 貴陽(yáng)5500２3; ４．貴州師范大學(xué)數(shù)學(xué)與計(jì)算機(jī)科學(xué)學(xué)院, 貴陽(yáng)55000４)
摘　要： 安全性和活性是兩大基本的系統(tǒng)屬性,對(duì)于指導(dǎo)系統(tǒng)的設(shè)計(jì)與驗(yàn)證具有重要意義。通過(guò)對(duì)它們?cè)级?
義的形式化梳理,發(fā)現(xiàn)其缺乏對(duì)狀態(tài)序列的具體約束。針對(duì)這一問(wèn)題,使用對(duì)系統(tǒng)動(dòng)作刻畫(huà)更完善的行為時(shí)序
邏輯進(jìn)行了重定義,加入了初始狀態(tài)和轉(zhuǎn)移條件的約束。以此為基礎(chǔ),對(duì)互斥這一并發(fā)系統(tǒng)的典型屬性進(jìn)行了
形式化的分析,由此說(shuō)明如何判斷一個(gè)屬性是否滿足安全性或活性的定義。該技術(shù)為實(shí)現(xiàn)系統(tǒng)性質(zhì)的自動(dòng)推理
與驗(yàn)證提供了形式化基礎(chǔ)。
關(guān)鍵詞： 互斥協(xié)議; 屬性分類; 安全性; 活性; 行為時(shí)序邏輯
中圖分類號(hào)： ＴＰ309．１　　　文獻(xiàn)標(biāo)志碼： Ａ　　　　　文章編號(hào)： １00１-3695(２0１5)05-１４８6-03
ｄoｉ：１0．3969/j．ｉｓｓｎ．１00１-3695．２0１5．05．05２
Sａｆｅｔｙ ａｎａｌｙｓｉｓ oｆ ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ pｒoｔocoｌ
ＺＨＡO Ｍｅｎg-ｌoｎg１, ＴＡＮG Ｚｈｅｎg-ｙｉ２ , ＷＡＮ Ｌｉａｎg3 , ＷＥＩ Ｌｉ４
(１.Ｄｅｐｔ.ｏfＩｎfｏrｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏgy, Gｕｉｚｈｏｕ Ｖｏｃａｔｉｏｎａｌ Ｔｅｃｈｎｏｌｏgy Ｉｎsｔｉｔｕｔｅ, Gｕｉyａｎg 5500２3, Ｃｈｉｎａ; ２.Ｓｃｈｏｏｌ ｏfＩｎfｏrｍａｔｉｏｎ Ｓｃｉｅｎｃｅ ＆
Ｅｎgｉｎｅｅrｉｎg, Ｆｕｊｉａｎ Ｕｎｉvｅrsｉｔy ｏfＴｅｃｈｎｏｌｏgy, Ｆｕｚｈｏｕ 350１１８, Ｃｈｉｎａ; 3.Ｓｃｈｏｏｌ ｏfＣｏｍｐｕｔｅr Ｓｃｉｅｎｃｅ ＆Ｔｅｃｈｎｏｌｏgy, Gｕｉｚｈｏｕ Ｕｎｉvｅrsｉｔy, Gｕｉyａｎg
5500２3, Ｃｈｉｎａ; ４.Ｓｃｈｏｏｌ ｏfＭａｔｈｅｍａｔｉｃs ＆Ｃｏｍｐｕｔｅr Ｓｃｉｅｎｃｅ, Gｕｉｚｈｏｕ Ｎｏrｍａｌ Ｕｎｉvｅrsｉｔy, Gｕｉyａｎg 55000４, Ｃｈｉｎａ)
Ａｂsｔｒａｃｔ: Sａｆｅｔｙ ａｎｄ ｌｉｖｅｎｅｓｓ ａｒｅ ｔoｗ bａｓｉc ｔｙpｅｓ oｆ ｓｙｓｔｅｍ pｒopｅｒｔｙ ａｎｄ ａｒｅ ｖｅｒｙ ｕｓｅｆｕｌ ｆoｒ ｔｈｅ ｄｅｓｉgｎ ａｎｄ ｖｅｒｉｆｉcａｔｉoｎ oｆ ｓｙｓｔｅｍ．
Ｔｈｉｓ pａpｅｒ poｉｎｔｅｄ oｕｔ ｔｈｅ ｄｉｓａｄｖａｎｔａgｅ oｆ ｌａcｋｉｎg ｒｅｓｔｒｉcｔｓ ｔo ｓｔａｔｅ ｓｅｑｕｅｎcｅ ｉｎ ｔｈｅｉｒ oｒｉgｉｎａｌ ｄｅｆｉｎｉｔｉoｎ．Ｆoｒ ｔｈｉｓ pｒobｌｅｍ,
ｉｔ gａｖｅ ｒｅｄｅｆｉｎｉｔｉoｎ bｙ ｔｈｅ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ ｗｈｉcｈ ｗａｓ ｍoｒｅ ｓｕｉｔａbｌｅ ｔo ｄｅｓcｒｉbｅ ｓｙｓｔｅｍ ａcｔｉoｎ．Ｔｈｅ ｎｅｗ ｆoｒｍａｌ ｄｅｆｉｎｉｔｉoｎ
ａｄｄｅｄ ｉｎｉｔｉａｌ ｓｔａｔｅ ａｎｄ coｎｓｔｒａｉｎｔ coｎｄｉｔｉoｎｓ ｆoｒ ｔｒａｎｓｆｅｒ．Oｎ ｔｈｉｓ bａｓｉｓ, ｉｔ ａｎａｌｙｚｅｄ ｔｈｅ ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ ｗｈｉcｈ ｗａｓ ｔｈｅ
ｔｙpｉcａｌ pｒopｅｒｔｙ oｆ coｎcｕｒｒｅｎｔ ｓｙｓｔｅｍ bｙ ｆoｒｍａｌ ｍｅｔｈoｄ．Ｉｔ ａｌｓo ｓｈoｗｓ ｔｈａｔ ｈoｗ ｔo jｕｄgｅ ｗｈｅｔｈｅｒ ａ pｒopｅｒｔｙ ｍｅｅｔｓ ｔｈｅ ｄｅｆｉｎｉｔｉoｎ
oｆ ｓａｆｅｔｙ oｒ ｌｉｖｅｎｅｓｓ．Ｔｈｉｓ ｔｅcｈｎoｌogｙ pｒoｖｉｄｅｄ ｔｈｅ ｆoｒｍａｌ bａｓｉc ｆoｒ ｔｈｅ ａｕｔoｍａｔｉc ｒｅａｓoｎｉｎg ａｎｄ ｖｅｒｉｆｉcａｔｉoｎ oｆ ｓｙｓｔｅｍ pｒopｅｒｔｙ．
Ｋｅy ｗｏｒｄs: ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ pｒoｔocoｌ; cｌａｓｓｉｆｉcａｔｉoｎ oｆ pｒopｅｒｔｉｅｓ; ｓａｆｅｔｙ; ｌｉｖｅｎｅｓｓ; ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ
O　引言
在操作系統(tǒng)中,為了保證程序最終執(zhí)行結(jié)果的正確性,必
須對(duì)并發(fā)執(zhí)行的各進(jìn)程進(jìn)行制約,以控制它們的執(zhí)行速度和對(duì)
資源的競(jìng)爭(zhēng)［１］ 。進(jìn)程之間的間接制約在操作系統(tǒng)中通常叫互
斥,互斥是系統(tǒng)設(shè)計(jì)的關(guān)鍵問(wèn)題之一［２］ ,它保證了相互沖突的
并發(fā)進(jìn)程可以共享資源。本文介紹了安全性與活性的形式化
定義,并針對(duì)其對(duì)狀態(tài)序列沒(méi)有作具體約束的不足,在行為時(shí)
序邏輯中對(duì)其進(jìn)行了重定義。根據(jù)安全性和活性的形式化定
義,對(duì)互斥協(xié)議的安全性進(jìn)行了形式化的分析,證明了互斥協(xié)
議是安全性而不是活性。
1　安全性與活性介紹
１9７７ 年,美國(guó)科學(xué)家Ｌａｍpoｒｔ 在驗(yàn)證多線程程序正確性的
過(guò)程中,最早提出了將系統(tǒng)的性質(zhì)分為安全性和活性兩類,并
給出了它們的非形式化定義:
ａ)安全性:規(guī)定一些行為不會(huì)在系統(tǒng)中發(fā)生。
b)活性:規(guī)定一些行為必須在系統(tǒng)中發(fā)生。
2　安全性與活性的形式化定義
在１9８４ 年,Ｌａｍpoｒｔ 第一次對(duì)安全性進(jìn)行了形式化的定
義,隨后Ａｌpｅｒｎ 和Scｈｎｅｉｄｅｒ 又進(jìn)一步給出了活性的形式化定
義。Ｌａｍpoｒｔ ［3］ 是行為時(shí)序邏輯( ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ) 的創(chuàng)
立者,而安全性和活性的定義主要也是由他提出或啟發(fā)的,其
中的很多概念都被他加入到后來(lái)的行為時(shí)序邏輯當(dāng)中。這使
得安全性和活性能夠方便地使用行為時(shí)序邏輯進(jìn)行定義。因
此下面首先介紹安全性和活性的原始定義,然后再以行為時(shí)序
邏輯對(duì)它們進(jìn)行更精確的定義。
2．1　原始定義
系統(tǒng)的一次運(yùn)行用系統(tǒng)狀態(tài)的無(wú)限序列來(lái)表示:
$1 s0 s１ s２
狀態(tài)之間的轉(zhuǎn)移是由于系統(tǒng)執(zhí)行了某個(gè)行為而發(fā)生的。
第3２ 卷第5 期
２0１5 年5 月　
計(jì)算機(jī)應(yīng)用研究
Ａppｌｉcａｔｉoｎ Ｒｅｓｅａｒcｈ oｆ Coｍpｕｔｅｒｓ
Ｖoｌ．3２ Ｎo．5
Ｍａｙ ２0１5
對(duì)于一次不可終止的運(yùn)行,狀態(tài)序列顯然是無(wú)限的;而對(duì)于一
次可終止的運(yùn)行,可以通過(guò)不斷地重復(fù)序列中的最后一個(gè)狀態(tài)
使其成為無(wú)限序列［４］ 。
同時(shí),$［ｉ］ 1 sｉ,$［..ｉ］ 1 s0 s１ s２ sｉ －１ ,$［ ｉ..］ 1 sｉ sｉ ＋１
sｉ ＋２ 。對(duì)于兩個(gè)運(yùn)轉(zhuǎn)α1 s0 s１ s２ sｉ －１ , β 1 sｉ ＋１ sｉ ＋２ sｉ ＋3 ,
αβ1 s0 s１ s２ sｉ －１ sｉ ＋１ sｉ ＋２ sｉ ＋3 。
一個(gè)屬性被看做是運(yùn)轉(zhuǎn)的集合,其中所包含的元素是滿足
該屬性的運(yùn)轉(zhuǎn)［5］ 。如果說(shuō)系統(tǒng)滿足一個(gè)屬性,那么該系統(tǒng)所
有可能的運(yùn)轉(zhuǎn)都包含在屬性所描述的集合中。
定義１　屬性(pｒopｅｒｔｙ) ［6］ 。一個(gè)屬性Ｐ 被看做是所有符
合滿足該屬性的運(yùn)轉(zhuǎn)的集合,一個(gè)運(yùn)轉(zhuǎn)滿足Ｐ 等價(jià)于該運(yùn)轉(zhuǎn)
屬于Ｐ 所表示的集合,即α(Ｐ$｜＝Ｐ。
用Ｓ 表示所有系統(tǒng)狀態(tài)的集合;用Ｓ*表示所有系統(tǒng)狀態(tài)
有限序列的集合,系統(tǒng)狀態(tài)的有限序列用來(lái)表示系統(tǒng)一次運(yùn)行
中的部分時(shí)刻;用Ｓw 表示所有系統(tǒng)狀態(tài)無(wú)限序列的集合,系統(tǒng)
狀態(tài)的無(wú)限序列用來(lái)表示系統(tǒng)一次運(yùn)行。對(duì)于有限運(yùn)轉(zhuǎn)$(
Ｓ*,｜$｜表示它的長(zhǎng)度。
安全性的定義是一些“ 壞的事情” 不會(huì)發(fā)生,因此如果屬
性Ｐ 是一個(gè)安全性,那么當(dāng)一個(gè)運(yùn)轉(zhuǎn)不滿足屬性Ｐ 的約束時(shí),
那么在運(yùn)轉(zhuǎn)中的某些點(diǎn)上發(fā)生了“壞的事情”。“ 壞的事情” 一
旦發(fā)生就不可補(bǔ)救,因?yàn)榘踩砸蟮氖恰?壞的事情” 永遠(yuǎn)都
不會(huì)發(fā)生。
定義２　安全性( ｓａｆｅｔｙ) ［5］ 。屬性Ｐ 是一個(gè)安全性,當(dāng)且
僅當(dāng)($:$(Ｓw:$｜≠Ｐ  (ｉ: ｉ≥0: (β: β(Ｓw: $［..
ｉ］β｜≠Ｐ)))。
安全性的含義是:安全性Ｐ 中的所有運(yùn)轉(zhuǎn)的任意前綴都
可以被擴(kuò)展為一個(gè)或多個(gè)屬于Ｐ 的無(wú)限運(yùn)轉(zhuǎn)。這個(gè)定義并沒(méi)
有對(duì)“壞的事情” 作出具體限制,但它一定是一個(gè)獨(dú)立的原子
行為,因?yàn)橐坏┮粋€(gè)運(yùn)轉(zhuǎn)中出現(xiàn)了“壞的事情”,那么一定是在
一個(gè)可確認(rèn)的點(diǎn)發(fā)生的。
活性的定義是在系統(tǒng)運(yùn)行的過(guò)程中,“ 好的事情” 最終會(huì)
發(fā)生?；钚砸笙到y(tǒng)運(yùn)行到任何時(shí)刻都存在著發(fā)生“ 好的事
情”的可能,無(wú)論過(guò)去“ 好的事情” 是否發(fā)生,至少要存在未來(lái)
發(fā)生的可能。
定義3　活性( ｌｉｖｅｎｅｓｓ) ［5］ 。屬性Ｐ 是一個(gè)活性,當(dāng)且僅
當(dāng)(α: α(Ｓ*: (β: β(Ｓw: αβ｜＝Ｐ))。
活性的含義是:系統(tǒng)中的任意有限狀態(tài)序列都可以被擴(kuò)展
為一個(gè)或多個(gè)屬于Ｐ 的無(wú)限序列。這個(gè)定義同樣沒(méi)有對(duì)“ 好
的事情”作出具體的規(guī)定,甚至沒(méi)有限制它必須是一個(gè)獨(dú)立的
原子行為。但只要求“好的事情”最終會(huì)發(fā)生,但不是一直( ａｌｗａｙｓ)
發(fā)生。
2．2　基于行為時(shí)序邏輯的形式化定義
在安全性與活性的原始定義中,對(duì)于無(wú)限序列集合Ｓw 和
有限序列集合Ｓ*并沒(méi)有作出具體的約束。然而一個(gè)系統(tǒng)的運(yùn)
行并不是隨意,系統(tǒng)的初始狀態(tài)和狀態(tài)之間的轉(zhuǎn)移是存在著限
制的［6］ 。因此, 本文在行為時(shí)序邏輯中對(duì)其進(jìn)行更嚴(yán)格的
定義。
下面首先簡(jiǎn)要介紹一些ＴＬＡ 中的定義［７ ～9］ 。
定義４　行為( ａcｔｉoｎ)。由變量、原本變量及常量符號(hào)組
成的布爾表達(dá)式。變量與當(dāng)前狀態(tài)相關(guān),原本變量與下一狀態(tài)
相關(guān)。
定義5　啞步(ｓｔｕｔｔｅｒｉｎg ｓｔｅpｓ)。啞步是一種特殊的行為,
在該行為發(fā)生后,系統(tǒng)中所有變量的值都保持不變。
定義6　標(biāo)記轉(zhuǎn)移系統(tǒng):一個(gè)標(biāo)記轉(zhuǎn)移系統(tǒng)T＝(Ｓ, Ｉ, ,
%),其中:
ａ)系統(tǒng)中的所有變量的一次有效賦值稱為一個(gè)狀態(tài)s,所
有的狀態(tài)(即所有可能的賦值)構(gòu)成狀態(tài)集合,記為Ｓ。
b)初始狀態(tài)ＩＳ。
c) 是所有行為構(gòu)成的集合。
ｄ)%Ｓ × ×Ｓ。
定義７　運(yùn)轉(zhuǎn)(ｒｕｎ)。運(yùn)轉(zhuǎn)是由無(wú)限或有限多個(gè)狀態(tài)組成
的序列,可以被看做是系統(tǒng)的一次運(yùn)行:$1 s0
Ａ
→
0 s１
Ａ
→
１
s２ ,其中s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。由于ＴＬＡ 引入了啞
步,有限長(zhǎng)的運(yùn)轉(zhuǎn)可以通過(guò)啞步擴(kuò)展為無(wú)限長(zhǎng)的運(yùn)轉(zhuǎn)。此外,
本文定義:$［ ｉ］ 1 sｉ,$［..ｉ］ 1 s0
Ａ
→
0 s１
Ａ
→
１ s２
Ａｉ
→
－１ sｉ －１ ,
(［ｉ..］ 1sｉ
Ａ
→
ｉ sｉ ＋１
Ａｉ
→
＋１ sｉ ＋２ 。
下面是在行為時(shí)序邏輯中重新定義表示系統(tǒng)運(yùn)行集合的
符號(hào):
定義８　系統(tǒng)運(yùn)行的集合。對(duì)于一個(gè)標(biāo)記轉(zhuǎn)移系統(tǒng)T＝
(Ｓ,Ｉ, ,%),一個(gè)有限的運(yùn)轉(zhuǎn)$表示系統(tǒng)的一次未終止的運(yùn)
行,而無(wú)限的運(yùn)轉(zhuǎn)$表示系統(tǒng)的一次運(yùn)行,有如下標(biāo)記:
ａ)T*
$ 表示滿足標(biāo)記轉(zhuǎn)移系統(tǒng)T 的有限運(yùn)轉(zhuǎn)的集合,其中
s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。
b)Tw
$ 表示滿足標(biāo)記轉(zhuǎn)移系統(tǒng)T 的無(wú)限運(yùn)轉(zhuǎn)的集合,其中
s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。
c)(Ｓ, )*
$ 表示有限運(yùn)轉(zhuǎn)的集合,其中Ａｉ( ,( sｉ, Ａｉ,
sｉ ＋１ )(%。
ｄ)(Ｓ, ) w
$ 表示無(wú)限運(yùn)轉(zhuǎn)的集合,其中Ａｉ( ,( sｉ, Ａｉ,
sｉ ＋１ )(%。
T*
$ 和Tw
$ 表示系統(tǒng)從初始狀態(tài)開(kāi)始的運(yùn)行,而( Ｓ, )*
$ 和
(Ｓ, ) w
$ 表示系統(tǒng)從任意狀態(tài)開(kāi)始的運(yùn)行。
定義9　安全性。屬性Ｐ 是一個(gè)安全性,當(dāng)且僅當(dāng)($:
$(Tw
$: $｜≠Ｐ  (ｉ: ｉ≥0: (β: β(( Ｓ, ) w
$: $［..ｉ］ β｜≠
Ｐ)))。
定義１0　活性。屬性Ｐ 是一個(gè)活性,當(dāng)且僅當(dāng)(α: α(
T*
$: (β: β((Ｓ, ) w
$: αβ｜＝Ｐ))。
新的定義是為安全性和活性加入了初始狀態(tài)和狀態(tài)間轉(zhuǎn)
移關(guān)系的限制,將描述的運(yùn)轉(zhuǎn)限定在符合系統(tǒng)基本要求的范圍
內(nèi),因?yàn)橹挥羞@樣的運(yùn)轉(zhuǎn)對(duì)于系統(tǒng)而言才有意義。
根據(jù)安全性的定義可知,如果一個(gè)屬性Ｐ 不是安全性,那
么就是滿足^($·$(Tw
$: $｜≠Ｐ (ｉ: ｉ≥0: (β: β(
(Ｓ, ) w
$: $［..ｉ］β｜≠Ｐ))),即:$·$(Ｓw: ($｜≠Ｐ)∧(ｉ:
ｉ≥0: β: β(Ｓw: $［..ｉ］β｜＝Ｐ)。
根據(jù)活性的定義可知,如果一個(gè)屬性Ｐ 不是活性,那么就
是滿足^(α: α(T*
$: (β: β((Ｓ, ) w
$: αβ｜＝Ｐ)),即α:
α(T*
$: (β: β((Ｓ, ) w
$: αβ｜≠Ｐ)。
3　互斥協(xié)議的安全性
3．1　互斥概述
現(xiàn)代計(jì)算機(jī)系統(tǒng)的中心方案包括多道程序設(shè)計(jì)、多處理和
分布式處理,這些方案的基礎(chǔ)以及操作系統(tǒng)設(shè)計(jì)的基礎(chǔ)是并發(fā)
第5 期 趙夢(mèng)龍,等：互斥協(xié)議的安全性分析 ·１４?。福贰?#183;　
　　
的,并發(fā)進(jìn)程可以按照多種方式進(jìn)行交互。系統(tǒng)中的眾多交互
進(jìn)程可能需要競(jìng)爭(zhēng)使用資源,如對(duì)Ｉ/O 設(shè)備的訪問(wèn)、主存中的
一塊空間或者一個(gè)文件等。此類交互中產(chǎn)生的重要問(wèn)題就是
互斥。
互斥的定義通常為［１0］ :一組并發(fā)進(jìn)程中的一個(gè)或多個(gè)程
序段,因共享某一公有資源而導(dǎo)致它們必須以一個(gè)不允許交叉
執(zhí)行的單位執(zhí)行。也就是說(shuō),不允許兩個(gè)以上的共享該資源的
并發(fā)進(jìn)程同時(shí)進(jìn)入臨界區(qū)。互斥技術(shù)不但可以用于解決諸如
共享資源競(jìng)爭(zhēng)等沖突,還可以用于進(jìn)程間同步,使它們可以協(xié)
調(diào)合作［１１］ ,例如著名生產(chǎn)者/消費(fèi)者問(wèn)題:一個(gè)進(jìn)程向緩沖中
寫(xiě)入/添加數(shù)據(jù),另外一個(gè)或若干個(gè)進(jìn)程從緩沖中讀取數(shù)據(jù)。
3．2　安全性分析
假設(shè)一個(gè)系統(tǒng)Ｔ 中有兩個(gè)進(jìn)程α和β,以及一個(gè)資源γ,進(jìn)
行如下約定:
ａ)變量x＝0 表示進(jìn)程α沒(méi)有占據(jù)資源γ;
b)變量x＝１ 表示進(jìn)程α占有了資源γ;
c)變量y＝0 表示進(jìn)程β 沒(méi)有占據(jù)資源γ;
ｄ)變量y＝１ 表示進(jìn)程β 占有了資源γ;
ｅ)行為x: ＝0 將變量x 賦值為0,表示進(jìn)程α釋放資源γ;
ｆ)行為x: ＝１ 將變量x 賦值為１,表示進(jìn)程α占據(jù)資源γ;
g)行為y: ＝0 將變量y 賦值為0,表示進(jìn)程β 釋放資源γ;
ｈ)行為y: ＝１ 將變量y 賦值為１,表示進(jìn)程β 占據(jù)資源γ。
則存在圖１ 所示的狀態(tài)轉(zhuǎn)移圖。
假如資源γ是一個(gè)臨界資源,那么就必須遵循互斥協(xié)議:
不允許被兩個(gè)或兩個(gè)以上的進(jìn)程同時(shí)占有資源γ。因此,就要
加入互斥性Ｍ:(x＝y(tǒng))(x＝0)。
互斥性Ｍ可以用下面的狀態(tài)轉(zhuǎn)移圖２ 來(lái)表示。
圖１　系統(tǒng)的Ｔ 狀態(tài)轉(zhuǎn)移圖圖２　互斥性Ｍ的狀態(tài)轉(zhuǎn)移圖
由于狀態(tài)ｑ２ 是系統(tǒng)中唯一不滿足互斥性的狀態(tài),所以可
以把互斥性Ｍ形式化地描述為
Ｍ＝｛$｜($(Tw
$)∧(ｉ≥0: sｉ≠ｑ２ )3
命題１　屬性Ｍ是安全性。
證明　$: $(Tw
$: $｜≠Ｐ (ｉ≥0: sｉ ＝ｑ２ ),取ｊ≥ｉ,
則β: β((Ｓ, ) w
$: $［..ｊ］β｜≠Ｍ。
因此,根據(jù)安全性的定義,屬性Ｍ是安全性。
證畢。
命題２　屬性Ｍ不是活性。
證明　系統(tǒng)中存在圖3 所示的有限運(yùn)轉(zhuǎn)α:
圖3　系統(tǒng)Ｔ 中的一條有限運(yùn)轉(zhuǎn)α
由于sｉ(α: sｉ ＝ｑ２ ,所以β((Ｓ, ) w
$,αβ｜≠Ｐ。
因此,屬性Ｐ 不是活性。
證畢。
由命題１ 和２ 可知,互斥協(xié)議屬于安全性而不是活性。它
只能保證系統(tǒng)不發(fā)生兩個(gè)進(jìn)程同時(shí)使用同一個(gè)臨界資源的情
況,但不能保證某個(gè)進(jìn)程一定能夠獲得一個(gè)臨界資源。
4　結(jié)束語(yǔ)
安全性和活性是兩類最基本的屬性,它們所確保的系統(tǒng)性
質(zhì)是完全不同的。由于對(duì)于安全性和活性的驗(yàn)證使用的是不
同的技術(shù),所以區(qū)分一個(gè)屬性是安全性還是活性是十分必要
的。研究屬性的分類、定義和分析技術(shù),對(duì)于系統(tǒng)的形式化分
析具有重要的意義。后續(xù)的研究可以在本文工作的基礎(chǔ)上,對(duì)
于一些典型的系統(tǒng)屬性進(jìn)行分析,同時(shí)也可以探索安全性和活
性在實(shí)際系統(tǒng)驗(yàn)證中的應(yīng)用新途徑。
參考文獻(xiàn)：
［１］ CＨＥＮ Ｒｕｉ, ＬO(píng)ＮG Sｈｉ-goｎg．Spｅcｉｆｙｉｎg coｎcｕｒｒｅｎｔ pｒogｒａｍ bａｓｅｄ oｎ
ＴＬＡ［C］//Ｐｒoc oｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ｍｅcｈａｎｉcａｌ
Ｄｅｓｉgｎ ａｎｄ Ｐoｗｅｒ Ｅｎgｉｎｅｅｒｉｎg．Ｚｕｒｉcｈ： Ｔｒａｎｓ Ｔｅcｈ Ｐｕbｌｉcａｔｉoｎｓ,
２0１４： ７9８-８0２．
［２］ ＰＡＲＫ Sｕｎg-ｈooｎ, ＫＩＭＹ Ｍ．Ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ ａｌgoｒｉｔｈｍ ｉｎ ｍobｉｌｅ
cｅｌｌｕｌａｒ ｎｅｔｗoｒｋｓ［ C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Ｅｌｅcｔｒｉcａｌ Ｅｎgｉｎｅｅｒｉｎg, ｖoｌ
２１5．２0１3： 695-７0２．
［3］ ＬＡＭＰOＲＴ Ｌ．Ｔｈｅ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ［Ｊ］．ＡCＭＴｒaｎｓ oｎ Ｐｒoｇｒaｍｍｉｎｇ
Ｌaｎｇｕaｇｅｓ aｎｄ Sｙｓｔｅｍｓ, １99４, １ 6(3)：８７２-9２3．
［４］ ＬＩ Ｊｕｎ-ｔａo, ＹＩＵ Ｚｉ-ｙｉ．Oｎ ａcｔｉoｎｓ oｆ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎｓ ［C］//
Ｐｒoc oｆ ｔｈｅ 3ｒｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ａｄｖａｎcｅｄ Coｍpｕｔｅｒ Ｔｈｅoｒｙ
ａｎｄ Ｅｎgｉｎｅｅｒｉｎg．Ｎｅｗ Ｙoｒｋ： ＩＥＥＥ Coｍpｕｔｅｒ Socｉｅｔｙ, ２0１0：
４４７４-４４７７．
［5］ CＨＡＵＤＨＵＲＩ Ｋ, ＤOＬＩGＥＺ Ｄ, ＬＡＭＰOＲＴ Ｌ, ｅｔ ａｌ．Ｖｅｒｉｆｙｉｎg ｓａｆｅｔｙ
pｒopｅｒｔｉｅｓ ｗｉｔｈ ｔｈｅ ＴＬＡ ＋pｒooｆ ｓｙｓｔｅｍ［C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Coｍpｕｔｅｒ
Scｉｅｎcｅ, ｖoｌ 6１７3．Ｂｅｒｌｉｎ：Spｒｉｎgｅｒ,２0１0： １４２-１４８．
［6］ ＭＥＲＺ S．Ｐｒooｆｓ ａｎｄ pｒooｆ cｅｒｔｉｆｉcａｔｉoｎ ｉｎ ｔｈｅ ＴＬＡ ＋pｒooｆ ｓｙｓｔｅｍ
［C］//Ｐｒoc oｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Ｗo(hù)ｒｋｓｈop oｎ Ｐｒooｆ Ｅｘcｈａｎgｅ ｆoｒ
Ｔｈｅoｒｅｍ Ｐｒoｖｉｎg．２0１２： １6-２0．
［７］ 唐鄭熠, 李均濤, 李祥．行為時(shí)序邏輯中公平性的研究與完善
［Ｊ］．計(jì)算機(jī)應(yīng)用研究, ２0１0, 27(5)： １７８８-１７9１．
［８］ COＵSＩＮＥＡＵ Ｄ, ＤOＬＩGＥＺ Ｄ, ＬＡＭＰOＲＴ Ｌ, ｅｔ ａｌ．ＴＬＡ ＋pｒooｆｓ
［C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Coｍpｕｔｅｒ Scｉｅｎcｅ, ｖoｌ ７４36．Ｂｅｒｌｉｎ：Spｒｉｎgｅｒ,
２0１２： １４７-１5４．
［9］ ＢＡＩ Ｊｉｎ-ｓｈａｎ, ＴＡＮG Ｚｈｅｎg-ｙｉ, ＬＩ Ｊｕｎ-ｔａo, ｅｔ ａｌ．Ｌｉｎｅａｒ ｔｉｍｅ pｒopｅｒｔｉｅｓ
ｉｎ ＴＬＡ［ Ｊ］．ＪoｕｒｎaＩ oｆ Coｎｖｅｒｇｅｎcｅ Ｉｎｆoｒｍaｔｉoｎ Ｔｅcｈｎo-
Ｉoｇｙ, ２0１１, 6(１)： ２８４-２８８．
［１0］ ＷＡＮ Ｌｉａｎg, SＨＩ Ｗｅｎ-cｈａｎg．Spｅcｉｆｙｉｎg ａｎｄ cｈｅcｋｉｎg ｎｅｔｗoｒｋ pｒoｔocoｌ
bａｓｅｄ oｎ ＴＬＡ［C］//Ｐｒoc oｆ ｔｈｅ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ａｎｔｉ-
Coｕｎｔｅｒｆｅｉｔｉｎg, Sｅcｕｒｉｔｙ ａｎｄ Ｉｄｅｎｔｉｆｉcａｔｉoｎ．Ｗａｓｈｉｎgｔoｎ ＤC： ＩＥＥＥ
Coｍpｕｔｅｒ Socｉｅｔｙ, ２0１２： １８７-１95．
［１１］ ＺＨＡＮG Ｊｕｎ-ｍｉｎg, ＷＡＮG Ｋoｕ-ｗｕ．Ｔｈｅ ｓａｆｅｔｙ ａｎｄ ｌｉｖｅｎｅｓｓ pｒopｅｒｔｉｅｓ
oｆ ｔｈｅ ｎｅｔｗoｒｋ pｒoｔocoｌ bａｓｅｄ oｎ ＴＬＡ ［C］//Ｐｒoc oｆ ｔｈｅ Ｉｎｔｅｒｎａｔｉoｎａｌ
Coｎｆｅｒｅｎcｅ oｎ Ｉｎｆoｒｍａｔｉoｎ ａｎｄ Coｍｍｕｎｉcａｔｉoｎｓ Ｔｅcｈｎoｌogｉｅｓ．
Sｔｅｖｅｎａgｅ： Ｉｎｓｔｉｔｕｔｉoｎ oｆ Ｅｎgｉｎｅｅｒｉｎg ａｎｄ Ｔｅcｈｎoｌogｙ, ２0１3： ２１８-
２２２．
·１４８８· 計(jì) 算 機(jī) 應(yīng) 用 研 究 　 第3２ 卷

網(wǎng)友評(píng)論 more

綜合安全論文最新內(nèi)容

05-04