Fast Game Verification for Safety- and Security-Critical Distributed Applications

The co-verification of safety and security is a necessary process for safety- and security-critical distributed applications, but conflicts exist between safety and security. The state-of-the-art Block-based Vulnerability Pre-assignment (BVP) and Reversed Block-based Time Pre-assignment (RBTP) co-verification techniques of safety and security have three main limitations: 1) only co-verifying the boundary values and ignoring the verification of non-boundary values; 2) algorithm redundancy (i.e., BVP and RBTP must be used simultaneously) makes the verification process complex and cumbersome; and 3) only one safety attribute and one security attribute participate in the co-verification. In this study, we explore the causal mechanisms for the mutual influence between safety and security: 1) they compete with each other in relation to Worst Case Execution Time (WCET); 2) there is a lack of cooperation between the two; and 3) both are pursuing maximum performance for each individual. Above causal mechanisms precisely conforms to the problem of maximizing benefits in non-cooperative games (i.e., Nash equilibrium). Therefore, we propose the Fast Game Verification (FGV) based on non-cooperative game to co-verify reliability in safety and confidentiality in security. FGV achieves non-boundary value co-verification and avoids redundancy. We develop Fast Game Verification plus plus (FGV++) algorithm to co-verify multiple safety attributes and multiple security attributes. We conduct actual cases of distributed applications. In terms of the co-verification of two attributes, FGV demonstrates average acceptance rate of 59.96% within 0.638 s, surpassing both BVP&RBTP by 6.94% (within 0.812 s); FGV++ achieves average acceptance rate of 58.73% within 0.663 s, exhibiting a 4.53% advantage over BVP and RBTP. In the co-verification of four attributes, the average acceptance rate of FGV++ has increased to 61.07% within 1.34102 s.