Verification Of The Social Network Privacy Policy Based On MSVL

As we all know, the invention of Six Degrees Separation theory opens a door to the modern Internet world. It introduces the initial social network into the Internet and creates the social network oriented Internet service which is also known as the SNS (Social Network Service). With the rapid development of the Internet and Web technologies, the SNS has involved all aspects of our lives and brought great conveniences to our lives, work and study. However, in SNS due to the excessive openness of the users' personal privacy information and its rapid spread in the Internet, a number of issues of the users'privacy information leak have raised.There are many reasons for the issues of users'privacy information leak, and one is that the privacy policy of some SNSs is not complete. To solve this kind of problem, this thesis proposes a method of modeling SNS and verifying privacy policies based on MSVL (Modeling Simulation Verification Language). MSVL is a modeling, simulation and verification language which is a framed temporal logic programming language. At first, a suitable SNS is selected and the users' information data packets in a certain period of time are obtained by using the web crawler technology. Then, the user-related information and relationships between users in the data packets are extracted by writing the Python program, and then the TXT texts are generated. After that, several users from the TXT texts are chosen, and a graph model of user relations in the SNS is created based on the relationships and operations of the selected users. Finally, the graph model is verified through the method of a unified model checking based on PTL (Projection Temporal Logic). During the verification the graph model is described with MSVL, and the typical privacy policy properties of the system are specified with PPTL (Propositional Projection Temporal Logic) formulas, then the MSVL program and the PPTL formulas are unified executed in the MSV platform. According to the result, the user can improve and modify the related SNS and the privacy policy properties. Finally, the method is used for the Sina Weibo instance and the result shows its effectiveness.