基于隨機模型檢驗的社交網絡隱私保護研究

劉 陽，高世國

（南京財經大學信息工程學院，南京 210046）

0 概述

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

社交網絡用戶行為的不確定性和網絡配置的不一致性，導致傳統檢驗模型無法應對復雜社交網絡的隨機特性。隨機檢驗模型是使用模型檢驗方法對帶有隨機行為的復雜系統進行定量驗證和分析［5-7］，而運行時驗證主要是針對復雜動態系統設計的驗證技術，但其也面臨隨著運行時間的不斷增加，所需的計算能力呈幾何式增長的問題［8］。本文提出一種動態隱私保護框架，將隱私策略設置作為觸發條件，通過運行時驗證中的參數化和監控技術對用戶隱私信息進行保護。

1 相關工作

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

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

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

針對社交網絡中圖片分享造成的隱私泄露問題，文獻［22］結合靜態與動態隱私規約建立形式化隱私語言框架，并通過經典模型檢驗方法對社交網絡的隱私保護問題進行深入研究。本文受其啟發，借鑒隱私規約的形式化方法，在考慮社交網絡模型特性的基礎上，對其形式化隱私語言框架進行適應性改進，引入概率因子并結合運行時驗證的相關監控技術，解決社交網絡中運行時用戶的隱私信息泄露驗證和保護問題，滿足用戶的動態隱私設置需求。

2 動態隱私保護框架

當前社交網絡隱私策略缺乏穩定性、靈活性和一致性，其主要原因是由于社交網絡架構對于數據庫的權限過于集中化。如圖1 所示，各終端用戶保存隱私設置發送給Web 服務器或轉發設備，Web 服務器或轉發設備在接收到相應的隱私設置數據后經過數據融合保存至云存儲機架集群中，整個社交網絡系統依據云數據庫中存儲的關系數據執行相應的權限設置，實現社交網絡中所有用戶的隱私設置。

圖1 社交網絡架構Fig.1 Social network architecture

由于社交網絡用戶的隱私需求不斷增加，當前社交網絡架構提供的靜態隱私策略已經無法滿足用戶的隱私需求，同時在大數據環境下，數據分布廣泛，多源數據融合過程可能存在一定的隨機性，進一步增加了用戶隱私信息泄露的風險。為使社交網絡的隱私設置更加靈活和安全，本文提出動態隱私保護框架，通過在終端植入監控器獲取社交網絡運行時參數進行運行時驗證，同時對傳統靜態隱私規約進行分解預處理，在傳統靜態隱私規約的基礎上增加觸發條件a，將動態隱私規約形式化表述為a→b的表達式形式，當前置條件滿足a時，隱私設置會自動更改為b，通過監控器來監控用戶所在社交網絡是否滿足a來動態執行隱私設置b。通過對隱私規約的預處理可大幅降低運行時驗證的復雜度，極大降低所需的運算能力。動態隱私保護框架如圖2所示。

圖2 動態隱私保護框架Fig.2 Dynamic privacy protection framework

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

3 基于KBL 的PCTL 轉換算法

3.1 KBL 定義及相關概念

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

3.2 PCTL 轉換算法

由于利用KBL 表述用戶知識庫狀態，因此通過判斷知識庫狀態可驗證隱私信息是否泄露，但是KBL 無法應用于隨機模型檢驗及使用PRISM 工具進行自動化驗證，本文設計一種將KBL 轉換為PCTL 的算法，通過該算法可將KBL 轉換成在PRISM 進行驗證的PCTL 語法。

算法1基于KBL 的PCTL 轉換算法

通過該算法可實現以下功能：1）基于監控器參數生成用戶社交關系圖；2）基于用戶屏蔽對象實現不同用戶的知識庫更新策略；3）基于用戶知識庫確定用戶狀態，依據用戶狀態確定可達目標集合s；4）實現引理1 及引理2 中基于KBL 的邏輯推理規則。

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

