基于隨機(jī)模型檢驗(yàn)的社交網(wǎng)絡(luò)隱私保護(hù)研究

劉 陽(yáng)，高世國(guó)

（南京財(cái)經(jīng)大學(xué)信息工程學(xué)院，南京 210046）

0 概述

隨著互聯(lián)網(wǎng)和通信技術(shù)的快速發(fā)展，在線社交網(wǎng)絡(luò)（Online Social Network，OSN）已成為人們信息交流的重要媒介［1］，但由于在線社交網(wǎng)絡(luò)用戶的不斷增長(zhǎng)［2］，隱私泄露問(wèn)題也愈發(fā)嚴(yán)重。2018 年，美國(guó)社交網(wǎng)絡(luò)科技公司Facebook 就因用戶隱私泄露問(wèn)題被處以50 億美金的罰款［3］，社交網(wǎng)絡(luò)的安全隱私問(wèn)題日益突出，引起了社會(huì)公共的廣泛關(guān)注。目前，在線社交網(wǎng)絡(luò)隱私策略主要存在隱私設(shè)置與用戶隱私需求不匹配且缺乏靈活性與一致性的問(wèn)題。對(duì)于在線社交網(wǎng)絡(luò)的隱私設(shè)置與用戶隱私需求不匹配問(wèn)題而言［4］，這主要是由于社交網(wǎng)絡(luò)運(yùn)行環(huán)境的不確定性所造成，在線社交網(wǎng)絡(luò)的終端用戶可以是移動(dòng)終端、Web 終端甚至物聯(lián)網(wǎng)設(shè)備終端，各個(gè)終端依靠自身通信協(xié)議進(jìn)行數(shù)據(jù)轉(zhuǎn)發(fā)，導(dǎo)致社交網(wǎng)絡(luò)運(yùn)行環(huán)境復(fù)雜多變，使得隱私保護(hù)難以定量分析和驗(yàn)證。對(duì)于社交網(wǎng)絡(luò)隱私設(shè)置缺乏靈活性問(wèn)題而言，這主要是由于當(dāng)前社交網(wǎng)絡(luò)模型多數(shù)采用靜態(tài)隱私策略，而用戶更希望使用更加靈活的動(dòng)態(tài)隱私策略，能以某個(gè)事件作為前提條件觸發(fā)用戶隱私設(shè)置的自動(dòng)更新。對(duì)于社交網(wǎng)絡(luò)隱私設(shè)置缺乏一致性問(wèn)題而言，這主要是由于社交網(wǎng)絡(luò)采用分布式架構(gòu)云存儲(chǔ)機(jī)架集群。用戶處于不同地理位置，任何用戶都有可能在任何時(shí)刻進(jìn)行隱私策略更改，只有保證多源數(shù)據(jù)融合時(shí)數(shù)據(jù)無(wú)延時(shí)和一致性，才能避免用戶隱私信息泄露情況發(fā)生。

社交網(wǎng)絡(luò)用戶行為的不確定性和網(wǎng)絡(luò)配置的不一致性，導(dǎo)致傳統(tǒng)檢驗(yàn)?zāi)Ｐ蜔o(wú)法應(yīng)對(duì)復(fù)雜社交網(wǎng)絡(luò)的隨機(jī)特性。隨機(jī)檢驗(yàn)?zāi)Ｐ褪鞘褂媚Ｐ蜋z驗(yàn)方法對(duì)帶有隨機(jī)行為的復(fù)雜系統(tǒng)進(jìn)行定量驗(yàn)證和分析［5-7］，而運(yùn)行時(shí)驗(yàn)證主要是針對(duì)復(fù)雜動(dòng)態(tài)系統(tǒng)設(shè)計(jì)的驗(yàn)證技術(shù)，但其也面臨隨著運(yùn)行時(shí)間的不斷增加，所需的計(jì)算能力呈幾何式增長(zhǎng)的問(wèn)題［8］。本文提出一種動(dòng)態(tài)隱私保護(hù)框架，將隱私策略設(shè)置作為觸發(fā)條件，通過(guò)運(yùn)行時(shí)驗(yàn)證中的參數(shù)化和監(jiān)控技術(shù)對(duì)用戶隱私信息進(jìn)行保護(hù)。

1 相關(guān)工作

目前，隱私泄露問(wèn)題已引起研究人員的廣泛關(guān)注，現(xiàn)有研究的重點(diǎn)主要包括隱私規(guī)約的形式化驗(yàn)證和隱私泄露的形式化驗(yàn)證兩方面。對(duì)于研究方法而言，隱私規(guī)約的形式化驗(yàn)證方法主要分為基于靜態(tài)模型的靜態(tài)隱私規(guī)約形式化驗(yàn)證方法和基于動(dòng)態(tài)模型的靜態(tài)隱私規(guī)約形式化驗(yàn)證方法，例如文獻(xiàn)［9-11］均是基于靜態(tài)社交網(wǎng)絡(luò)模型，提出靜態(tài)隱私規(guī)約的形式化驗(yàn)證方法。結(jié)合當(dāng)前社交網(wǎng)絡(luò)中存在的隱私泄露問(wèn)題，單純依賴靜態(tài)隱私規(guī)約進(jìn)行驗(yàn)證已經(jīng)無(wú)法滿足當(dāng)前用戶的需求，因此亟需一種針對(duì)社交網(wǎng)絡(luò)中動(dòng)態(tài)隨機(jī)不確定行為的形式化驗(yàn)證方法，例如：文獻(xiàn)［12］提出基于用戶代理知識(shí)邏輯的形式化驗(yàn)證方法，主要解決動(dòng)態(tài)模型的靜態(tài)隱私驗(yàn)證問(wèn)題；文獻(xiàn)［13］提出動(dòng)態(tài)隱私控制的隱私保護(hù)方法，通過(guò)檢驗(yàn)知識(shí)庫(kù)來(lái)驗(yàn)證隱私狀態(tài)是否滿足隱私設(shè)置。此外，研究人員還通過(guò)運(yùn)行時(shí)驗(yàn)證技術(shù)來(lái)驗(yàn)證動(dòng)態(tài)模型中的靜態(tài)隱私規(guī)約，例如文獻(xiàn)［14］提出基于傳播鏈的動(dòng)態(tài)訪問(wèn)控制模型，從訪問(wèn)權(quán)限限制傳播鏈后續(xù)用戶的操作權(quán)限，從而降低惡意用戶的不正當(dāng)分享行為。

