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服务器或转发设备在接收到相应的隐私设置数据后经过数据融合保存至云存储机架集群中，整个社交网络系统依据云数据库中存储的关系数据执行相应的权限设置，实现社交网络中所有用户的隐私设置。

由于社交网络用户的隐私需求不断增加，当前社交网络架构提供的静态隐私策略已经无法满足用户的隐私需求，同时在大数据环境下，数据分布广泛，多源数据融合过程可能存在一定的随机性，进一步增加了用户隐私信息泄露的风险。为使社交网络的隐私设置更加灵活和安全，本文提出动态隐私保护框架，通过在终端植入监控器获取社交网络运行时参数进行运行时验证，同时对传统静态隐私规约进行分解预处理，在传统静态隐私规约的基础上增加触发条件a，将动态隐私规约形式化表述为a→b的表达式形式，当前置条件满足a时，隐私设置会自动更改为b，通过监控器来监控用户所在社交网络是否满足a来动态执行隐私设置b。通过对隐私规约的预处理可大幅降低运行时验证的复杂度，极大降低所需的运算能力。动态隐私保护框架如图 2所示。

动态隐私保护框架主要是针对社交网络隐私设置不灵活和难以验证的问题提出的解决方案。本文使用随机模型检验与运行时检验中的监控技术相结合的方法，将整个社交网络模型构建为一个基于知识逻辑（Knowledge Based Logic，KBL）拓展的离散时间马尔科夫链（Discrete Time Markov Chains，DTMC）模型，将社交网络用户的隐私设置形式化表述为概率计算树逻辑（Probabilistic Computation Tree Logic，PCTL）^[23]，同时加入运行时验证理论中的参数化技术。通过向待验证的社交网络系统植入监控器P-monitor，获取待监控用户进行验证时所需的隐私数据作为参数传入随机模型检验工具，然后依据事先给定的隐私规约，若满足规约则继续监控，若不满足则给出反例和提示，提醒用户进行相应的更改和操作，以防止隐私信息泄露。

3 基于KBL的PCTL转换算法 3.1 KBL定义及相关概念

定义1（KBL）给定非空的命题集合P，用户i，$ g\in \mathrm{A}\mathrm{g} $，$ \mathrm{A}\mathrm{g}\mathrm{为}\mathrm{用}\mathrm{户}\mathrm{集}\mathrm{合} $，命题$ p\in P $，分组$ G\in \mathrm{A}\mathrm{g} $，路径公式$ \gamma \colon\colon =\neg \gamma \left|\gamma \wedge \gamma \left|φ \right.\right. $，事件$ φ \colon\colon =p\left|\right.φ \wedge φ \left|\neg φ \right. $ $ \left|{K}_{i}φ \right| $ $ {E}_{G}φ \left|{S}_{G}φ \right. $，KBL相关模态的定义如下：

$ {K}_{i}φ \left(\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{i}\mathrm{c}\,\,\mathrm{k}\mathrm{n}\mathrm{o}\mathrm{w}\mathrm{l}\mathrm{e}\mathrm{d}\mathrm{g}\mathrm{e}\right):\mathrm{a}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{t}\,i\,\mathrm{k}\mathrm{n}\mathrm{o}\mathrm{w}\mathrm{s}\,φ $

$ {E}_{G}φ \left(\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{o}\mathrm{n}\,\mathrm{k}\mathrm{n}\mathrm{o}\mathrm{w}\mathrm{l}\mathrm{e}\mathrm{d}\mathrm{g}\mathrm{e}\right):\\ \mathrm{e}\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{y}\,\mathrm{a}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{t}\,\mathrm{i}\mathrm{n}\,\mathrm{g}\mathrm{r}\mathrm{o}\mathrm{u}\mathrm{p}\,G\,\mathrm{k}\mathrm{n}\mathrm{o}\mathrm{w}\mathrm{s}φ $

$ {S}_{G}φ \left(\mathrm{s}\mathrm{o}\mathrm{m}\mathrm{e}\mathrm{o}\mathrm{n}\mathrm{e}\,\mathrm{k}\mathrm{n}\mathrm{o}\mathrm{w}\mathrm{l}\mathrm{e}\mathrm{d}\mathrm{g}\mathrm{e}\right):\\ \mathrm{s}\mathrm{o}\mathrm{m}\mathrm{e}\mathrm{o}\mathrm{n}\mathrm{e}\,\mathrm{a}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{t}\,\mathrm{i}\mathrm{n}\,\mathrm{g}\mathrm{r}\mathrm{o}\mathrm{u}\mathrm{p}\,G\,\mathrm{k}\mathrm{n}\mathrm{o}\mathrm{w}\mathrm{s}\,φ $

对于社交网络模型$ \mathrm{S}\mathrm{N}=〈w, {\left\{{R}_{i}\right\}}_{i\in C}, v, \mathrm{k}\mathrm{b}, \pi 〉 $，其中：w为非空字母表集合，每个字母代表用户集合Ag中的用户；$ {\left\{{R}_{i}\right\}}_{i\in C} $为二元关系集合，$ {R}_{i}\in w\times w $表示用户间的关系；v为值函数，返回值是真命题集合，如$ v:w\to {2}^{p} $；kb为基于知识的逻辑函数，表示每个代理均提供了一组累积的知识，这些知识存储在代理知识库中；$ \pi $为值函数，返回值是给定用户所设置的隐私策略，如$ \pi :w\to {2}^{{\mathit{\Pi}} }，{\mathit{\Pi}} \mathrm{表}\mathrm{示}\mathrm{用}\mathrm{户}\mathrm{策}\mathrm{略}\mathrm{集}\mathrm{合} $。用户$ i, j, $ $ u\in \mathrm{A}\mathrm{g} $，分组集合$ G\in \mathrm{A}\mathrm{g} $，给定某一事件$ φ $满足以下关系：