證明令M=＜S，＜action，p＞，linit，AP，L＞，B∈s是目標狀態集合，最終到達目標狀態集合B記作?B，為證明到達目標狀態是可終止的，需證?B的路徑集合是可計算的。

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

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

2）在無窮路徑狀態下，對于任意狀態s∈S，令ps代表從狀態s出發到達B狀態集合的概率：若B是從s出發不可到達的，則ps=0；若s∈B，則ps=1；若ps＞0，則說明從狀態s出發到達B狀態集合是可到達的。因此，對于任意狀態s∈S?B均可到達B需滿足：

對于任意狀態s∈S?B，若s是可到達B的，則可分為以下兩種情況：

（1）從s到B是一步之內可到達的，情況如式（2）右邊第2 項所示：設u是屬于集合B內的狀態，則在該情況下的路徑為s→u。

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

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

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

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

綜上所述，當路徑為有限路徑時到達集合B的概率是一個有關M的?代數，當路徑為無限路徑時到達集合B的概率是求解式（4）的線性最優解，因此基于KBL 的DTMC 模型的可達性概率是可計算的，該模型為可終止得以證明。

定理2基于KBL 的DTMC 模型保證在PCTL轉換算法執行前后及執行過程中都可以正確迭代用戶知識庫狀態。

證明使用循環不變式證明PCTL 轉換算法的正確性，需要證明在算法執行前、執行時及結束時均能正確迭代用戶知識庫狀態。

1）算法執行前：循環不變式成立，監控器中的關系列表、圖G中所有用戶節點、用戶知識庫kb、集合S均為?，即在循環開始前滿足監控器參數與用戶社交圖的對應關系，屏蔽對象、post 函數參數為?且滿足用戶知識庫的迭代策略，圖G中所有節點狀態均為﹁Kuφ，保證用戶狀態的分類結果正確。

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

3）算法結束時：第1 個while 循環的終止條件list=?，此時i=0，u=len(list)-i，即u=len(list)，說明列表中的所有相關用戶已被完全生成圖G中的節點。第2 個while 循環的終止條件是block(i)=?，當block(i)=?時，此時有i=len(block)，設m為圖G中所有的節點數目，根據算法1 的第14 行、第15 行可知m=u+i，即滿足功能2；對于第3 個for 循環的終止條件為遍歷完所有圖G中的節點，此時集合S中的狀態為滿足目標的狀態集合。綜上，基于KBL 的PCTL 轉換算法的正確性得以證明。

依據算法1 的第2 行～第11 行，遍歷監控器的整個用戶關系列表，創建社交關系圖，所需的時間復雜度為O(n2)，其中n為關系列表中的用戶個數，第13 行～第24 行遍歷圖G，通過廣度優先搜索為每個用戶設置知識庫的更新策略，因此時間復雜度為O(n2)，n為圖G中的節點個數。綜上，基于KBL 的PCTL 轉換算法的時間復雜度為O(n2)。

引理1若用戶設置SGφ，則分組G中至少有一個用戶的知識庫狀態為Kiφ，形式化為SGφ→∨i∈G Kiφ。

證明

1）算法執行前：此時未創建用戶關系節點圖，SGφ=?，所有用戶知識庫Kiφ=?，i表示所有用戶，滿足引理1。

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

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

引理2若用戶設置EGφ，則分組G中每一個用戶的知識庫狀態為Kiφ，形式化為EGφ→∧i∈G Kiφ。

證明

1）算法執行前：此時未創建用戶關系節點圖，EGφ=?，所有用戶知識庫Kiφ=?，i表示所有用戶，滿足引理2。

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

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

4 隱私規約的形式化表述

通過算法1 轉換后的PCTL 語義如下：