對(duì)于隱私策略而言，一些研究人員采取失真或加密技術(shù)來(lái)保護(hù)隱私，例如：文獻(xiàn)［15］采用失真技術(shù)對(duì)用戶隱私泄露問(wèn)題采取差分隱私保護(hù)，利用隨機(jī)森林算法對(duì)不同用戶發(fā)布不同的隱私數(shù)據(jù)，能較好地阻止惡意用戶攻擊；文獻(xiàn)［16］提出基于位置服務(wù)的隱私保護(hù)方法，通過(guò)匿名技術(shù)在不同時(shí)間段添加不同的虛擬用戶，使得社交網(wǎng)絡(luò)用戶的身份信息和位置信息得到加密保護(hù)，尤其是在稀疏環(huán)境下對(duì)用戶身份和位置隱私信息具有較好的保護(hù)作用；文獻(xiàn)［17］提出基于邏輯特征的差分隱私保護(hù)方案，通過(guò)定義語(yǔ)義距離和路徑距離對(duì)請(qǐng)求隱私數(shù)據(jù)的用戶進(jìn)行劃分，實(shí)現(xiàn)差分隱私保護(hù)。

由于在大數(shù)據(jù)環(huán)境下應(yīng)考慮社交網(wǎng)絡(luò)系統(tǒng)的隨機(jī)故障，因此監(jiān)控器技術(shù)作為一種在系統(tǒng)運(yùn)行時(shí)對(duì)系統(tǒng)進(jìn)行驗(yàn)證的技術(shù)，在應(yīng)對(duì)系統(tǒng)隨機(jī)故障時(shí)具有較好的效果，例如：文獻(xiàn)［18］通過(guò)監(jiān)控器監(jiān)控隨機(jī)系統(tǒng)的時(shí)間性質(zhì)，將性質(zhì)規(guī)約表述成表達(dá)式形式，將模型分割成安全性質(zhì)部分和活躍部分，模型檢驗(yàn)與運(yùn)行時(shí)檢驗(yàn)分別驗(yàn)證安全性質(zhì)部分和活躍部分是否滿足系統(tǒng)需求；文獻(xiàn)［19］研究基于數(shù)學(xué)框架的運(yùn)行時(shí)隨機(jī)模型驗(yàn)證方法，通過(guò)給定可靠性模型和需求靜態(tài)生成一組表達(dá)式，這些表達(dá)式可在運(yùn)行時(shí)驗(yàn)證系統(tǒng)需求；文獻(xiàn)［20］結(jié)合運(yùn)行時(shí)驗(yàn)證和模型檢驗(yàn)的相關(guān)技術(shù)提出一種運(yùn)行時(shí)驗(yàn)證框架；文獻(xiàn)［21］將系統(tǒng)模型和系統(tǒng)規(guī)約進(jìn)行預(yù)計(jì)算生成一系列表達(dá)式，降低了運(yùn)行時(shí)驗(yàn)證的計(jì)算復(fù)雜度。

針對(duì)社交網(wǎng)絡(luò)中圖片分享造成的隱私泄露問(wèn)題，文獻(xiàn)［22］結(jié)合靜態(tài)與動(dòng)態(tài)隱私規(guī)約建立形式化隱私語(yǔ)言框架，并通過(guò)經(jīng)典模型檢驗(yàn)方法對(duì)社交網(wǎng)絡(luò)的隱私保護(hù)問(wèn)題進(jìn)行深入研究。本文受其啟發(fā)，借鑒隱私規(guī)約的形式化方法，在考慮社交網(wǎng)絡(luò)模型特性的基礎(chǔ)上，對(duì)其形式化隱私語(yǔ)言框架進(jìn)行適應(yīng)性改進(jìn)，引入概率因子并結(jié)合運(yùn)行時(shí)驗(yàn)證的相關(guān)監(jiān)控技術(shù)，解決社交網(wǎng)絡(luò)中運(yùn)行時(shí)用戶的隱私信息泄露驗(yàn)證和保護(hù)問(wèn)題，滿足用戶的動(dòng)態(tài)隱私設(shè)置需求。

2 動(dòng)態(tài)隱私保護(hù)框架

當(dāng)前社交網(wǎng)絡(luò)隱私策略缺乏穩(wěn)定性、靈活性和一致性，其主要原因是由于社交網(wǎng)絡(luò)架構(gòu)對(duì)于數(shù)據(jù)庫(kù)的權(quán)限過(guò)于集中化。如圖1 所示，各終端用戶保存隱私設(shè)置發(fā)送給Web 服務(wù)器或轉(zhuǎn)發(fā)設(shè)備，Web 服務(wù)器或轉(zhuǎn)發(fā)設(shè)備在接收到相應(yīng)的隱私設(shè)置數(shù)據(jù)后經(jīng)過(guò)數(shù)據(jù)融合保存至云存儲(chǔ)機(jī)架集群中，整個(gè)社交網(wǎng)絡(luò)系統(tǒng)依據(jù)云數(shù)據(jù)庫(kù)中存儲(chǔ)的關(guān)系數(shù)據(jù)執(zhí)行相應(yīng)的權(quán)限設(shè)置，實(shí)現(xiàn)社交網(wǎng)絡(luò)中所有用戶的隱私設(shè)置。

圖1 社交網(wǎng)絡(luò)架構(gòu)Fig.1 Social network architecture

由于社交網(wǎng)絡(luò)用戶的隱私需求不斷增加，當(dāng)前社交網(wǎng)絡(luò)架構(gòu)提供的靜態(tài)隱私策略已經(jīng)無(wú)法滿足用戶的隱私需求，同時(shí)在大數(shù)據(jù)環(huán)境下，數(shù)據(jù)分布廣泛，多源數(shù)據(jù)融合過(guò)程可能存在一定的隨機(jī)性，進(jìn)一步增加了用戶隱私信息泄露的風(fēng)險(xiǎn)。為使社交網(wǎng)絡(luò)的隱私設(shè)置更加靈活和安全，本文提出動(dòng)態(tài)隱私保護(hù)框架，通過(guò)在終端植入監(jiān)控器獲取社交網(wǎng)絡(luò)運(yùn)行時(shí)參數(shù)進(jìn)行運(yùn)行時(shí)驗(yàn)證，同時(shí)對(duì)傳統(tǒng)靜態(tài)隱私規(guī)約進(jìn)行分解預(yù)處理，在傳統(tǒng)靜態(tài)隱私規(guī)約的基礎(chǔ)上增加觸發(fā)條件a，將動(dòng)態(tài)隱私規(guī)約形式化表述為a→b的表達(dá)式形式，當(dāng)前置條件滿足a時(shí)，隱私設(shè)置會(huì)自動(dòng)更改為b，通過(guò)監(jiān)控器來(lái)監(jiān)控用戶所在社交網(wǎng)絡(luò)是否滿足a來(lái)動(dòng)態(tài)執(zhí)行隱私設(shè)置b。通過(guò)對(duì)隱私規(guī)約的預(yù)處理可大幅降低運(yùn)行時(shí)驗(yàn)證的復(fù)雜度，極大降低所需的運(yùn)算能力。動(dòng)態(tài)隱私保護(hù)框架如圖2所示。