$ \mathrm{S}\mathrm{N}, u\models \neg p\,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\neg p\in v\left(u\right) $

$ \mathrm{S}\mathrm{N}, u\models p\,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,p\in v\left(u\right) $

$ \mathrm{S}\mathrm{N}, u\models \neg φ \,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\mathrm{S}\mathrm{N}, u\models \neg φ $

$ \mathrm{S}\mathrm{N}, u\models \gamma \wedge φ \,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\mathrm{S}\mathrm{N}, u\models \gamma \,\mathrm{a}\mathrm{n}\mathrm{d}\,u\models φ $

$ \mathrm{S}\mathrm{N}, u\models {K}_{i}φ \,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\left\{\begin{array}{l}φ \in \mathrm{k}\mathrm{b}\left(i\right)，φ ={K}_{j}φ \text{'}, j\in \mathrm{A}\mathrm{g}\\ \mathrm{S}\mathrm{N}, i\models φ \end{array}\right. $

$ \mathrm{S}\mathrm{N}, u\models {E}_{G}φ \,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\,\mathrm{S}\mathrm{N}, i\models {K}_{i}φ \,\mathrm{f}\mathrm{o}\mathrm{r}\,\mathrm{a}\mathrm{l}\mathrm{l}\,i\,\mathrm{i}\mathrm{n}\,G $

$ \mathrm{S}\mathrm{N}, u\models {S}_{G}φ \,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\mathrm{S}\mathrm{N}, i\models {K}_{i}φ \,\mathrm{f}\mathrm{o}\mathrm{r}\,\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}\,\mathrm{e}\mathrm{x}\mathrm{i}\mathrm{s}\mathrm{t}\,i\,\mathrm{i}\mathrm{n}\,G $

3.2 PCTL转换算法

由于利用KBL表述用户知识库状态，因此通过判断知识库状态可验证隐私信息是否泄露，但是KBL无法应用于随机模型检验及使用PRISM工具进行自动化验证，本文设计一种将KBL转换为PCTL的算法，通过该算法可将KBL转换成在PRISM进行验证的PCTL语法。

算法1  基于KBL的PCTL转换算法

输入  P-monitor：< User，timer，location，list，operation >

输出  $ \mathrm{s}\mathrm{e}\mathrm{t}s $

1.let set s=Null//设置初始满足状态集合s为$ \mathrm{\varnothing } $

2.//according to the parameters create graph G（node，kb）

3.$ \mathrm{f}\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\,\mathrm{C}\mathrm{r}\mathrm{e}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{N}\mathrm{o}\mathrm{d}\mathrm{e}\left(\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\right) $//依据监控器list参数创建//用户节点

4.$ \mathrm{f}\mathrm{o}\mathrm{r}\,\mathrm{e}\mathrm{a}\mathrm{c}\mathrm{h}\,\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\,\mathrm{d}\mathrm{o} $

5.$ \mathrm{n}\mathrm{o}\mathrm{d}\mathrm{e}=\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\,\mathrm{a}\mathrm{n}\mathrm{d}\,\mathrm{k}\mathrm{b}=\mathrm{\varnothing } $

6.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{f}\mathrm{o}\mathrm{r} $

7.$ \mathrm{r}\mathrm{e}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{n}\,\mathrm{G} $

8.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{f}\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n} $

9.$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e}\left(\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\ne \mathrm{N}\mathrm{u}\mathrm{l}\mathrm{l}\right)\mathrm{d}\mathrm{o} $//创建用户节点

10.$ \mathrm{C}\mathrm{r}\mathrm{e}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{N}\mathrm{o}\mathrm{d}\mathrm{e}\left(\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\right) $

11.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $

12.$ {\mathrm{i}\mathrm{f}\,\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}}$(φ)= True//依据监控器post参数及block参//数设置权限

13.$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e}\,\mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(\mathrm{i}\right)\ne \mathrm{\varnothing }\,\mathrm{d}\mathrm{o}\,\{ $

14.$ \mathrm{s}\mathrm{e}\mathrm{t}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\,\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{a}\mathrm{c}\mathrm{y}{\mathrm{S}}_{\mathrm{u}\in \mathrm{g}}$ φ in G

15.$ \mathrm{f}\mathrm{o}\mathrm{r}\,\mathrm{e}\mathrm{a}\mathrm{c}\mathrm{h}\,\mathrm{n}\mathrm{o}\mathrm{d}\mathrm{e}\,\mathrm{i}\mathrm{n}\,\mathrm{g}\,\mathrm{a}\mathrm{n}\mathrm{d}\,\mathrm{n}\mathrm{o}\mathrm{d}\mathrm{e}\ne \mathrm{i}\,\mathrm{d}\mathrm{o}\{ $

16.$ \mathrm{k}\mathrm{b}=\mathrm{k}\mathrm{b}\bigcup$ φ}

17.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{f}\mathrm{o}\mathrm{r}\,\} $

