System and method for software verification

Patent metadata

Field	Value
Publication number	US-11275860-B2
Application number	US-202016814460-A
Country	US
Kind code	B2
Filing date	Mar 10, 2020
Priority date	Nov 8, 2019
Publication date	Mar 15, 2022
Grant date	Mar 15, 2022

Abstract

A system and a method for verification of a source code are provided. There as many techniques available that can be used for verification of software codes, however, it is difficult to determine appropriate technique that can be utilized for verification of a given software code. In an embodiment, the system receives a source code encoded with one or more specifications to be verified. A static analysis of the source code is performed to identify program features of the source code. The program features may include, but are not limited to, multiple return paths, loops with an unstructured control flow, loops with arrays, short ranges and numerical loops. Based on the identification of the program features, verification techniques are applied to the source code for the verification. Each verification technique of the one or more verification techniques is applied for a predetermined period of time and in a predefined order.

First claim

What is claimed is:

1. A processor implemented method for verification of a source code, comprising:
receiving a source code encoded with one or more specifications to be verified, via one or more hardware processors;
performing, via the one or more hardware processors, static analysis of the source code to identify one or more program features of the source code, the one or more program features comprising at least one of multiple return paths, loops with an unstructured control flow, loops with arrays, loops with inputs of discrete values and numerical loops;
performing a structural analysis of a plurality of loops and an interval analysis of input values read in the plurality of loops to determine a predefined order of a plurality of verification techniques to verify the source code based on the plurality of loops and a program control flow;
applying the plurality of verification techniques associated with the one or more program features to the source code for the verification, via the one or more hardware processors, wherein the source code comprises the loops with inputs of discrete values and numerical loops, wherein each verification technique of the plurality of verification techniques is applied for a predetermined period of time and in the predefined order, wherein a verification technique from the plurality of verification techniques for verification of the source code comprising the loops with inputs of discrete values comprises an explicit state model checking technique and loop invariant generation techniques and the loop invariant generation techniques result in loop abstraction, wherein when the explicit state model checking technique cannot scale, two loop invariant generation techniques are applied simultaneously, wherein one of the loop invariant generation techniques uses fuzz testing and program syntax analysis to guess and check candidate loop invariants, and another of the loop invariant generation techniques is a counter-example guided loop abstraction refinement (CEGLAR) technique that havocs output variables of each loop subject to application of the another of the loop invariant generation techniques and applies induction to each loop subject to application of the another of the loop invariant generation techniques containing user properties to generate an abstracted loop; and
displaying a verification result as one of a verification successful (S) when the one or more specifications hold for all program executions, a verification failure (F) when any specification from the one or more specifications failed to hold for at least one program execution, and unknown (U) when one or more of the specifications is not verified or the verification technique run out of time or memory.

2. The method of claim 1 , further comprising selecting a plurality of default verification techniques upon elapse of a respective predetermined period of time to verify a corresponding property by the plurality of verification techniques.

3. The method of claim 1 , wherein the source code comprises the multiple return paths, wherein the plurality of verification techniques comprises one or more inter procedural verification techniques for the verification of the source code with the multiple return paths, the one or more inter procedural verification techniques comprising the interval analysis followed by bounded model checking, wherein when the source code is not verified with the verification result as unknown (U), then a next verification technique in the predefined order is determined.

4. The method of claim 1 , wherein a verification technique, from the plurality of verification techniques, for verification of the source code having the one or more loops with the unstructured control flow comprises random testing.

5. The method of claim 1 , wherein a verification technique, from the plurality of verification techniques, for verification of the source code comprising the loops with arrays comprises a plurality of array abstraction techniques, wherein the plurality of array abstraction techniques comprises array pruning followed by loop shrinking, wherein the specification is verified with respect to a subset of array elements in the source code or the specification is verified with respect to loop iterations, wherein the plurality of array abstraction techniques validate user properties or assertions for a subset of array elements to verify the source code with an improved scalability, wherein when the array abstraction techniques run out of time and memory with the verification result as unknown (U), then a default verification technique is applied on the source code.

6. The method of claim 1 , wherein when the abstracted loop produces a counter-example, loop invariants are checked to eliminate all paths leading to the counter-example and continued until the verification results in success (S) or failure (F).

7. The method of claim 2 , wherein the plurality of default verification techniques comprises carrying out an execution sequence comprising interval analysis including a k-path interval analysis invoked twice, first with k=1 aiming at scalability and later with k=500 for precision, loop abstraction followed by bounded model checking (BMC) in which each loop is replaced by an abstract loop of known bounds, apply the BMC to the source code with bounds produced by the interval analysis to show absence of errors, loop summarization to analyze interleaving of unique paths within a respective loop to produce a disjunctive summarization of the respective loop to find errors or proofs, the bounded model checking is applied when the loop summarization is inconclusive and generates the unknown (U) verification result and performs a heuristic search for bounds that calls the BMC multiple times asserting if all loops in the source code is unwound to invalidate an input property of the source code, and k-induction.

8. The method of claim 1 , wherein the static analysis is performed by carrying out an analysis of the one or more program features in a predefined sequential order.

9. The method of claim 1 , wherein the static analysis is performed by carrying out an analysis of the one or more program features in parallel.

10. A system for verification of a source code comprising:
at least one memory; and
one or more hardware processors, the at least one memory coupled to the one or more hardware processors wherein the one or more hardware processors are capable of executing programmed instructions stored in the at least one memory to:
receive a source code encoded with one or more specifications to be verified;
perform static analysis of the source code to identify one or more program features of the source code, the one or more program features comprising at least one of multiple return paths, loops with an unstructured control flow, loops with arrays, loops with inputs of discrete values and numerical loops;
perform a structural analysis of a plurality of loops and an interval analysis of input values read in the plurality of loops to determine a predefined order of a plurality of verification techniques to verify the source code based on the plurality of loops and a program control flow;
apply the plurality of verification techniques associated with the one or more program features to the source code for the verification, wherein the source code comprises the loops with inputs of discrete values and numerical loops, wherein each verification technique of the plurality of verification techniques is applied for a predetermined period of time and in the predefined order, wherein a verification technique from the plurality of verification techniques for verification of the source code comprising the loops with inputs of discrete value

Assignees

• Tata Consultancy Services Ltd

Inventors

• Darke Priyanka
• Chimdyalwar Bharti
• Chauhan Avriti
• Shah Punit
• Kumar Shrawan
• Afzal Mohammad
• Ramanathan Venkatesh
• Datar Advaita
• Akhtar Asia
• Shah Tanha

Classifications

• G06F8/75

  Structural analysis for program understanding · CPC title

• G06F11/3604 Primary

  Analysis of software for verifying properties of programs (testing of software G06F11/3668) · CPC title

• G06F8/33

  Intelligent editors · CPC title

• G06F9/44589

  Program code verification, e.g. Java bytecode verification, proof-carrying code (high-level semantic checks G06F8/43; prevention of errors by analysis, debugging or testing of software G06F11/36) · CPC title

• G06F21/6209 Primary

  to a single file or object, e.g. in a secure envelope, encrypted and accessed using a key, or with access control rules appended to the object itself · CPC title