Social networking system privacy security runtime verification method based on PPTL3

Abstract

The invention discloses a social networking system privacy security runtime verification method based on PPTL3. The method comprises the steps that the property P to be verified is described with a PPTL3 formula, then logical formulas corresponding to P and non P are converted into normal formulas and further converted into normal form graphs and normal form graphs with marks, a corresponding Buchi automaton can be obtained according to the latter, a finite automaton is defined and determined by changing a receiving set, and finally quadrature is carried out on the finite automaton to build a monitor. On the basis, the invention further discloses application of runtime verification in a social networking system, the property needed by the social networking system is described through the PPTL3 formula, and a corresponding monitor is built and monitors the running system to judge whether current running meets the property or not.

Description

technical field [0001] The invention belongs to the field of computer application technology, and in particular relates to a PPTL-based 3 A privacy-safe runtime verification method for a social networking system. Background technique [0002] With the development of computer technology, computer software is widely used in various fields, among which social network (Social Network Service / Site, SNS) has penetrated into all aspects of people's life and work. In a broad sense, SNS is an online community created by a group of people with the same interests and activities, providing them with a way to quickly communicate and share various information, which brings great convenience to life and work. Typical SNS abroad include Facebook, Twitter, YouTube, etc., and domestically, there are WeChat, Sina Weibo, Baidu Tieba, Qzone, etc. While SNS is convenient for people's life, it also brings a lot of security problems. In May 2009, the Koobface worm attacked Facebook, stealing use...

AI Technical Summary

Problems solved by technology

While SNS is convenient for people's life, it also brings a lot of security problems

In May 2009, the Koobface worm attacked Facebook, stealing user information and spreading it on other SNS; in June 2011, a large number of Sina Weibo users suffered cross-site scripting attacks, automatically sent Weibo and private messages, and followed user hellosamy; in 2014 In September, a large number of photos of Hollywood actresses were leaked through iCloud. The real reason was the privacy leak brought by SNS; in March 2015, the Wuyun Vulnerability Platform released a high-risk vulnerability, showing that there are design flaws in WeChat red envelopes, hackers can design programs to automatically receive others to send In September 2015, nearly 350 Apple apps such as WeChat found Xcode’s “malicious backdoor” that could leak users’ private information

[0008] However, the above-mentioned runtime verification methods based on LTL and ITL have achieved some results in formal verification, but there are still shortcomings: First, the expressive ability of LTL is not strong enough, and it does not have the full regular expression ability of Omega, such as " Propositional variable p is true on all even states of a state sequence" cannot be expressed in LTL; and the runtime verification tools based on ITL are prototype systems and have not been widely used

Images