Research And Application Of Runtime Verification Method For The Security Of Online Social Networks

The rapid development of Internet technology has caused the explosive growth of information in modern society.Nowadays people are increasingly enjoying sharing information on the Internet.The emergence of social networks(SNs)provides the platform for billions of Internet users to quickly share information.In recent years,the popularity of smart mobile devices has further promoted the rapid development of SN.People can socialize and work anywhere,anytime through mobile devices,and rely more and more on SN in life and work.The number of users of popular social platforms at home and abroad has reached billions.The large number of users make SN the hardest hit area for cyber-attacks.Once privacy leaks,it often involves large-scale users.Therefore,the security of SN cannot be ignored.The reason for the leakage of privacy is that the security and reliability of the SN system itself is not high enough.On the other hand,users are not aware of their privacy protection.As a software system,SN can use software verification methods to ensure its security and reliability.However,traditional software verification methods such as model checking,theorem proving and testing have some shortcomings for verifying complex systems.Therefore,in order to improve the reliability and security of SN,it is necessary to adopt a more complete and real-time verification method.In order to verify the SN system,this thesis proposes an online runtime verification method.The method uses source code instrumentation technology to capture information generated during the running process of the system and verify the system in real time without modeling.Firstly,the security-related properties of the SN system are obtained,and these properties are formally described by the Three-valued Propositional Projection Temporal Logic(PPTL3)formulas,which are then transformed into corresponding finite state automata(property monitor).Then,positions of the inserted probes are determined according to the related events in the security property of the system.Probes capture the sequence of events related to the security property and send it to the receiving server of the runtime monitor.At the same time,the runtime monitor reads the information of the property monitor.Also the runtime monitor starts monitoring and receiving the sequence of events sent by the probe in real time,and converting the sequence into a combination of atomic propositions.The property monitor determines the state transition of each step according to the combination: When the acceptance node(TRUE or FALSE)is reached,the runtime monitor stops monitoring and gives the verification result,otherwise the verification result is inconclusive and can continue to monitor.Finally,two open source SN systems are studied.The results show the effectiveness of the proposed method and detect some violations of security properties of the two systems.