圖2 動(dòng)態(tài)隱私保護(hù)框架Fig.2 Dynamic privacy protection framework

動(dòng)態(tài)隱私保護(hù)框架主要是針對(duì)社交網(wǎng)絡(luò)隱私設(shè)置不靈活和難以驗(yàn)證的問(wèn)題提出的解決方案。本文使用隨機(jī)模型檢驗(yàn)與運(yùn)行時(shí)檢驗(yàn)中的監(jiān)控技術(shù)相結(jié)合的方法，將整個(gè)社交網(wǎng)絡(luò)模型構(gòu)建為一個(gè)基于知識(shí)邏輯（Knowledge Based Logic，KBL）拓展的離散時(shí)間馬爾科夫鏈（Discrete Time Markov Chains，DTMC）模型，將社交網(wǎng)絡(luò)用戶的隱私設(shè)置形式化表述為概率計(jì)算樹(shù)邏輯（Probabilistic Computation Tree Logic，PCTL）［23］，同時(shí)加入運(yùn)行時(shí)驗(yàn)證理論中的參數(shù)化技術(shù)。通過(guò)向待驗(yàn)證的社交網(wǎng)絡(luò)系統(tǒng)植入監(jiān)控器Pmonitor，獲取待監(jiān)控用戶進(jìn)行驗(yàn)證時(shí)所需的隱私數(shù)據(jù)作為參數(shù)傳入隨機(jī)模型檢驗(yàn)工具，然后依據(jù)事先給定的隱私規(guī)約，若滿足規(guī)約則繼續(xù)監(jiān)控，若不滿足則給出反例和提示，提醒用戶進(jìn)行相應(yīng)的更改和操作，以防止隱私信息泄露。

3 基于KBL 的PCTL 轉(zhuǎn)換算法

3.1 KBL 定義及相關(guān)概念

定義1（KBL）給定非空的命題集合P，用戶i，g∈Ag，Ag為用戶集合，命題p∈P，分組G∈Ag，路徑公式γ∷=﹁γ|γ∧γ|φ，事件φ∷=p|φ∧φ|﹁φ|Kiφ|EGφ|SGφ，KBL 相關(guān)模態(tài)的定義如下：

3.2 PCTL 轉(zhuǎn)換算法

由于利用KBL 表述用戶知識(shí)庫(kù)狀態(tài)，因此通過(guò)判斷知識(shí)庫(kù)狀態(tài)可驗(yàn)證隱私信息是否泄露，但是KBL 無(wú)法應(yīng)用于隨機(jī)模型檢驗(yàn)及使用PRISM 工具進(jìn)行自動(dòng)化驗(yàn)證，本文設(shè)計(jì)一種將KBL 轉(zhuǎn)換為PCTL 的算法，通過(guò)該算法可將KBL 轉(zhuǎn)換成在PRISM 進(jìn)行驗(yàn)證的PCTL 語(yǔ)法。

算法1基于KBL 的PCTL 轉(zhuǎn)換算法

通過(guò)該算法可實(shí)現(xiàn)以下功能：1）基于監(jiān)控器參數(shù)生成用戶社交關(guān)系圖；2）基于用戶屏蔽對(duì)象實(shí)現(xiàn)不同用戶的知識(shí)庫(kù)更新策略；3）基于用戶知識(shí)庫(kù)確定用戶狀態(tài)，依據(jù)用戶狀態(tài)確定可達(dá)目標(biāo)集合s；4）實(shí)現(xiàn)引理1 及引理2 中基于KBL 的邏輯推理規(guī)則。

定理1基于KBL 的DTMC 模型為可終止。

證明令M=＜S，＜action，p＞，linit，AP，L＞，B∈s是目標(biāo)狀態(tài)集合，最終到達(dá)目標(biāo)狀態(tài)集合B記作?B，為證明到達(dá)目標(biāo)狀態(tài)是可終止的，需證?B的路徑集合是可計(jì)算的。

1）在有窮狀態(tài)下，可知路徑集合?B滿足Cyl（s0，s1，…，sn），其中（s0，s1，…，sn）是一個(gè)屬于模型M的初始路徑片段，滿足（s0，s1，…，sn）?B，sn∈B所有的路徑集合由Paths(M) ∩(S?B)×B給出，由于路徑是有窮的，因此到達(dá)目標(biāo)狀態(tài)集合B的路徑長(zhǎng)度是可數(shù)的，屬于M的?代數(shù)，同時(shí)由于這些路徑集合是成對(duì)不相交的，因此最終到達(dá)集合M的概率計(jì)算公式為：

其中，PrM代表在馬爾科夫鏈模型M中滿足某條路徑集合的概率，Paths為最終到達(dá)節(jié)點(diǎn)s的路徑集合。

2）在無(wú)窮路徑狀態(tài)下，對(duì)于任意狀態(tài)s∈S，令ps代表從狀態(tài)s出發(fā)到達(dá)B狀態(tài)集合的概率：若B是從s出發(fā)不可到達(dá)的，則ps=0；若s∈B，則ps=1；若ps＞0，則說(shuō)明從狀態(tài)s出發(fā)到達(dá)B狀態(tài)集合是可到達(dá)的。因此，對(duì)于任意狀態(tài)s∈S?B均可到達(dá)B需滿足：

對(duì)于任意狀態(tài)s∈S?B，若s是可到達(dá)B的，則可分為以下兩種情況：

（1）從s到B是一步之內(nèi)可到達(dá)的，情況如式（2）右邊第2 項(xiàng)所示：設(shè)u是屬于集合B內(nèi)的狀態(tài)，則在該情況下的路徑為s→u。