其中，φ表示狀態公式，a∈AP 表示原子命題，～∈｛＜，≤，＞，≥｝，ψ表示路徑公式。轉換后的PCTL 引入了K算子，通過K算子來描述用戶的知識庫狀態，對于給定的社交網絡模型以及隱私設置π，有狀態s∈S，狀態公式φ滿足如下關系：

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

路徑公式ψ的滿足如下關系：

其中，路徑π=s0，s1，…，si，i表示整數，π[i]表示路徑π的第i個狀態。

4.1 靜態隱私規約的形式化表述

為滿足用戶的隱私保護需求，在形式化表述的靜態隱私規約的基礎上加入[ ]標記，在KBL 的外面加上[ ]標記表示該項隱私設置由該用戶設置。本文通過集合spec()記錄用戶u設置的隱私規約，記為spec(u)，假設靜態隱私規約1 為如果用戶A暫時屏蔽了用戶B，即用戶A不希望用戶B知道其所發的某一條動態post(φ)，使用帶[ ]標記的公式進行表示：

1）對于用戶A：用戶A不希望用戶B知道其所發的某一條動態φ，For agentAsatisfy：。

2）對于社交網絡模型SN 而言，整個系統需求要求用戶B知道用戶A所發的某一條動態φ的概率不高于0.01，For module SN satisfy：。

為表述方便，靜態隱私規約1 也可以表述為For module SN satisfy：。通過以上方式可對SN 中用戶設置的靜態隱私規約進行形式化表述。

4.2 動態隱私規約的形式化表述

動態隱私與靜態隱私的區別在于動態隱私可根據預先設定的觸發條件對隱私設置進行更改，靜態隱私則是如果用戶不主動進行更改則一直維持該設置，因此本文將動態隱私表示為a→b的形式，即如果滿足條件a，那么就執行b，將動態隱私設置分解為a→b的形式并依據觸發條件的不同，將動態隱私設置主要分為基于時間的動態隱私設置（BOT）、基于地點的動態隱私設置（BOL）、基于事件的動態隱私設置（BOE）3 類，具體為：

1）基于時間的動態隱私設置。觸發條件為時間，當系統內部時間滿足條件a時會觸發條件b，定義動態隱私規約1 為在社交網絡中某一用戶u希望對其工作時間和非工作時間進行區分，非工作時間避免同事們打擾，可設置如下的BOT 規則：在非工作時間第1 天晚上20：00 至第2 天早上08：00，不希望college列表中的同事們看到自己的某一條動態φ，用PCTL可表示為[ ]20：00≤timer≤08：00→。

2）基于地點的動態隱私設置。觸發條件為地點，當系統內部定位的地點滿足條件時會觸發條件，定義動態隱私規約2 為在社交網絡中某一用戶u希望對其工作地點和非工作地點進行區分，只在工作地點（company）所發表的動態才會被同事們所看到，可設置如下BOL 規則：只在工作地點所發表的動態可被college 列表中的同事所看見，用PCTL 可表示為。

3）基于事件的動態隱私設置。觸發條件為事件，當系統內檢測到滿足條件的事件發生時就會觸發條件，定義動態隱私規約3 為某一用戶u希望能更加靈活地管理自己的朋友列表，為防止自己的動態被人無限制轉發，可設置如下BOE 規則：只有當好友a點贊并評論自己所發的某條動態后，該好友才有權限轉發該動態，否則不給予其轉發該條動態的權限，用PCTL 可表示為[ ]（like(φ)∧comment(φ)=true）∈a→reposted(φ) ?a。

由于動態隱私設置需要依據觸發條件來動態更改用戶的社交網絡結構，因此本文需先對靜態隱私設置進行更改以滿足動態隱私需求。設置一個臨時屏蔽分組（block），在分組中存儲不滿足動態隱私規范而被臨時屏蔽的好友，基于時間的動態隱私保護框架如圖3 所示。

圖3 基于時間的動態隱私保護框架Fig.3 Dynamic privacy protection framework based on time