18.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $

19.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{f} $

20.//依据监控器post参数及block参数设置权限

21.$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e}\,\mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(\mathrm{i}\right)=\mathrm{\varnothing }\,\mathrm{d}\mathrm{o}\,\{ $

22.$ \mathrm{s}\mathrm{e}\mathrm{t}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\,\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{a}\mathrm{c}\mathrm{y}{\mathrm{E}}_{\mathrm{u}\in \mathrm{g}} $ φ in G

23.$ \mathrm{f}\mathrm{o}\mathrm{r}\,\mathrm{e}\mathrm{a}\mathrm{c}\mathrm{h}\,\mathrm{n}\mathrm{o}\mathrm{d}\mathrm{e}\,\mathrm{i}\mathrm{n}\,\mathrm{G}\,\mathrm{d}\mathrm{o}\,\{ $

24.$ \mathrm{k}\mathrm{b}=\mathrm{k}\mathrm{b}\bigcup $ φ

25.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{f}\mathrm{o}\mathrm{r}\} $

26.$ \mathrm{e}\mathrm{n}\mathrm{d}\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $

通过该算法可实现以下功能：1）基于监控器参数生成用户社交关系图；2）基于用户屏蔽对象实现不同用户的知识库更新策略；3）基于用户知识库确定用户状态，依据用户状态确定可达目标集合$ s $；4）实现引理1及引理2中基于KBL的逻辑推理规则。

定理1  基于KBL的DTMC模型为可终止。

证明  令M= < S，< action，p > ，l_init，AP，L > ，$ B\in s $是目标状态集合，最终到达目标状态集合B记作$ \vdash B $，为证明到达目标状态是可终止的，需证$ \vdash B $的路径集合是可计算的。

1）在有穷状态下，可知路径集合$ \vdash B $满足Cyl（s₀，s₁，…，s_n），其中（s₀，s₁，…，s_n）是一个属于模型M的初始路径片段，满足（s₀，s₁，…，s_n）$ \notin B $，s_{n$ \in B $}所有的路径集合由$ {P}_{\mathrm{a}\mathrm{t}\mathrm{h}\mathrm{s}}\left(M\right)\bigcap \left(S\setminus B\right)\times B $给出，由于路径是有穷的，因此到达目标状态集合$ B $的路径长度是可数的，属于$ M $的$ \partial $代数，同时由于这些路径集合是成对不相交的，因此最终到达集合$ M $的概率计算公式为：

$ p= \mathrm{P}{\mathrm{r}}^{M}\left(◊B=\sum\limits _{{s}_{0}, {s}_{1}, \cdots , {s}_{n}\in {P}_{\mathrm{a}\mathrm{t}\mathrm{h}\mathrm{s}}\left(M\right)\bigcap \left(S\setminus B\right)\times B}\mathrm{P}{\mathrm{r}}^{M}\left(\mathrm{C}\mathrm{y}\mathrm{l}\left({s}_{0}, {s}_{1}, \cdots , {s}_{n}\right)\right)\right) $

(1)

其中，$ \mathrm{P}{\mathrm{r}}^{M} $代表在马尔科夫链模型M中满足某条路径集合的概率，P_aths为最终到达节点s的路径集合。

2）在无穷路径状态下，对于任意状态$ s\in S $，令$ {p}_{s} $代表从状态$ s $出发到达$ B $状态集合的概率：若$ B $是从$ s $出发不可到达的，则$ {p}_{s}=0 $；若s$ \in B $，则$ {p}_{s}=1 $；若$ {p}_{s}>0 $，则说明从状态$ s $出发到达$ B $状态集合是可到达的。因此，对于任意状态$ s\in S\setminus B $均可到达$ B $需满足：

$ {p}_{s}=\sum\limits _{t\in S\setminus B}P\left(s, t\right)\cdot {p}_{t}+\sum\limits _{u\in B}P\left(s, u\right) $

(2)

对于任意状态$ s\in S\setminus B $，若$ s $是可到达$ B $的，则可分为以下两种情况：

（1）从$ s $到$ B $是一步之内可到达的，情况如式（2）右边第2项所示：设$ u $是属于集合$ B $内的状态，则在该情况下的路径为$ s\to u $。

（2）从$ s $到$ B $是非一步之内可到达的，情况如式（2）右边第1项所示：设$ t $是从$ s $出发到达$ u $的中间状态，$ u $是属于集合$ B $内的状态，则在该情况下的路径为$ s\to t\to \cdots \to u $，令$ S\text{'}=\mathrm{P}\mathrm{r}\left(B\right)\setminus B $代表满足路径片段条件为$ {s}_{0}, {s}_{1}, \cdots , {s}_{n}(n>0 $，$ {s}_{0}=S, {s}_{n}\in B $）的状态集合。对于所有的状态$ s\in S\setminus B $，其到达$ B $的可达性概率$ {p}_{s} $可记为向量$ {\mathit{\boldsymbol{X}}}=（{p}_{s}{）}_{s\in S\setminus B} $并得到：

$ {\mathit{\boldsymbol{X}}}={\mathit{\boldsymbol{A}}}{\mathit{\boldsymbol{X}}}+{\mathit{\boldsymbol{b}}} $

(3)

其中，A代表$ s\in S\setminus B $的所有状态迁移矩阵，$ {\mathit{\boldsymbol{b}}} $是所有位于集合$ B $外可一步到达$ B $的状态集合的迁移向量。式（3）移项可得式（4）：

$ \left({\mathit{\boldsymbol{I}}}-{\mathit{\boldsymbol{A}}}\right)\cdot {\mathit{\boldsymbol{X}}}={\mathit{\boldsymbol{b}}} $

(4)

其中，$ {\mathit{\boldsymbol{I}}} $是一个|$ s\text{'} $|$ \times \left|s\text{'}\right| $的基数恒等矩阵。因此，该过程是对方程组$ \left({\mathit{\boldsymbol{I}}}-{\mathit{\boldsymbol{A}}}\right)\cdot {\mathit{\boldsymbol{X}}}={\mathit{\boldsymbol{b}}} $的线性求解过程：当$ {\mathit{\boldsymbol{I}}}-{\mathit{\boldsymbol{A}}} $为非奇异矩阵，必然有唯一解；当$ {\mathit{\boldsymbol{I}}}-{\mathit{\boldsymbol{A}}} $为奇异矩阵，有多解，此时该求解问题转化为求解期望的概率向量的最优解问题，可通过近似迭代方法计算出概率向量$ {\mathit{\boldsymbol{b}}} $，例如高斯消元法。

设$ M=\left(S, P, {l}_{\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}}, \mathrm{A}\mathrm{P}, L\right) $为一个马尔科夫链$ \left(\mathrm{M}\mathrm{C}\right) $，$ B, C\in S $，假设事件最终到达状态B，经历如下有穷路径片段：先经过状态集合C然后到达最终状态s，即$ {l}_{\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}}\to \cdots \to C\to s $，s$ \in B $，对于该假设事件可记作$ C\bigcup B $，已知$ ◊B $严格满足于$ S\bigcup B $，即对于$ n\ge 0 $，事件$ C{\bigcup }^{\le n}B $与事件$ C\bigcup B $具有相同的路径，但事件$ C{\bigcup }^{\le n}B $要求经过前驱状态集合$ B $，因此$ ◊B $的路径片段$ {s}_{0}, {s}_{1}, \cdots ，{s}_{k} $满足$ k\le n, {s}_{i}\in C, {s}_{k}\in B $，$ 0\le i\le k $，可将$ S $分割成$ {S}_{=0}\mathrm{、}{S}_{=1}\mathrm{和}{S}_{=?} $，分为以下3种情况：①$ B\subseteq $ $ {S}_{=0}\subseteq \{s\in S|\mathrm{P}\mathrm{r}\left(s\models C\bigcup B\right)=1\} $；②$ S\setminus (C\bigcup B)\subseteq {S}_{=0}\subseteq $ $ \{s\in S| $ $ \mathrm{P}\mathrm{r}\left(s\models C\bigcup B\right)=0\} $；③$ {S}_{=?}=S\setminus ({S}_{=0}\bigcup {S}_{=1}) $。情况1和情况2显然很容易得到求解结果。情况3可通过高斯消元法得到二次型矩阵$ {\mathit{\boldsymbol{A}}}=(P{(s, t))}_{s, t\in {S}_{=?}} $，通过同样的方法向量$ {\mathit{\boldsymbol{b}}} $可定义为$ ({b}_{s}{)}_{s\in {S}_{=?}} $，$ {b}_{s}=P(s, S=1) $，最终通过求解概率$ \mathrm{P}\mathrm{r}{\left(s\models C\bigcup B\right)}_{s\in S} $的最小不动特征点来求解该方程组的最优解。