（2）從s到B是非一步之內(nèi)可到達(dá)的，情況如式（2）右邊第1 項(xiàng)所示：設(shè)t是從s出發(fā)到達(dá)u的中間狀態(tài)，u是屬于集合B內(nèi)的狀態(tài)，則在該情況下的路徑為s→t→…→u，令S′=Pr(B)?B代表滿足路徑片段條件為s0，s1，…，sn(n＞0，s0=S，sn∈B）的狀態(tài)集合。對(duì)于所有的狀態(tài)s∈S?B，其到達(dá)B的可達(dá)性概率ps可記為向量X=（ps）s∈S?B并得到：

其中，A代表s∈S?B的所有狀態(tài)遷移矩陣，b是所有位于集合B外可一步到達(dá)B的狀態(tài)集合的遷移向量。式（3）移項(xiàng)可得式（4）：

其中，I是一個(gè)|s′|×|s′|的基數(shù)恒等矩陣。因此，該過(guò)程是對(duì)方程組(I-A) ·X=b的線性求解過(guò)程：當(dāng)IA為非奇異矩陣，必然有唯一解；當(dāng)I-A為奇異矩陣，有多解，此時(shí)該求解問(wèn)題轉(zhuǎn)化為求解期望的概率向量的最優(yōu)解問(wèn)題，可通過(guò)近似迭代方法計(jì)算出概率向量b，例如高斯消元法。

設(shè)M=(S，P，linit，AP，L)為一個(gè)馬爾科夫鏈(MC)，B，C∈S，假設(shè)事件最終到達(dá)狀態(tài)B，經(jīng)歷如下有窮路徑片段：先經(jīng)過(guò)狀態(tài)集合C然后到達(dá)最終狀態(tài)s，即linit→…→C→s，s∈B，對(duì)于該假設(shè)事件可記作C?B，已知?B嚴(yán)格滿足于S?B，即對(duì)于n≥0，事件C?≤n B與事件C?B具有相同的路徑，但事件C?≤n B要求經(jīng)過(guò)前驅(qū)狀態(tài)集合B，因此?B的路徑片段s0，s1，…，sk滿足k≤n，si∈C，sk∈B，0 ≤i≤k，可將S分割成S=0、S=1和S=？，分為以下3 種情況：①B?情況1和情況2 顯然很容易得到求解結(jié)果。情況3 可通過(guò)高斯消元法得到二次型矩陣A=(P(s，t))s，t∈S=？，通過(guò)同樣的方法向量b可定義為，最終通過(guò)求解概率Pr(s?C?B)s∈S的最小不動(dòng)特征點(diǎn)來(lái)求解該方程組的最優(yōu)解。

綜上所述，當(dāng)路徑為有限路徑時(shí)到達(dá)集合B的概率是一個(gè)有關(guān)M的?代數(shù)，當(dāng)路徑為無(wú)限路徑時(shí)到達(dá)集合B的概率是求解式（4）的線性最優(yōu)解，因此基于KBL 的DTMC 模型的可達(dá)性概率是可計(jì)算的，該模型為可終止得以證明。

定理2基于KBL 的DTMC 模型保證在PCTL轉(zhuǎn)換算法執(zhí)行前后及執(zhí)行過(guò)程中都可以正確迭代用戶知識(shí)庫(kù)狀態(tài)。

證明使用循環(huán)不變式證明PCTL 轉(zhuǎn)換算法的正確性，需要證明在算法執(zhí)行前、執(zhí)行時(shí)及結(jié)束時(shí)均能正確迭代用戶知識(shí)庫(kù)狀態(tài)。

1）算法執(zhí)行前：循環(huán)不變式成立，監(jiān)控器中的關(guān)系列表、圖G中所有用戶節(jié)點(diǎn)、用戶知識(shí)庫(kù)kb、集合S均為?，即在循環(huán)開(kāi)始前滿足監(jiān)控器參數(shù)與用戶社交圖的對(duì)應(yīng)關(guān)系，屏蔽對(duì)象、post 函數(shù)參數(shù)為?且滿足用戶知識(shí)庫(kù)的迭代策略，圖G中所有節(jié)點(diǎn)狀態(tài)均為﹁Kuφ，保證用戶狀態(tài)的分類結(jié)果正確。

2）算法執(zhí)行時(shí)：在第1 個(gè)while 循環(huán)的算法1 的第9 行～第11 行，將圖G中節(jié)點(diǎn)u的個(gè)數(shù)依次迭代增加，同時(shí)list列表中變量i依次減少，此時(shí)u=len(list-i)，在循環(huán)過(guò)程中滿足節(jié)點(diǎn)個(gè)數(shù)等于遍歷列表的元素個(gè)數(shù)，滿足功能1；在第2 個(gè)while 循環(huán)的第13 行～第17 行，對(duì)于圖G中任意的u∈G∧u?block 均滿足setting privacySu∈gφinG，滿足功能2，第3 個(gè)for 循環(huán)的第19 行～第23 行，對(duì)于圖G中任意的u∈G均滿足setting privacyEu∈gφinG；第3 個(gè)和第4 個(gè)for 循環(huán)遍歷所有節(jié)點(diǎn)的知識(shí)庫(kù)狀態(tài)，將滿足的狀態(tài)加入目標(biāo)狀態(tài)集合S中，滿足功能3。

3）算法結(jié)束時(shí)：第1 個(gè)while 循環(huán)的終止條件list=?，此時(shí)i=0，u=len(list)-i，即u=len(list)，說(shuō)明列表中的所有相關(guān)用戶已被完全生成圖G中的節(jié)點(diǎn)。第2 個(gè)while 循環(huán)的終止條件是block(i)=?，當(dāng)block(i)=?時(shí)，此時(shí)有i=len(block)，設(shè)m為圖G中所有的節(jié)點(diǎn)數(shù)目，根據(jù)算法1 的第14 行、第15 行可知m=u+i，即滿足功能2；對(duì)于第3 個(gè)for 循環(huán)的終止條件為遍歷完所有圖G中的節(jié)點(diǎn)，此時(shí)集合S中的狀態(tài)為滿足目標(biāo)的狀態(tài)集合。綜上，基于KBL 的PCTL 轉(zhuǎn)換算法的正確性得以證明。

依據(jù)算法1 的第2 行～第11 行，遍歷監(jiān)控器的整個(gè)用戶關(guān)系列表，創(chuàng)建社交關(guān)系圖，所需的時(shí)間復(fù)雜度為O(n2)，其中n為關(guān)系列表中的用戶個(gè)數(shù)，第13 行～第24 行遍歷圖G，通過(guò)廣度優(yōu)先搜索為每個(gè)用戶設(shè)置知識(shí)庫(kù)的更新策略，因此時(shí)間復(fù)雜度為O(n2)，n為圖G中的節(jié)點(diǎn)個(gè)數(shù)。綜上，基于KBL 的PCTL 轉(zhuǎn)換算法的時(shí)間復(fù)雜度為O(n2)。

引理1若用戶設(shè)置SGφ，則分組G中至少有一個(gè)用戶的知識(shí)庫(kù)狀態(tài)為Kiφ，形式化為SGφ→∨i∈G Kiφ。

證明

1）算法執(zhí)行前：此時(shí)未創(chuàng)建用戶關(guān)系節(jié)點(diǎn)圖，SGφ=?，所有用戶知識(shí)庫(kù)Kiφ=?，i表示所有用戶，滿足引理1。

2）算法執(zhí)行時(shí)：依據(jù)list 參數(shù)生成關(guān)系表，并根據(jù)算法1 的第13 行～第18 行，根據(jù)block 參數(shù)為非block 節(jié)點(diǎn)更新知識(shí)庫(kù)Kiφ，其中i=list(μ)，i?block(i)，μ為被監(jiān)控的用戶，同時(shí)有SGφ=φ，∨i∈G Kiφ=φ，滿足引理1。

3）算法結(jié)束時(shí)：用戶關(guān)系節(jié)點(diǎn)圖及用戶知識(shí)庫(kù)更新完畢。循環(huán)遍歷G中所有節(jié)點(diǎn)知識(shí)庫(kù)Kiφ，有∨i∈G Kiφ=φ，其中i=list(μ)，i?block(i)，同時(shí)有SGφ=φ，滿足引理1。

引理2若用戶設(shè)置EGφ，則分組G中每一個(gè)用戶的知識(shí)庫(kù)狀態(tài)為Kiφ，形式化為EGφ→∧i∈G Kiφ。

證明

1）算法執(zhí)行前：此時(shí)未創(chuàng)建用戶關(guān)系節(jié)點(diǎn)圖，EGφ=?，所有用戶知識(shí)庫(kù)Kiφ=?，i表示所有用戶，滿足引理2。

2）算法執(zhí)行時(shí)：依據(jù)list 參數(shù)生成關(guān)系表，并根據(jù)算法1 中的第21 行～第26 行以及block 參數(shù)為非block 節(jié)點(diǎn)更新知識(shí)庫(kù)Kiφ，其中，∧i∈G Kiφ=φ且i=list(μ)，i?block(i)，同時(shí)有EGφ=φ，滿足引理2。

3）算法結(jié)束時(shí)：用戶關(guān)系節(jié)點(diǎn)圖及用戶知識(shí)庫(kù)更新完畢。循環(huán)遍歷G中所有節(jié)點(diǎn)知識(shí)庫(kù)Kiφ，有∧i∈G Kiφ=φ，其中i=list(μ)，i?block(i)，同時(shí)有EGφ=φ，滿足引理2。

4 隱私規(guī)約的形式化表述

通過(guò)算法1 轉(zhuǎn)換后的PCTL 語(yǔ)義如下：

其中，φ表示狀態(tài)公式，a∈AP 表示原子命題，～∈｛＜，≤，＞，≥｝，ψ表示路徑公式。轉(zhuǎn)換后的PCTL 引入了K算子，通過(guò)K算子來(lái)描述用戶的知識(shí)庫(kù)狀態(tài)，對(duì)于給定的社交網(wǎng)絡(luò)模型以及隱私設(shè)置π，有狀態(tài)s∈S，狀態(tài)公式φ滿足如下關(guān)系：

其中，Pr(s?φ)=Prs{π∈Paths(s)|π?ψ}，Prs為滿足最終到達(dá)節(jié)點(diǎn)s的路徑概率。

路徑公式ψ的滿足如下關(guān)系：

其中，路徑π=s0，s1，…，si，i表示整數(shù)，π[i]表示路徑π的第i個(gè)狀態(tài)。

4.1 靜態(tài)隱私規(guī)約的形式化表述

為滿足用戶的隱私保護(hù)需求，在形式化表述的靜態(tài)隱私規(guī)約的基礎(chǔ)上加入[ ]標(biāo)記，在KBL 的外面加上[ ]標(biāo)記表示該項(xiàng)隱私設(shè)置由該用戶設(shè)置。本文通過(guò)集合spec()記錄用戶u設(shè)置的隱私規(guī)約，記為spec(u)，假設(shè)靜態(tài)隱私規(guī)約1 為如果用戶A暫時(shí)屏蔽了用戶B，即用戶A不希望用戶B知道其所發(fā)的某一條動(dòng)態(tài)post(φ)，使用帶[ ]標(biāo)記的公式進(jìn)行表示：

1）對(duì)于用戶A：用戶A不希望用戶B知道其所發(fā)的某一條動(dòng)態(tài)φ，F(xiàn)or agentAsatisfy：。

2）對(duì)于社交網(wǎng)絡(luò)模型SN 而言，整個(gè)系統(tǒng)需求要求用戶B知道用戶A所發(fā)的某一條動(dòng)態(tài)φ的概率不高于0.01，F(xiàn)or module SN satisfy：。

為表述方便，靜態(tài)隱私規(guī)約1 也可以表述為For module SN satisfy：。通過(guò)以上方式可對(duì)SN 中用戶設(shè)置的靜態(tài)隱私規(guī)約進(jìn)行形式化表述。

4.2 動(dòng)態(tài)隱私規(guī)約的形式化表述

動(dòng)態(tài)隱私與靜態(tài)隱私的區(qū)別在于動(dòng)態(tài)隱私可根據(jù)預(yù)先設(shè)定的觸發(fā)條件對(duì)隱私設(shè)置進(jìn)行更改，靜態(tài)隱私則是如果用戶不主動(dòng)進(jìn)行更改則一直維持該設(shè)置，因此本文將動(dòng)態(tài)隱私表示為a→b的形式，即如果滿足條件a，那么就執(zhí)行b，將動(dòng)態(tài)隱私設(shè)置分解為a→b的形式并依據(jù)觸發(fā)條件的不同，將動(dòng)態(tài)隱私設(shè)置主要分為基于時(shí)間的動(dòng)態(tài)隱私設(shè)置（BOT）、基于地點(diǎn)的動(dòng)態(tài)隱私設(shè)置（BOL）、基于事件的動(dòng)態(tài)隱私設(shè)置（BOE）3 類，具體為：

1）基于時(shí)間的動(dòng)態(tài)隱私設(shè)置。觸發(fā)條件為時(shí)間，當(dāng)系統(tǒng)內(nèi)部時(shí)間滿足條件a時(shí)會(huì)觸發(fā)條件b，定義動(dòng)態(tài)隱私規(guī)約1 為在社交網(wǎng)絡(luò)中某一用戶u希望對(duì)其工作時(shí)間和非工作時(shí)間進(jìn)行區(qū)分，非工作時(shí)間避免同事們打擾，可設(shè)置如下的BOT 規(guī)則：在非工作時(shí)間第1 天晚上20：00 至第2 天早上08：00，不希望college列表中的同事們看到自己的某一條動(dòng)態(tài)φ，用PCTL可表示為[ ]20：00≤timer≤08：00→。

2）基于地點(diǎn)的動(dòng)態(tài)隱私設(shè)置。觸發(fā)條件為地點(diǎn)，當(dāng)系統(tǒng)內(nèi)部定位的地點(diǎn)滿足條件時(shí)會(huì)觸發(fā)條件，定義動(dòng)態(tài)隱私規(guī)約2 為在社交網(wǎng)絡(luò)中某一用戶u希望對(duì)其工作地點(diǎn)和非工作地點(diǎn)進(jìn)行區(qū)分，只在工作地點(diǎn)（company）所發(fā)表的動(dòng)態(tài)才會(huì)被同事們所看到，可設(shè)置如下BOL 規(guī)則：只在工作地點(diǎn)所發(fā)表的動(dòng)態(tài)可被college 列表中的同事所看見(jiàn)，用PCTL 可表示為。

3）基于事件的動(dòng)態(tài)隱私設(shè)置。觸發(fā)條件為事件，當(dāng)系統(tǒng)內(nèi)檢測(cè)到滿足條件的事件發(fā)生時(shí)就會(huì)觸發(fā)條件，定義動(dòng)態(tài)隱私規(guī)約3 為某一用戶u希望能更加靈活地管理自己的朋友列表，為防止自己的動(dòng)態(tài)被人無(wú)限制轉(zhuǎn)發(fā)，可設(shè)置如下BOE 規(guī)則：只有當(dāng)好友a(bǔ)點(diǎn)贊并評(píng)論自己所發(fā)的某條動(dòng)態(tài)后，該好友才有權(quán)限轉(zhuǎn)發(fā)該動(dòng)態(tài)，否則不給予其轉(zhuǎn)發(fā)該條動(dòng)態(tài)的權(quán)限，用PCTL 可表示為[ ]（like(φ)∧comment(φ)=true）∈a→reposted(φ) ?a。

由于動(dòng)態(tài)隱私設(shè)置需要依據(jù)觸發(fā)條件來(lái)動(dòng)態(tài)更改用戶的社交網(wǎng)絡(luò)結(jié)構(gòu)，因此本文需先對(duì)靜態(tài)隱私設(shè)置進(jìn)行更改以滿足動(dòng)態(tài)隱私需求。設(shè)置一個(gè)臨時(shí)屏蔽分組（block），在分組中存儲(chǔ)不滿足動(dòng)態(tài)隱私規(guī)范而被臨時(shí)屏蔽的好友，基于時(shí)間的動(dòng)態(tài)隱私保護(hù)框架如圖3 所示。

圖3 基于時(shí)間的動(dòng)態(tài)隱私保護(hù)框架Fig.3 Dynamic privacy protection framework based on time

當(dāng)不滿足遷移條件的好友被移到block 分組時(shí)，若一旦監(jiān)控器監(jiān)測(cè)到條件滿足，則會(huì)將block 分組中的好友移回原分組?；诘攸c(diǎn)和事件的動(dòng)態(tài)隱私保護(hù)框架如圖4、圖5 所示，其中，like（φ）=μ表示用戶μ對(duì)動(dòng)態(tài)φ進(jìn)行點(diǎn)贊，comment（φ）=μ表示用戶μ對(duì)動(dòng)態(tài)φ進(jìn)行評(píng)論，reposted（φ）=μ表示用戶μ對(duì)動(dòng)態(tài)φ進(jìn)行轉(zhuǎn)發(fā)。

圖4 基于地點(diǎn)的動(dòng)態(tài)隱私保護(hù)框架Fig.4 Dynamic privacy protection framework based on location

圖5 基于事件的動(dòng)態(tài)隱私保護(hù)框架Fig.5 Dynamic privacy protection framework based on event

5 社交網(wǎng)絡(luò)系統(tǒng)的形式化建模

5.1 基于靜態(tài)隱私保護(hù)框架的DTMC 模型

對(duì)于靜態(tài)隱私保護(hù)框架，終端用戶設(shè)置隱私規(guī)約后發(fā)送給服務(wù)器或轉(zhuǎn)發(fā)設(shè)備，服務(wù)器接受隱私規(guī)約后進(jìn)行數(shù)據(jù)融合更新，本文對(duì)靜態(tài)隱私保護(hù)框架的DTMC建模如圖6 所示。若狀態(tài)間未標(biāo)明轉(zhuǎn)移概率，則默認(rèn)其轉(zhuǎn)移概率為1，系統(tǒng)狀態(tài)及其含義如表1 所示。

圖6 基于靜態(tài)隱私保護(hù)框架的DTMC 模型Fig.6 DTMC model based on static privacy protection framework

表1 系統(tǒng)狀態(tài)及其含義Table 1 System status and its meaning

社交網(wǎng)絡(luò)用戶將新的隱私設(shè)置發(fā)送給服務(wù)器，但服務(wù)器和用戶之間的通信協(xié)議存在一定的隨機(jī)性，即服務(wù)器可能有p1的概率接收數(shù)據(jù)失敗。由于社交網(wǎng)絡(luò)用戶非常多，服務(wù)器在短時(shí)間內(nèi)接收的用戶隱私設(shè)置無(wú)法同一時(shí)間立即完成更新，因此當(dāng)服務(wù)器正在更新設(shè)置時(shí)，剛接收到的數(shù)據(jù)有p2的概率進(jìn)入服務(wù)器忙碌狀態(tài)，需要服務(wù)器等待重新接收數(shù)據(jù)進(jìn)行處理。當(dāng)服務(wù)器處于空閑狀態(tài)并接收數(shù)據(jù)后開(kāi)始更新操作，由于更新操作建立在通信協(xié)議的基礎(chǔ)上，因此更新操作有p3的概率更新失敗。

5.2 基于動(dòng)態(tài)隱私保護(hù)框架的DTMC 模型

本文根據(jù)動(dòng)態(tài)隱私保護(hù)框架，將其分為社交網(wǎng)絡(luò)模型SN 和隱私監(jiān)控器P-monitor 兩部分進(jìn)行建模。社交網(wǎng)絡(luò)模型如圖7 所示，其中實(shí)線單向箭頭、實(shí)線雙向箭頭、虛線單向箭頭、點(diǎn)劃線單向箭頭分別代表用戶節(jié)點(diǎn)之間的好友、同事、屏蔽、陌生人4 種社交關(guān)系。

圖7 社交網(wǎng)絡(luò)模型Fig.7 Social network model

定義2（P-monitor）P-monitor=＜User，timer，location，list，operation＞，其中：User表示記錄被監(jiān)控的社交網(wǎng)絡(luò)用戶，返回值是用戶u∈Ag；timer 表示時(shí)間記錄器，用于記錄系統(tǒng)內(nèi)部時(shí)間，返回值是時(shí)間序列；location 表示地點(diǎn)記錄器，用于記錄被監(jiān)控用戶當(dāng)前的位置，返回值是定位信息；list表示＜friend，family，strange，college，block＞，list列表用于記錄被監(jiān)控用戶的關(guān)系列表，返回值是集合｛u1，u2，…｝，u1，u2∈Ag；operation表示主要監(jiān)控用戶權(quán)限范圍內(nèi)可調(diào)用的函數(shù)，如發(fā)表動(dòng)態(tài)、轉(zhuǎn)發(fā)別人的動(dòng)態(tài)、允許別人轉(zhuǎn)發(fā)自己的某一條動(dòng)態(tài)、點(diǎn)贊、不喜歡、評(píng)論等行為分別調(diào)用post、repost、reposted、like、dislike 等函數(shù)。

將隱私監(jiān)控器P-monitor 植入社交網(wǎng)絡(luò)模型中，結(jié)合隨機(jī)模型檢驗(yàn)工具，構(gòu)建基于動(dòng)態(tài)隱私保護(hù)框架的DTMC 模型，如圖8 所示。

圖8 基于動(dòng)態(tài)隱私保護(hù)框架的DTMC 模型Fig.8 DTMC model based on dynamic privacy protection framework

在動(dòng)態(tài)隱私保護(hù)框架中發(fā)送給服務(wù)器更新隱私規(guī)約這部分內(nèi)容與靜態(tài)隱私保護(hù)框架相同，不同的是在動(dòng)態(tài)隱私保護(hù)框架下，用戶會(huì)將動(dòng)態(tài)隱私策略會(huì)發(fā)送給P-monitor。P-monitor 與用戶之間是一一對(duì)應(yīng)關(guān)系，即每個(gè)使用靜態(tài)隱私策略的用戶都會(huì)在用戶終端生成一個(gè)P-monitor，P-monitor 可以執(zhí)行服務(wù)器接收數(shù)據(jù)的功能，由于P-monitor 與用戶之間的通信也建立在通信協(xié)議的基礎(chǔ)上，因此P-monitor 有p4的概率未接受用戶的隱私規(guī)約，但是當(dāng)P-monitor接受新的隱私規(guī)約后就立即對(duì)社交網(wǎng)絡(luò)進(jìn)行監(jiān)控，因此不會(huì)出現(xiàn)更新失敗的情況。

6 實(shí)驗(yàn)結(jié)果與分析

由于當(dāng)前社交網(wǎng)絡(luò)均是非開(kāi)源網(wǎng)絡(luò)，因此本文選擇開(kāi)源社交網(wǎng)絡(luò)軟件驗(yàn)證社交網(wǎng)絡(luò)的隱私泄露問(wèn)題。Diaspora是一款由美國(guó)紐約大學(xué)學(xué)生所開(kāi)發(fā)的基于Web的開(kāi)源社交網(wǎng)絡(luò)［24］。PRISM 是一款由英國(guó)牛津大學(xué)Prof.Marta 研究組研發(fā)的隨機(jī)模型檢驗(yàn)工具［25］，被用于驗(yàn)證通信協(xié)議、密碼協(xié)議和生物系統(tǒng)［26］等的可靠性，具有較好的檢驗(yàn)效果。本文在Diaspora 社交網(wǎng)絡(luò)上植入監(jiān)控器，并在PRISM 隨機(jī)模型檢驗(yàn)工具上進(jìn)行驗(yàn)證。實(shí)驗(yàn)共分為靜態(tài)隱私驗(yàn)證和動(dòng)態(tài)隱私驗(yàn)證兩部分，其中：靜態(tài)隱私部分針對(duì)靜態(tài)隱私規(guī)約1；動(dòng)態(tài)隱私部分針對(duì)動(dòng)態(tài)隱私規(guī)約1和3。整體實(shí)驗(yàn)運(yùn)行基于PRISM4.5，假定Diaspora 服務(wù)器端接收用戶發(fā)送信息失敗的概率p1和服務(wù)器更新失敗的概率p2均為0.01，同時(shí)在動(dòng)態(tài)隱私保護(hù)框架中假設(shè)P-monitor 接收用戶新的隱私設(shè)置數(shù)據(jù)失敗的概率p4也為0.01。通過(guò)PRISM 建立靜態(tài)隱私保護(hù)框架模型累計(jì)狀態(tài)集合為32個(gè)，其中包含1個(gè)初始狀態(tài)，轉(zhuǎn)移狀態(tài)共64 個(gè)，動(dòng)態(tài)隱私保護(hù)框架模型累計(jì)狀態(tài)集合為1 152 個(gè)，其中包含1 個(gè)初始狀態(tài)，轉(zhuǎn)移狀態(tài)共6 519 個(gè)。

對(duì)于動(dòng)態(tài)隱私規(guī)約1，P-monitor輸入?yún)?shù)如表2 所示，其中，User 表示被監(jiān)控的用戶，timer 表示時(shí)間記錄器，location 表示地點(diǎn)記錄器，post表示被監(jiān)控用戶是否發(fā)表動(dòng)態(tài)，reposted 表示對(duì)動(dòng)態(tài)進(jìn)行轉(zhuǎn)發(fā)的用戶集合，like 表示被對(duì)動(dòng)態(tài)進(jìn)行點(diǎn)贊的用戶集合，dislike 表示對(duì)動(dòng)態(tài)不喜歡的用戶集合，comment 表示對(duì)動(dòng)態(tài)進(jìn)行評(píng)論的用戶集合，表示最終用戶Bob知道被監(jiān)控對(duì)象Alice 發(fā)表動(dòng)態(tài)的概率。

