Research On Static Analysis And Verification Technology Based On Iterative Abstract Interpretation

Nowadays the size and complexity of software are increasing gradually.Improving the trustworthiness of software has become the focus of research in the field of software engineering,especially in the safety-critical fields such as national defense,finance and healthcare.Most of the safety-critical software,which are generally related to mathemat-ical and physical models closely,inevitably involve a large number of numerical compu-tations.Hence,it is especially important to analyze and verify the numerical properties of programs to improve the trustworthiness of the safety-critical software.interpretation is a general theory of abstraction and approximation.It provides an unified theoretical framework for the abstraction and reasoning of program semantics,and has been widely used in the field of program analysis and verification.The analysis and verification technology based on single-pass abstract interpretation is good at analyzing programs soundly with high scalability under abstract semantics,which leads to the huge precision loss.As a result,it may bring false alarms and reach incomplete conclusion during the program analysis and verification.Therefore,this paper proposes an iterative abstract interpretation based analysis and verification framework based on input domain partitioning and semantic transfer function relaxation,and combines dynamic testing techniques to achieve more accurate program analysis and more complete property verification.This paper makes the following three contributions.(1)We propose a property-guided verification framework based on iterative abstract testing and bounded exhaustive testing,which aims to enhance the numerical program verification ability of abstract interpretation.Abstract testing essentially uses the result of forward abstraction interpretation to check whether the property holds.If the property does not holds,the input space is refined by forward abstraction interpretation.When the single-pass abstract testing cannot judge whether the property holds or not,we use the dynamic input splitting technique,which is guided by program structure and the property,to divide the abstract input into several sub-abstract inputs.On the one hand,since each sub-abstract input corresponding program involves less and simpler specific behaviors,it is easier to be verified by abstract testing on the other hand,when the sub-abstract input space is small enough,we use bounded exhaustive testing to achieve more complete verification.Abstract testing and specific testing are two complementary verification techniques,which are effectively combined in our verification framework.We have implemented the tool VATer based on the verification framework proposed in this paper.The verification rate of VATer is increased by up to 3 times compared with that of the single-pass abstract interpretation based tools.And compared with three state-of-the-art model checking based verifiers,VATer achieves over an order of magnitude speedup on average.The experimental results demonstrate the high effectiveness and efficiency of VATer.(2)We propose a hierarchical iterative abstract interpretation analysis of program with loops,which is based on the relaxation technique of semantic transfer function.Loop is one of the most challenging structures in program analysis,and it is also an major source of precision loss in abstract interpretation.We first partition all variables involved in a loop into different hierarchical layers,and constructs a list of sliced program based on hierarchical layers of variables.Then we compute invariants over the variables layer by layer in a bottom-up manner.During the iterative process,the computed partial invari-ants over lower layer variables are then used to relax transfer functions when analyzing the higher layer variables,which finally reaches a precise analysis result for the whole program.Relaxation of transfer function is the core operator of our approach,we have proposed and combined several alternative relaxation strategies to reach an effective preci-sion improvement.We have implemented a tool named Relax AIer based on our approach.Compared with a single-pass abstract interpreter Interproc,Relax AIer infers finite bound-aries for 4.78 X variables.The number of bounded variables contained in the loop invari-ant inferred by Relax AIer is 4.78 times that of Interproc,which is a single-pass abstract interpreter.The experimental results have shown that Relax AIer significantly improves the precision of abstract interpretation.(3)We propose a sound and complete neural net-work verification framework based on iterative abstract analysis.Neural network can be regarded as a special program.In this paper,we apply the technique of program analysis and verification to the safety and robustness verification of neural networks.The iterative abstraction verification based general framework is designed by input splitting technique.Considering the characteristics of neural network itself,our core idea is to generate input splitting predicates based on the first undeterministic layer(FUL)neurons that make ac-tivation states of hidden neurons become deterministic.And the splitting predicates are then utilized for refining inputs systematically.So that the relaxed transfer function based abstract analysis over refined input can be more precise.Our verification process also in-corporates dynamic testing to generate counterexamples for false properties efficiently.We have implemented a parallel tool called INDICATOR to verify safety and robustness properties of neural networks in a sound and complete way,and evaluated it extensively on several benchmark sets.The experimental results show that the INDICATOR veri-fies more neural networks completely with less time overhead than three state-of-the-art sound and complete verifiers named Relu Val,Planet and Marabou.And when verifying the properties of the ACAS Xu neural network,INDICATOR obtains at least 43 times,324 times and 317 times verification speedups compared to the other three tools respec-tively.