综上所述，当路径为有限路径时到达集合$ B $的概率是一个有关$ M $的$ \partial $代数，当路径为无限路径时到达集合$ B $的概率是求解式（4）的线性最优解，因此基于KBL的DTMC模型的可达性概率是可计算的，该模型为可终止得以证明。

定理2  基于KBL的DTMC模型保证在PCTL转换算法执行前后及执行过程中都可以正确迭代用户知识库状态。

证明  使用循环不变式证明PCTL转换算法的正确性，需要证明在算法执行前、执行时及结束时均能正确迭代用户知识库状态。

1）算法执行前：循环不变式成立，监控器中的关系列表、图G中所有用户节点、用户知识库kb、集合S均为Ø，即在循环开始前满足监控器参数与用户社交图的对应关系，屏蔽对象、$ \mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t} $函数参数为Ø且满足用户知识库的迭代策略，图G中所有节点状态均为$ \neg {K}_{u}φ $，保证用户状态的分类结果正确。

2）算法执行时：在第1个$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $循环的算法1的第9行~第11行，将图G中节点$ u $的个数依次迭代增加，同时$ \mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t} $列表中变量$ i $依次减少，此时$ u=\mathrm{l}\mathrm{e}\mathrm{n}(\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}-) $，在循环过程中满足节点个数等于遍历列表的元素个数，满足功能1；在第2个$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $循环的第13行~第17行，对于图G中任意的$ u\in G\wedge u\notin \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k} $均满足$ \mathrm{s}\mathrm{e}\mathrm{t}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g} \,\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{a}\mathrm{c}\mathrm{y}\,{S}_{u\in g}φ \,\mathrm{i}\mathrm{n}\,G $，满足功能2，第3个$ \mathrm{f}\mathrm{o}\mathrm{r} $循环的第19行~第23行，对于图G中任意的$ u\in G $均满足$ \mathrm{s}\mathrm{e}\mathrm{t}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\,\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{a}\mathrm{c}\mathrm{y}\,{E}_{u\in g}φ \, \mathrm{i}\mathrm{n}\,G $；第3个和第4个$ \mathrm{f}\mathrm{o}\mathrm{r} $循环遍历所有节点的知识库状态，将满足的状态加入目标状态集合S中，满足功能3。