表2 動(dòng)態(tài)隱私規(guī)約1 的P-monitor 輸入?yún)?shù)Table 2 P-monitor input parameters of dynamic privacy specification 1

通過(guò)實(shí)驗(yàn)數(shù)據(jù)發(fā)現(xiàn)，在服務(wù)器和監(jiān)控器的容錯(cuò)概率下，使用監(jiān)控器來(lái)保存動(dòng)態(tài)隱私設(shè)置要比使用服務(wù)器來(lái)更新靜態(tài)隱私設(shè)置的隱私泄露風(fēng)險(xiǎn)降低50%，這主要是因?yàn)閮烧呒軜?gòu)不同，服務(wù)器是針對(duì)所有用戶，存在擁塞和延遲，并且出錯(cuò)概率也大幅提高，但是監(jiān)控器是針對(duì)個(gè)人用戶，不存在擁塞和延遲，所以可以大幅降低隱私泄露風(fēng)險(xiǎn)。

為進(jìn)一步驗(yàn)證動(dòng)態(tài)隱私策略和靜態(tài)隱私策略在時(shí)間維度上的隱私泄露風(fēng)險(xiǎn)，設(shè)定每一步長(zhǎng)的reward 為1，其中reward 為執(zhí)行圖遍歷算法的花費(fèi)，通過(guò)實(shí)驗(yàn)對(duì)比分析不同時(shí)間維度下動(dòng)態(tài)和靜態(tài)隱私泄露風(fēng)險(xiǎn)，實(shí)驗(yàn)結(jié)果如圖9 所示。靜態(tài)DTMC 模型內(nèi)部各個(gè)節(jié)點(diǎn)的狀態(tài)變化如圖10 所示，其中，User表示被監(jiān)控用戶的節(jié)點(diǎn)狀態(tài)，Agent 表示代理服務(wù)器的節(jié)點(diǎn)狀態(tài)。

