Research On Array Abstraction Based Efficient Program Verification Technology

Array is a common data structure that exists widely in various programs.Because large array processing loops often lead to large state spaces,array programs are one of the main challenges for current program verification techniques.When verifying programs with large arrays,traditional verification methods often run out of time or memory.Ar-rays are also commonly used in embedded software.Shared register access conflict is an important type of vulnerabilities in interrupt-driven programs.How to effectively detect shared register access conflicts in interrupt-driven programs is a key issue to ensure the security of embedded systems.In this paper,we study an array abstraction based efficient program verification tech-nique and propose an array program verification framework based on loop dependence analysis.For each array processing loop in an array program,we design a static analy-sis method to obtain a compressed loop and construct an abstract program.The property checking of the abstract program can be used to approximate the original property.In addition,this paper also studies the array abstraction based shared register access conflict detection technique for interrupt-driven programs.We transform the shared reg-ister operations into the operations on array elements,which is semantically equivalent to the original program.Then we design two conflict detection methods based on static analysis to find all potential defects in an interrupt-driven program.In order to effectively eliminate false positives in the results of static analysis,we propose a defect-guided se-quentialization method to generate sequentialized programs.Then we validate the defect by verifying the reachability property in the sequentialized program.If an execution path that triggers the defect can be found,it means that the defect is a real vulnerability.Based on the above methods,we implement the prototype tool AIPCBMC.We eval-uate AIPCBMC on the benchmarks from SV-COMP 2019 and test cases from industry.The experimental results show that the loop compression method improves the verifica-tion efficiency of array programs effectively.At the same time,the tool can detect the shared register access conflicts in interrupt-driven programs and achieve high precision.