3）算法结束时：第1个$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $循环的终止条件$ \mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}=\mathrm{\varnothing } $，此时$ i=0 $，$ u=\mathrm{l}\mathrm{e}\mathrm{n}\left(\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\right)-i $，即$ u=\mathrm{l}\mathrm{e}\mathrm{n}\left(\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\right) $，说明列表中的所有相关用户已被完全生成图G中的节点。第2个$ \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{l}\mathrm{e} $循环的终止条件是$ \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(i\right)=\mathrm{\varnothing } $，当$ \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(i\right)=\mathrm{\varnothing } $时，此时有$ i=\mathrm{l}\mathrm{e}\mathrm{n}\left(\mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\right) $，设$ m $为图G中所有的节点数目，根据算法1的第14行、第15行可知$ m=u+i $，即满足功能2；对于第3个$ \mathrm{f}\mathrm{o}\mathrm{r} $循环的终止条件为遍历完所有图G中的节点，此时集合S中的状态为满足目标的状态集合。综上，基于KBL的PCTL转换算法的正确性得以证明。

依据算法1的第2行~第11行，遍历监控器的整个用户关系列表，创建社交关系图，所需的时间复杂度为$ O\left({n}^{2}\right) $，其中$ n $为关系列表中的用户个数，第13行~第24行遍历图G，通过广度优先搜索为每个用户设置知识库的更新策略，因此时间复杂度为$ O\left({n}^{2}\right) $，$ n $为图G中的节点个数。综上，基于KBL的PCTL转换算法的时间复杂度为$ O\left({n}^{2}\right) $。

引理1  若用户设置$ {S}_{G}φ $，则分组G中至少有一个用户的知识库状态为$ {K}_{i}φ $，形式化为$ {S}_{G}φ \to {\vee }_{i\in G}{K}_{i}φ $。

证明

1）算法执行前：此时未创建用户关系节点图，$ {S}_{G}φ =\mathrm{\varnothing } $，所有用户知识库$ {K}_{i}φ =\mathrm{\varnothing } $，i$ \mathrm{表}\mathrm{示}\mathrm{所}\mathrm{有}\mathrm{用}\mathrm{户} $，满足引理1。

2）算法执行时：依据list参数生成关系表，并根据算法1的第13行~第18行，根据block参数为非block节点更新知识库$ {K}_{i}φ $，其中$ i=\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\left(\mu \right), i\notin $ $ \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(i\right), \mu \mathrm{为}\mathrm{被}\mathrm{监}\mathrm{控}\mathrm{的}\mathrm{用}\mathrm{户} $，同时有$ {S}_{G}φ =φ $，$ {\vee }_{i\in G}{K}_{i}φ =φ $，满足引理1。

3）算法结束时：用户关系节点图及用户知识库更新完毕。循环遍历G中所有节点知识库$ {K}_{i}φ $，有$ {\vee }_{i\in G}{K}_{i}φ =φ $，其中$ i=\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\left(\mu \right), i\notin \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(i\right) $，同时有$ {S}_{G}φ =φ $，满足引理1。

引理2  若用户设置$ {E}_{G}φ $，则分组G中每一个用户的知识库状态为$ {K}_{i}φ $，形式化为$ {E}_{G}φ \to {\wedge }_{i\in G}{K}_{i}φ $。

证明

1）算法执行前：此时未创建用户关系节点图，$ {E}_{G}φ =\mathrm{\varnothing } $，所有用户知识库$ {K}_{i}φ =\mathrm{\varnothing } $，i$ \mathrm{表}\mathrm{示}\mathrm{所}\mathrm{有}\mathrm{用}\mathrm{户} $，满足引理2。

2）算法执行时：依据list参数生成关系表，并根据算法1中的第21行~第26行以及block参数为非block节点更新知识库$ {K}_{i}φ $，其中，$ {\wedge }_{i\in G}{K}_{i}φ =φ \mathrm{且}i=\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\left(\mu \right), i\notin \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(i\right) $，同时有$ {E}_{G}φ =φ $，满足引理2。

3）算法结束时：用户关系节点图及用户知识库更新完毕。循环遍历G中所有节点知识库$ {K}_{i}φ $，有$ {\wedge }_{i\in G}{K}_{i}φ =φ $，其中$ i=\mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}\left(\mu \right), i\notin \mathrm{b}\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{k}\left(i\right) $，同时有$ {E}_{G}φ =φ $，满足引理2。

4 隐私规约的形式化表述

通过算法1转换后的$ \mathrm{P}\mathrm{C}\mathrm{T}\mathrm{L} $语义如下：

