Program security verification based on abstract invariants

Program security verification is a difficult issue with program invariants used for program security verification. Verification of whether a program has the correct temporal nature is converted into a problem solved at a fixed point. However, directly constructing an algorithm to solve the fixed point problem is very difficult. This paper presents a class of invariant construction methods based on an abstract interpretation framework to solve the structure method. Firstly, the Tableau method is used to construct the figure of the temporal formula based on the traditional invariant structure rules, with forward or backward state transitions to improve the invariant validation rules. Secondly, this paper presents an abstract state transition system based on an abstract interpretation framework and gives the abstract invariants validation rules. Finally, the fixed point theorem of abstract invariants is used with the forward or reverse transformations to solve the approximate fixed point in an automatic validation method based on abstract invariants of the program. Approximate widening and narrowing operations based on the abstract fixed point invariant verification algorithm accelerate the convergence.