圖9 靜態(tài)與動(dòng)態(tài)隱私策略的隱私泄露風(fēng)險(xiǎn)對(duì)比Fig.9 Comparison of privacy disclosure risks between static and dynamic privacy strategy

圖10 靜態(tài)DTMC 模型節(jié)點(diǎn)狀態(tài)遷移Fig.10 Node state transition of static DTMC model

實(shí)驗(yàn)結(jié)果表明，在極短時(shí)間內(nèi)動(dòng)態(tài)隱私規(guī)約相比靜態(tài)隱私規(guī)約出現(xiàn)了用戶隱私信息泄露的情況，產(chǎn)生該情況的主要原因?yàn)閯?dòng)態(tài)隱私設(shè)置采用監(jiān)控器直接對(duì)用戶隱私設(shè)置進(jìn)行保存和監(jiān)控，同時(shí)考慮到監(jiān)控器在接收用戶數(shù)據(jù)信息時(shí)會(huì)產(chǎn)生一定的失敗概率，并且監(jiān)控器發(fā)生錯(cuò)誤的情況要比服務(wù)器更快，因此在極短時(shí)間內(nèi)，若監(jiān)控器發(fā)生錯(cuò)誤，則會(huì)比靜態(tài)隱私保護(hù)框架下服務(wù)器發(fā)生錯(cuò)誤的時(shí)間更短。但是從長(zhǎng)時(shí)間而言，在穩(wěn)定狀態(tài)下動(dòng)態(tài)隱私保護(hù)框架比靜態(tài)隱私保護(hù)框架的用戶隱私信息泄露風(fēng)險(xiǎn)更低，并且動(dòng)態(tài)隱私規(guī)約也更靈活性。