當不滿足遷移條件的好友被移到block 分組時，若一旦監控器監測到條件滿足，則會將block 分組中的好友移回原分組。基于地點和事件的動態隱私保護框架如圖4、圖5 所示，其中，like（φ）=μ表示用戶μ對動態φ進行點贊，comment（φ）=μ表示用戶μ對動態φ進行評論，reposted（φ）=μ表示用戶μ對動態φ進行轉發。

圖4 基于地點的動態隱私保護框架Fig.4 Dynamic privacy protection framework based on location

圖5 基于事件的動態隱私保護框架Fig.5 Dynamic privacy protection framework based on event

5 社交網絡系統的形式化建模

5.1 基于靜態隱私保護框架的DTMC 模型

對于靜態隱私保護框架，終端用戶設置隱私規約后發送給服務器或轉發設備，服務器接受隱私規約后進行數據融合更新，本文對靜態隱私保護框架的DTMC建模如圖6 所示。若狀態間未標明轉移概率，則默認其轉移概率為1，系統狀態及其含義如表1 所示。

圖6 基于靜態隱私保護框架的DTMC 模型Fig.6 DTMC model based on static privacy protection framework

表1 系統狀態及其含義Table 1 System status and its meaning

社交網絡用戶將新的隱私設置發送給服務器，但服務器和用戶之間的通信協議存在一定的隨機性，即服務器可能有p1的概率接收數據失敗。由于社交網絡用戶非常多，服務器在短時間內接收的用戶隱私設置無法同一時間立即完成更新，因此當服務器正在更新設置時，剛接收到的數據有p2的概率進入服務器忙碌狀態，需要服務器等待重新接收數據進行處理。當服務器處于空閑狀態并接收數據后開始更新操作，由于更新操作建立在通信協議的基礎上，因此更新操作有p3的概率更新失敗。

5.2 基于動態隱私保護框架的DTMC 模型

本文根據動態隱私保護框架，將其分為社交網絡模型SN 和隱私監控器P-monitor 兩部分進行建模。社交網絡模型如圖7 所示，其中實線單向箭頭、實線雙向箭頭、虛線單向箭頭、點劃線單向箭頭分別代表用戶節點之間的好友、同事、屏蔽、陌生人4 種社交關系。

圖7 社交網絡模型Fig.7 Social network model

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

將隱私監控器P-monitor 植入社交網絡模型中，結合隨機模型檢驗工具，構建基于動態隱私保護框架的DTMC 模型，如圖8 所示。

圖8 基于動態隱私保護框架的DTMC 模型Fig.8 DTMC model based on dynamic privacy protection framework

在動態隱私保護框架中發送給服務器更新隱私規約這部分內容與靜態隱私保護框架相同，不同的是在動態隱私保護框架下，用戶會將動態隱私策略會發送給P-monitor。P-monitor 與用戶之間是一一對應關系，即每個使用靜態隱私策略的用戶都會在用戶終端生成一個P-monitor，P-monitor 可以執行服務器接收數據的功能，由于P-monitor 與用戶之間的通信也建立在通信協議的基礎上，因此P-monitor 有p4的概率未接受用戶的隱私規約，但是當P-monitor接受新的隱私規約后就立即對社交網絡進行監控，因此不會出現更新失敗的情況。

6 實驗結果與分析

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

對于動態隱私規約1，P-monitor輸入參數如表2 所示，其中，User 表示被監控的用戶，timer 表示時間記錄器，location 表示地點記錄器，post表示被監控用戶是否發表動態，reposted 表示對動態進行轉發的用戶集合，like 表示被對動態進行點贊的用戶集合，dislike 表示對動態不喜歡的用戶集合，comment 表示對動態進行評論的用戶集合，表示最終用戶Bob知道被監控對象Alice 發表動態的概率。

表2 動態隱私規約1 的P-monitor 輸入參數Table 2 P-monitor input parameters of dynamic privacy specification 1