$ φ \colon\colon =\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}\left|{K}_{i}a\left|{φ }_{1}\wedge {φ }_{2}\left|\neg φ \left|{P}_{~p}\left[\psi \right]\right.\right.\right.\right. $

$ \psi \colon\colon =φ \left|{φ }_{1}\bigcup {φ }_{2}\left|{φ }_{1}{\bigcup }^{\le n}{φ }_{2}\right.\right. $

其中，$ φ $表示状态公式，$ a\in \mathrm{A}\mathrm{P} $表示原子命题，$ ~\in ${$ < $，≤，> ，≥}，$ \psi $表示路径公式。转换后的PCTL引入了K算子，通过K算子来描述用户的知识库状态，对于给定的社交网络模型$ \mathrm{S}\mathrm{N}=〈S, 〈\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}, p〉, {l}_{\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}}, $ $ \mathrm{A}\mathrm{P}, L〉 $以及隐私设置$ \pi $，有状态$ s\in S $，状态公式$ φ $满足如下关系：

$ s\models {K}_{i}a\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,a\in L\left(s\right) $

$ s\models \,\neg φ \,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,s⊭φ $

$ s\models {φ }_{1}\wedge {φ }_{2}\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,s\models {φ }_{1}\mathrm{a}\mathrm{n}\mathrm{d}s\models {φ }_{2} $

$ s\models {P}_{~p}\left[\psi \right]\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\mathrm{P}\mathrm{r}\left(s\models φ \right)\in p $

其中，$ \mathrm{P}\mathrm{r}\left(s\models φ \right)=\mathrm{P}{\mathrm{r}}_{s}\left\{\pi \in {P}_{\mathrm{a}\mathrm{t}\mathrm{h}\mathrm{s}}\left(s\right)\left|\pi \models \right.\psi \right\} $，$ \mathrm{P}{\mathrm{r}}_{s} $为满足最终到达节点s的路径概率。

路径公式$ \psi $的满足如下关系：

$ \pi \models ○φ \,\,\,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\,\,\pi \left[1\right]\models φ $

$ \begin{array}{l}\pi \,\models {φ }_{1}\bigcup {φ }_{2}\,\,\,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\,\,\exists j\ge 0\left(\pi \left[j\,\right]\models {φ }_{2}\wedge \right.\\ \left.\left(\exists 0\le k\le j\,\right).\pi \left[k\,\right]\models {φ }_{1}\right)\end{array} $

$ \pi \models {φ }_{1}{\bigcup }^{\le n}{φ }_{2}\,\,\,\,\,\,\,\mathrm{i}\mathrm{f}\mathrm{f}\,\,\,\,\,\exists 0\le j\le n\left(\pi \left[j\right]\models {φ }_{2}\wedge \\ \left(\exists 0\le k\le j\right).\pi \left[k\right]\models {φ }_{1}\right) $

其中，路径$ \pi ={s}_{0}, {s}_{1}, \cdots ，{s}_{i}, i $表示整数，$ \mathrm{\pi }\left[i\right] $表示路径$ \pi $的第$ i $个状态。

4.1 静态隐私规约的形式化表述

为满足用户的隐私保护需求，在形式化表述的静态隐私规约的基础上加入$ \left[\right] $标记，在KBL的外面加上$ \left[\right] $标记表示该项隐私设置由该用户设置。本文通过集合$ \mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\left(\mathrm{ }\right) $记录用户$ u $设置的隐私规约，记为$ \mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\left(u\right) $，假设静态隐私规约1为如果用户A暂时屏蔽了用户B，即用户A不希望用户B知道其所发的某一条动态$ \mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}\left(φ \right) $，使用带$ \left[\right] $标记的公式进行表示：

1）对于用户A：用户A不希望用户B知道其所发的某一条动态$ φ $，$ \mathrm{F}\mathrm{o}\mathrm{r}\,\mathrm{a}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{t}\,A\,\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{s}\mathrm{f}\mathrm{y}:\left[\neg {K}_{B}φ \in \mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\left(A\right)\right] $。

2）对于社交网络模型SN而言，整个系统需求要求用户B知道用户A所发的某一条动态$ φ $的概率不高于0.01，$ \mathrm{F}\mathrm{o}\mathrm{r}\,\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{l}\mathrm{e}\,\mathrm{S}\mathrm{N}\,\,\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{s}\mathrm{f}\mathrm{y}:p\le 0.01{\left[{K}_{B}φ \right]}_{A} $。

为表述方便，静态隐私规约1也可以表述为$ \mathrm{F}\mathrm{o}\mathrm{r}\,\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{l}\mathrm{e}\,\mathrm{S}\mathrm{N}\,\,\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{s}\mathrm{f}\mathrm{y}:p>0.99{\left[\neg {K}_{B}φ \right]}_{A} $。通过以上方式可对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可表示为$ \left[\right]20:00\le \mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{r}\le 08:00\to $ $ {\left[{K}_{\mathrm{c}\mathrm{o}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{g}\mathrm{e}}φ \right]}_{u} $。

