Research on Privacy Protection in Social Network Based on Stochastic Model Checking

doi:10.19678/j.issn.1000-3428.0057769

Abstract

Abstract: The privacy settings in static privacy strategies of the existing online social networks are not flexible and hard for quantitative verification.To address the problem,this paper proposes a dynamic privacy protection framework,which models social networks as Discrete Time Markov Chains(DTMC).The dynamic privacy policy for users is realized by adding triggers and transformed into Probabilistic Computation Tree Logic(PCTL) formula.Then the stochastic model-based checking technique and parameterization and monitoring technique in runtime verification are used to protect users' dynamic privacy information in the case of random social network failures.Experimental results on the open-source social network called Diaspora show that compared with the static privacy protection framework,the proposed dynamic privacy protection framework has higher security and flexibility,meeting the privacy protection requirements of users.

Key words: social network, privacy protection, runtime verification, stochastic model checking, Probabilistic Computation Tree Logic(PCTL)

摘要： 针对现有社交网络所提供静态隐私策略的隐私设置不够灵活且难以定量验证问题，提出一种动态隐私保护框架，将社交网络建模为离散时间马尔科夫链模型，通过设置触发条件实现用户动态隐私规约并将其转化为概率计算树逻辑公式，同时结合随机模型检验和运行时验证中的参数化与监控技术，保护社交网络发生随机故障情况下的用户动态隐私信息。在Diaspora开源社交网络上的实验结果表明，与静态隐私保护框架相比，动态隐私保护框架具有更高的安全性和灵活性，能较好满足用户的隐私保护需求。

关键词: 社交网络, 隐私保护, 运行时验证, 随机模型检验, 概率计算树逻辑

CLC Number:

TP311

LIU Yang, GAO Shiguo. Research on Privacy Protection in Social Network Based on Stochastic Model Checking[J]. Computer Engineering, 2021, 47(5): 144-153.

刘阳, 高世国. 基于随机模型检验的社交网络隐私保护研究[J]. 计算机工程, 2021, 47(5): 144-153.

/ / Recommend / Download Citations

URL: http://www.ecice06.com/EN/10.19678/j.issn.1000-3428.0057769

http://www.ecice06.com/EN/Y2021/V47/I5/144

References