對(duì)于動(dòng)態(tài)隱私規(guī)約3，由于在動(dòng)態(tài)隱私保護(hù)框架中隱私泄露的風(fēng)險(xiǎn)只與是否成功接收到被監(jiān)控用戶發(fā)送的數(shù)據(jù)有關(guān)，因此本文只驗(yàn)證在P-monitor 未正常更新的情況下，由于用戶的隨機(jī)行為所產(chǎn)生的隱私泄露概率。假定用戶設(shè)置的動(dòng)態(tài)隱私設(shè)置未成功保存至P-monitor中，在該假設(shè)前提下P-monitor輸入?yún)?shù)如表3所示。動(dòng)態(tài)DTMC 模型內(nèi)部各節(jié)點(diǎn)的狀態(tài)變化如圖11所示，其中，Bob 表示用戶Bob 的節(jié)點(diǎn)狀態(tài)，Update 表示監(jiān)控器執(zhí)行用戶隱私設(shè)置的狀態(tài)。

表3 動(dòng)態(tài)隱私規(guī)約3 的P-monitor 輸入?yún)?shù)Table 3 P-monitor input parameters of dynamic privacy specification 3

圖11 動(dòng)態(tài)DTMC 模型節(jié)點(diǎn)狀態(tài)遷移Fig.11 Node state transition of dynamic DTMC model