2）基于地点的动态隐私设置。触发条件为地点，当系统内部定位的地点满足条件时会触发条件，定义动态隐私规约2为在社交网络中某一用户u希望对其工作地点和非工作地点进行区分，只在工作地点（company）所发表的动态才会被同事们所看到，可设置如下BOL规则：只在工作地点所发表的动态可被college列表中的同事所看见，用PCTL可表示为$ \left[\right]\mathrm{l}\mathrm{o}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\,!=\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{p}\mathrm{a}\mathrm{n}\mathrm{y}\to {\left[\neg {K}_{\mathrm{c}\mathrm{o}\mathrm{l}\mathrm{l}\mathrm{e}\mathrm{g}\mathrm{e}}φ \right]}_{u} $。

3）基于事件的动态隐私设置。触发条件为事件，当系统内检测到满足条件的事件发生时就会触发条件，定义动态隐私规约3为某一用户u希望能更加灵活地管理自己的朋友列表，为防止自己的动态被人无限制转发，可设置如下BOE规则：只有当好友a点赞并评论自己所发的某条动态后，该好友才有权限转发该动态，否则不给予其转发该条动态的权限，用PCTL可表示为$ \left[\right]（\mathrm{l}\mathrm{i}\mathrm{k}\mathrm{e}\left(φ \right)\wedge \mathrm{c}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}\left(φ \right)=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}）\in a\to $ $ \mathrm{r}\mathrm{e}\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{t}\mathrm{e}\mathrm{d}\left(φ \right)\bigcup a $。

由于动态隐私设置需要依据触发条件来动态更改用户的社交网络结构，因此本文需先对静态隐私设置进行更改以满足动态隐私需求。设置一个临时屏蔽分组（block），在分组中存储不满足动态隐私规范而被临时屏蔽的好友，基于时间的动态隐私保护框架如图 3所示。

当不满足迁移条件的好友被移到block分组时，若一旦监控器监测到条件满足，则会将block分组中的好友移回原分组。基于地点和事件的动态隐私保护框架如图 4、图 5所示，其中，like（φ）=μ表示用户μ对动态φ进行点赞，comment（φ）=μ表示用户μ对动态φ进行评论，reposted（φ）=μ表示用户$ \mu $对动态$ φ $进行转发。

5 社交网络系统的形式化建模 5.1 基于静态隐私保护框架的DTMC模型

对于静态隐私保护框架，终端用户设置隐私规约后发送给服务器或转发设备，服务器接受隐私规约后进行数据融合更新，本文对静态隐私保护框架的DTMC建模如图 6所示。若状态间未标明转移概率，则默认其转移概率为1，系统状态及其含义如表 1所示。

社交网络用户将新的隐私设置发送给服务器，但服务器和用户之间的通信协议存在一定的随机性，即服务器可能有$ {p}_{1} $的概率接收数据失败。由于社交网络用户非常多，服务器在短时间内接收的用户隐私设置无法同一时间立即完成更新，因此当服务器正在更新设置时，刚接收到的数据有$ {p}_{2} $的概率进入服务器忙碌状态，需要服务器等待重新接收数据进行处理。当服务器处于空闲状态并接收数据后开始更新操作，由于更新操作建立在通信协议的基础上，因此更新操作有$ {p}_{3} $的概率更新失败。

5.2 基于动态隐私保护框架的DTMC模型

本文根据动态隐私保护框架，将其分为社交网络模型SN和隐私监控器P-monitor两部分进行建模。社交网络模型如图 7所示，其中实线单向箭头、实线双向箭头、虚线单向箭头、点划线单向箭头分别代表用户节点之间的好友、同事、屏蔽、陌生人4种社交关系。

定义2 （P-monitor）   P-monitor= < User，timer，location，list，operation > ，其中：User表示记录被监控的社交网络用户，返回值是用户$ u\in \mathrm{A}\mathrm{g} $；timer表示时间记录器，用于记录系统内部时间，返回值是时间序列；location表示地点记录器，用于记录被监控用户当前的位置，返回值是定位信息；list表示 < friend，family，strange，college，block > ，list列表用于记录被监控用户的关系列表，返回值是集合{$ {u}_{1}, {u}_{2}, \cdots $}，$ {u}_{1}, {u}_{2}\in \mathrm{A}\mathrm{g} $；operation表示主要监控用户权限范围内可调用的函数，如发表动态、转发别人的动态、允许别人转发自己的某一条动态、点赞、不喜欢、评论等行为分别调用post、repost、reposted、like、dislike等函数。

将隐私监控器P-monitor植入社交网络模型中，结合随机模型检验工具，构建基于动态隐私保护框架的DTMC模型，如图 8所示。

在动态隐私保护框架中发送给服务器更新隐私规约这部分内容与静态隐私保护框架相同，不同的是在动态隐私保护框架下，用户会将动态隐私策略会发送给P-monitor。P-monitor与用户之间是一一对应关系，即每个使用静态隐私策略的用户都会在用户终端生成一个P-monitor，P-monitor可以执行服务器接收数据的功能，由于P-monitor与用户之间的通信也建立在通信协议的基础上，因此P-monitor有$ {p}_{4} $的概率未接受用户的隐私规约，但是当P-monitor接受新的隐私规约后就立即对社交网络进行监控，因此不会出现更新失败的情况。

6 实验结果与分析