通過實驗數據發現，在服務器和監控器的容錯概率下，使用監控器來保存動態隱私設置要比使用服務器來更新靜態隱私設置的隱私泄露風險降低50%，這主要是因為兩者架構不同，服務器是針對所有用戶，存在擁塞和延遲，并且出錯概率也大幅提高，但是監控器是針對個人用戶，不存在擁塞和延遲，所以可以大幅降低隱私泄露風險。

為進一步驗證動態隱私策略和靜態隱私策略在時間維度上的隱私泄露風險，設定每一步長的reward 為1，其中reward 為執行圖遍歷算法的花費，通過實驗對比分析不同時間維度下動態和靜態隱私泄露風險，實驗結果如圖9 所示。靜態DTMC 模型內部各個節點的狀態變化如圖10 所示，其中，User表示被監控用戶的節點狀態，Agent 表示代理服務器的節點狀態。

圖9 靜態與動態隱私策略的隱私泄露風險對比Fig.9 Comparison of privacy disclosure risks between static and dynamic privacy strategy

圖10 靜態DTMC 模型節點狀態遷移Fig.10 Node state transition of static DTMC model

實驗結果表明，在極短時間內動態隱私規約相比靜態隱私規約出現了用戶隱私信息泄露的情況，產生該情況的主要原因為動態隱私設置采用監控器直接對用戶隱私設置進行保存和監控，同時考慮到監控器在接收用戶數據信息時會產生一定的失敗概率，并且監控器發生錯誤的情況要比服務器更快，因此在極短時間內，若監控器發生錯誤，則會比靜態隱私保護框架下服務器發生錯誤的時間更短。但是從長時間而言，在穩定狀態下動態隱私保護框架比靜態隱私保護框架的用戶隱私信息泄露風險更低，并且動態隱私規約也更靈活性。

對于動態隱私規約3，由于在動態隱私保護框架中隱私泄露的風險只與是否成功接收到被監控用戶發送的數據有關，因此本文只驗證在P-monitor 未正常更新的情況下，由于用戶的隨機行為所產生的隱私泄露概率。假定用戶設置的動態隱私設置未成功保存至P-monitor中，在該假設前提下P-monitor輸入參數如表3所示。動態DTMC 模型內部各節點的狀態變化如圖11所示，其中，Bob 表示用戶Bob 的節點狀態，Update 表示監控器執行用戶隱私設置的狀態。

表3 動態隱私規約3 的P-monitor 輸入參數Table 3 P-monitor input parameters of dynamic privacy specification 3

圖11 動態DTMC 模型節點狀態遷移Fig.11 Node state transition of dynamic DTMC model

實驗結果表明，本文設計的動態隱私保護框架通過植入P-monitor 進行用戶隱私設置，但不發送到服務器端，其主要原因為服務器端存在的接收失敗、忙碌、更新失敗等隨機故障，會導致隱私泄露風險遠大于用戶需求。基于P-monitor 的動態隱私保護框架通過動態的隱私設置，提高社交網絡隱私設置的靈活性，并基于P-monitor 與用戶間一對一的監控結構，解決了服務器端存在的接收失敗、忙碌、更新失敗等隨機故障，降低了用戶隱私泄露風險。

7 結束語

本文提出一種面向社交網絡的動態隱私保護框架，結合隨機模型檢驗與運行時驗證技術，構建基于知識邏輯拓展的離散時間馬爾科夫鏈模型，將用戶隱私設置形式化表述為概率計算樹邏輯，同時通過運行時驗證中的參數化和監控技術實現用戶隱私信息的保護。實驗結果表明，與靜態隱私保護框架相比，該動態隱私保護框架在提高用戶隱私策略靈活性的同時降低了隱私泄露風險。但該框架中的動態隱私策略僅針對時間、地點和事件的觸發條件，下一步將優化動態隱私保護框架，擴展動態隱私策略的應用范圍，以滿足多用戶的個性化隱私保護需求。