[1] PARDO R,SCHNEIDER G.A formal privacy policy framework for social networks[C]//Proceedings of International Conference on Software Engineering and Formal Methods.Berlin,Germany:Springer,2014:378-392.
[2] COLOMBO C,PACE G J,SCHNEIDER G.Dynamic event-based runtime monitoring of real-time and contextual properties[C]//Proceedings of International Workshop on Formal Methods for Industrial Critical Systems.Berlin,Germany:Springer,2008:135-149.
[3] KOZUCH K.Facebook slammed with $5 billion fine for privacy fails[EB/OL].[2020-02-01].https://www.twice.com/keeping-current/facebook-slammed-with-5-billion-fine-for-privacy-fails.
[4] LIU Y,GUMMADI K P,KRISHNAMURTHY B,et al.Analyzing Facebook privacy settings:user expectations vs.reality[C]//Proceedings of 2011 ACM SIGCOMM Conference on Internet Measurement.New York,USA:ACM Press,2011:61-70.
[5] LIU Yang,LI Xuandong,MA Yan,et al.Survey for stochastic model checking[J].Chinese Journal of Computers,2015,38(11):2145-2162.(in Chinese)刘阳,李宣东,马艳,等.随机模型检验研究[J].计算机学报,2015,38(11):2145-2162.
[6] CLARKE E M,EMERSON E A,SIFAKIS J.Model checking:algorithmic verification and debugging[J].Communications of the ACM,2009,52(11):74-84.
[7] KWIATKOWSKA M,NORMAN G,PARKER D.Stochastic model checking[C]//Proceedings of International Conference on Formal Methods for the Design of Computer,Communication and Software Systems.Berlin,Germany:Springer,2007:220-270.
[8] BODDEN E,LAM P,HENDREN L.Partially evaluating finite-state runtime monitors ahead of time[J].ACM Transactions on Programming Languages and Systems,2012,34(2):7-12.
[9] JOSHAGHANI R,MEHRPOUYAN H.A model-checking approach for enforcing purpose-based privacy policies[C]//Proceedings of Privacy-Aware Computing Conference.Washington D.C.,USA:IEEE Press,2017:178-179.
[10] BHATIA J,BREAUX T D.A data purpose case study of privacy policies[C]//Proceedings of the 25th International Requirements Engineering Conference.Washington D.C.,USA:IEEE Press,2017:394-399.
[11] WANG Xiaobing,SUN Tao.A method based on MSVL for verification of the social network privacy policy[C]//Proceedings of International Workshop on Structured Object-oriented Formal Language & Method.Berlin,Germany:Springer,2015:118-131.
[12] DENNIS L A,SLAVKOVIK M,FISHER M."How did they know?"-model-checking for analysis of information leakage in social networks[M]//CRANEFIELD S,MAHMOUD S,PADGET J,et al.Coordination,organizations,institutions,and norms in agent systems XⅡ.Berlin,Germany:Springer,2016:42-59.
[13] KOLEINI M,RYAN M.A knowledge-based verification method for dynamic access control policies[C]//Proceedings of International Conference on Formal Methods & Software Engineering.Berlin,Germany:Springer,2011:243-258.
[14] LI Fenghua,SUN Ze,NIU Ben,et al.A framework of private images sharing across social networks[J].Journal on Communications,2019,40(7):1-13.(in Chinese)李凤华,孙哲,牛犇,等.跨社交网络的隐私图片分享框架[J].通信学报,2019,40(7):1-13.
[15] LI Yuanhang,CHEN Xianlai,LIU Li,et al.Random forest algorithm for differential privacy protection[J].Computer Engineering,2020,46(1):93-101.(in Chinese)李远航,陈先来,刘莉,等.面向差分隐私保护的随机森林算法[J].计算机工程,2020,46(1):93-101.
[16] WU Xu,LUO Min.Privacy-preserving method of location based service in sparse environment[J].Computer Engineering,2017,43(5):108-114.(in Chinese)伍旭,罗敏.稀疏环境下基于位置服务的隐私保护方法[J].计算机工程,2017,43(5):108-114.
[17] CASTIGLIONI V,CHATZIKOKOLAKIS K,PALAMIDESSI C.A logical characterization of differential privacy[J].Science of Computer Programming,2020,188:57-88.
[18] FILIERI A,GHEZZI C,TAMBURRELLI G,et al.Run-time efficient probabilistic model checking[C]//Proceedings of International Conference on Software Engineering.New York,USA:ACM Press,2011:341-350.
[19] BARTOCCI E,BORTOLUSSI L,NENZI L,et al.System design of stochastic models using robustness of temporal properties[J].Theoretical Computer Science,2015,587:3-25.
[20] HINRICHS T L,SISTLA A P,ZUCK L D.Model check what you can,runtime verify the rest[C]//Proceedings of HOWARD'14.Berlin,Germany:Springer,2014:11-25.
[21] FILIERI A,GHEZZI C,TAMBURRELLI G.Run-time efficient probabilistic model checking[C]//Proceedings of the 33rd International Conference on Software Engineering.New York,USA:ACM Press,2011:341-350.
[22] PACE G J,PARDO R,SCHNEIDER G.On the runtime enforcement of evolving privacy policies in online social networks[C]//Proceedings of International Symposium on Leveraging Applications of Formal Methods.Berlin,Germany:Springer,2016:407-412.
[23] HANSSON H,JONSSON B.A logic for reasoning about time and reliability[J].Formal Aspects of Computing,1994,6(5):512-535.
[24] Diaspora[EB/OL].[2020-02-01].https://diasporafoundation.org/.
[25] KWIATKOWSKA M,NORMAN G,PARKER D,et al.PRISM 4.0:verification of probabilistic real-time systems[C]//Proceedings of the 23rd International Conference on Computer Aided Verification.Berlin,Germany:Springer,2011:585-591.
[26] PRISM:probabilistic symbolic model checker[EB/OL].[2020-02-01].http://www.prismmodelchecker.org.

Please choose a citation manager

Content to export