由于当前社交网络均是非开源网络，因此本文选择开源社交网络软件验证社交网络的隐私泄露问题。Diaspora是一款由美国纽约大学学生所开发的基于Web的开源社交网络^[24]。PRISM是一款由英国牛津大学Prof.Marta研究组研发的随机模型检验工具^[25]，被用于验证通信协议、密码协议和生物系统^[26]等的可靠性，具有较好的检验效果。本文在Diaspora社交网络上植入监控器，并在PRISM随机模型检验工具上进行验证。实验共分为静态隐私验证和动态隐私验证两部分，其中：静态隐私部分针对静态隐私规约1；动态隐私部分针对动态隐私规约1和3。整体实验运行基于PRISM4.5，假定Diaspora服务器端接收用户发送信息失败的概率$ {p}_{1} $和服务器更新失败的概率$ {p}_{2} $均为0.01，同时在动态隐私保护框架中假设P-monitor接收用户新的隐私设置数据失败的概率$ {p}_{4} $也为0.01。通过PRISM建立静态隐私保护框架模型累计状态集合为32个，其中包含1个初始状态，转移状态共64个，动态隐私保护框架模型累计状态集合为1 152个，其中包含1个初始状态，转移状态共6 519个。

对于静态隐私规约1，本文使用PRISM验证的结果为$ {p}_{\mathrm{m}\mathrm{a}\mathrm{x}}\left[{K}_{\mathrm{B}\mathrm{o}\mathrm{b}}=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}\right] $，该等式表示最终用户Bob的知识库K的值为true的最大概率，计算得到p=0.020 000 252 231 567 4，该概率值高于系统需求的0.01。

对于动态隐私规约1，P-monitor输入参数如表 2所示，其中，User表示被监控的用户，timer表示时间记录器，location表示地点记录器，post表示被监控用户是否发表动态，reposted表示对动态进行转发的用户集合，like表示被对动态进行点赞的用户集合，dislike表示对动态不喜欢的用户集合，comment表示对动态进行评论的用户集合，$ {p}_{\mathrm{m}\mathrm{a}\mathrm{x}}\left[{K}_{\mathrm{B}\mathrm{o}\mathrm{b}}=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}\right] $表示最终用户Bob知道被监控对象Alice发表动态的概率。

通过实验数据发现，在服务器和监控器的容错概率下，使用监控器来保存动态隐私设置要比使用服务器来更新静态隐私设置的隐私泄露风险降低50%，这主要是因为两者架构不同，服务器是针对所有用户，存在拥塞和延迟，并且出错概率也大幅提高，但是监控器是针对个人用户，不存在拥塞和延迟，所以可以大幅降低隐私泄露风险。

为进一步验证动态隐私策略和静态隐私策略在时间维度上的隐私泄露风险，设定每一步长的reward为1，其中reward为执行图遍历算法的花费，通过实验对比分析不同时间维度下动态和静态隐私泄露风险，实验结果如图 9所示。静态DTMC模型内部各个节点的状态变化如图 10所示，其中，User表示被监控用户的节点状态，Agent表示代理服务器的节点状态。

实验结果表明，在极短时间内动态隐私规约相比静态隐私规约出现了用户隐私信息泄露的情况，产生该情况的主要原因为动态隐私设置采用监控器直接对用户隐私设置进行保存和监控，同时考虑到监控器在接收用户数据信息时会产生一定的失败概率，并且监控器发生错误的情况要比服务器更快，因此在极短时间内，若监控器发生错误，则会比静态隐私保护框架下服务器发生错误的时间更短。但是从长时间而言，在稳定状态下动态隐私保护框架比静态隐私保护框架的用户隐私信息泄露风险更低，并且动态隐私规约也更灵活性。

对于动态隐私规约3，由于在动态隐私保护框架中隐私泄露的风险只与是否成功接收到被监控用户发送的数据有关，因此本文只验证在P-monitor未正常更新的情况下，由于用户的随机行为所产生的隐私泄露概率。假定用户设置的动态隐私设置未成功保存至P-monitor中，在该假设前提下P-monitor输入参数如表 3所示。动态DTMC模型内部各节点的状态变化如图 11所示，其中，Bob表示用户Bob的节点状态，Update表示监控器执行用户隐私设置的状态。

实验结果表明，本文设计的动态隐私保护框架通过植入P-monitor进行用户隐私设置，但不发送到服务器端，其主要原因为服务器端存在的接收失败、忙碌、更新失败等随机故障，会导致隐私泄露风险远大于用户需求。基于P-monitor的动态隐私保护框架通过动态的隐私设置，提高社交网络隐私设置的灵活性，并基于P-monitor与用户间一对一的监控结构，解决了服务器端存在的接收失败、忙碌、更新失败等随机故障，降低了用户隐私泄露风险。

7 结束语

本文提出一种面向社交网络的动态隐私保护框架，结合随机模型检验与运行时验证技术，构建基于知识逻辑拓展的离散时间马尔科夫链模型，将用户隐私设置形式化表述为概率计算树逻辑，同时通过运行时验证中的参数化和监控技术实现用户隐私信息的保护。实验结果表明，与静态隐私保护框架相比，该动态隐私保护框架在提高用户隐私策略灵活性的同时降低了隐私泄露风险。但该框架中的动态隐私策略仅针对时间、地点和事件的触发条件，下一步将优化动态隐私保护框架，扩展动态隐私策略的应用范围，以满足多用户的个性化隐私保护需求。