實(shí)驗(yàn)結(jié)果表明，本文設(shè)計(jì)的動(dòng)態(tài)隱私保護(hù)框架通過(guò)植入P-monitor 進(jìn)行用戶隱私設(shè)置，但不發(fā)送到服務(wù)器端，其主要原因?yàn)榉?wù)器端存在的接收失敗、忙碌、更新失敗等隨機(jī)故障，會(huì)導(dǎo)致隱私泄露風(fēng)險(xiǎn)遠(yuǎn)大于用戶需求。基于P-monitor 的動(dòng)態(tài)隱私保護(hù)框架通過(guò)動(dòng)態(tài)的隱私設(shè)置，提高社交網(wǎng)絡(luò)隱私設(shè)置的靈活性，并基于P-monitor 與用戶間一對(duì)一的監(jiān)控結(jié)構(gòu)，解決了服務(wù)器端存在的接收失敗、忙碌、更新失敗等隨機(jī)故障，降低了用戶隱私泄露風(fēng)險(xiǎn)。

7 結(jié)束語(yǔ)

本文提出一種面向社交網(wǎng)絡(luò)的動(dòng)態(tài)隱私保護(hù)框架，結(jié)合隨機(jī)模型檢驗(yàn)與運(yùn)行時(shí)驗(yàn)證技術(shù)，構(gòu)建基于知識(shí)邏輯拓展的離散時(shí)間馬爾科夫鏈模型，將用戶隱私設(shè)置形式化表述為概率計(jì)算樹(shù)邏輯，同時(shí)通過(guò)運(yùn)行時(shí)驗(yàn)證中的參數(shù)化和監(jiān)控技術(shù)實(shí)現(xiàn)用戶隱私信息的保護(hù)。實(shí)驗(yàn)結(jié)果表明，與靜態(tài)隱私保護(hù)框架相比，該動(dòng)態(tài)隱私保護(hù)框架在提高用戶隱私策略靈活性的同時(shí)降低了隱私泄露風(fēng)險(xiǎn)。但該框架中的動(dòng)態(tài)隱私策略僅針對(duì)時(shí)間、地點(diǎn)和事件的觸發(fā)條件，下一步將優(yōu)化動(dòng)態(tài)隱私保護(hù)框架，擴(kuò)展動(dòng)態(tài)隱私策略的應(yīng)用范圍，以滿足多用戶的個(gè)性化隱私保護(hù)需求。