With the rapid development of the Internet, people are becoming more dependent on the Internet. However, the security of the network is an issue that cannot be ignored. As a formal verification method, model checking has the advantage of automation in security property verification. In this paper, we organized much literature about model checking and SPIN. SPIN is one of the most widely used model checking tools. We tracked the application and development of SPIN in the past 30 years. In addition, we also discussed the optimization problems of SPIN, such as the problem of source code automation modeling. And we gave a theoretical framework for modeling to help professional researchers solve the problem faster and better. In the application of model checking and SPIN, we mainly focus on network protocols and cyberspace vulnerability. Finally, we discussed the challenges and future work.
Some recent studies have found that there are some side-channel vulnerabilities in the operating system. Attackers would exploit the side-channel vulnerability for malicious purpose, such as hijack connections, denial of service attacks, etc. Currently, most attacks are detected manually. In this paper, we found that the reason for the existence of network protocol side-channel vulnerability is the use of shared resources. Since the state of shared resource affects all connections, when a connection uses a shared resource, information about that connection can be inferred by observing the usage of the shared resource. In order to find the shared resources, we implemented a tool called TASR which is a method of static analysis. The first is to find out what shared resources are available by the definition of shared resources in static analysis. Then, the data packet is used as the taint source to search the tainted shared resources. The second step is to analyze the taint-transmission-path according to the acquired tainted shared variable. Then it can find the side-channel vulnerability. By using this method on TCP, UDP and ICMP protocols, we find the following four shared variables: challenge_count, tcp_memory_allocated, tcp_memory_pressure, sysctl_icmp_msg_per_sec. It is difficult for tcp_memory allocated and tcp_memory pressure to exploit, because they will go through multiple strict checks. Using challenge_count can hijack the connection and inject malicious packets. Using sysctl_icmp_msg_per_sec can assist in DNS cache poisoning attack.
'/%3e%3cuse xlink:href='%23a' transform='rotate(23.036 .093 25.536)'/%3e%3cuse xlink:href='%23a' transform='rotate(45.87 1.273 16.18)'/%3e%3cuse xlink:href='%23a' transform='rotate(69.945 .996 12.078)'/%3e%3cuse xlink:href='%23a' transform='rotate(20.66 -19.689 31.932)'/%3e%3c/svg%3e)
'/%3e%3cuse xlink:href='%23a' transform='translate(288.889 -214.211)'/%3e%3cuse xlink:href='%23a' transform='translate(108 342.749)'/%3e%3cuse xlink:href='%23a' transform='translate(469.189 342.749)'/%3e%3c/svg%3e)
'%3e%3cpath fill='%23012169' d='M0 0v30h60V0z'/%3e%3cpath stroke='%23fff' stroke-width='6' d='m0 0 60 30m0-30L0 30'/%3e%3cpath stroke='%23C8102E' stroke-width='4' d='m0 0 60 30m0-30L0 30' clip-path='url(%23b)'/%3e%3cpath stroke='%23fff' stroke-width='10' d='M30 0v30M0 15h60'/%3e%3cpath stroke='%23C8102E' stroke-width='6' d='M30 0v30M0 15h60'/%3e%3c/g%3e%3c/svg%3e)