Automated software verification service

Patent metadata

Field	Value
Publication number	US-11232015-B2
Application number	US-202016864713-A
Country	US
Kind code	B2
Filing date	May 1, 2020
Priority date	Sep 5, 2018
Publication date	Jan 25, 2022
Grant date	Jan 25, 2022

Abstract

A method for verifying source code for a program includes determining that a new version of the source code is available. One or more verification tools are determined to use for verification of the new version of the source code from a verification specification associated with the source code. A plurality of verification tasks to perform for the verification of the new version of the source code are automatically determined from the verification specification associated with the source code. The plurality of verification tasks for the new version of the source code are automatically performed using the one or more verification tools. A determination is then made as to whether the new version of the source code is verified.

First claim

What is claimed is:

1. A computer-implemented method of coordinating verification activity of source code, comprising:
receiving a request to verify the source code for a program;
determining one or more verification tools to use for verification of the source code;
determining a plurality of verification tasks to perform for the verification of the source code;
instantiating a plurality of virtual resources comprising the one or more verification tools;
for at least a first virtual resource and a second virtual resource of the plurality of virtual resources:
determining, from the plurality of verification tasks, one or more first verification tasks performed by the one or more verification tools of the first virtual resource and one or more second verification tasks performed by the one or more verification tools of the second virtual resource;
causing the first virtual resource to perform, for the source code, the one or more first verification tasks, and the second virtual resource to perform, for the source code, the one or more second verification tasks using the corresponding one or more verification tools; and
receiving one or both of first output of the first virtual resource and second output of the second virtual resource, the first and second outputs associated with the verification of the source code;
wherein receiving one or both of the first output and the second output comprises:
receiving the first output before receiving the second output; and
responsive to receiving the first output, causing the second virtual resource to cease performing the one or more second verification tasks for the source code;

determining output information associated with the plurality of virtual resources performing the plurality of verification tasks for the source code, the output information based at least in part on one or both of the first output and the second output; and
outputting a result of the verification based on the output information.

2. The method of claim 1 , wherein the one or more first verification tasks and the one or more second verification tasks are performed in parallel as a first verification stage, and wherein the output information defines an operating state of the source code at an end of the first verification stage, the method further comprising:
determining, of the plurality of verification tasks, one or more next verification tasks defining a second stage of the verification that follows the first stage, the one or more next verification tasks depending on the operating state of the source code at the end of the first verification stage;
causing at least one of the plurality of virtual resources to perform, for the source code, at least one corresponding task of the one or more next verification tasks; and
receiving second stage output of the plurality of virtual resources, the output resulting from performance of the one or more next verification tasks, wherein the output information used to determine the result is further based at least in part on the second stage output.

3. The method of claim 1 , further comprising:
determining a computer environment for the verification of the source code from at least one of the request or configuration information referenced in the request; and
generating the computer environment for the verification of the source code, wherein the computer environment comprises memory resources, processing resources, and a number of hardware instances comprising the memory resources and the processing resources, wherein the one or more virtual resources are instantiated in the computer environment.

4. The method of claim 1 , wherein outputting the result comprises outputting generic information that is generic to the one or more verification tools, and outputting tool-specific information that is specific to a first verification tool of the one or more verification tools.

5. The method of claim 1 , wherein the first virtual resource comprises a first configuration of the one or more verification tools and the second virtual resources comprises a second configuration of the one or more verification tools, and wherein:
causing the first virtual resource to perform the one or more first verification tasks and the second virtual resource to perform the one or more second verification tasks comprises causing the first virtual resource and the second virtual resource to perform a first verification task of the plurality of verification tasks in parallel; and
causing the second virtual resource to cease performing the one or more second verification tasks for the source code comprises:
determining, based on the first output, that the first virtual resource has completed the first verification task; and
causing the second virtual resource to cease performing the first verification task for the source code.

6. A method of using a single application programming interface (API) to coordinate verification activity of source code, comprising:
receiving at the API a first request to verify a first source code for a program;
determining a first configuration of a set of verification tools to use for verification of the first source code based on a first verification specification included in the first request, wherein the first configuration comprises first settings for a first verification tool of the set of verification tools and second settings for the first verification tool different from the first settings;
causing a first plurality of virtual resources comprising the set of verification tools to perform verification of the first source code using the first configuration, wherein causing the first plurality of virtual resources to perform the verification of the first source code comprises:
configuring a first virtual resource of the first plurality of virtual resources to use the first settings for the first verification tool;
configuring a second virtual resource of the first plurality of virtual resources to use the second settings for the first verification tool; and
causing the first virtual resource and the second virtual resource to perform one or more verification tasks in parallel using the first verification tool;

receiving at the API a second request to verify a second source code for the program;
determining a second configuration of the set of verification tools to use for verification of the second source code based on a second verification specification included in the second request, wherein the second source code is different from the first source code;
causing a second plurality of virtual resources comprising the set of verification tools to perform verification of the second source code using the second configuration; and
outputting a result of the verification of the second source code.

7. The method of claim 6 , further comprising:
generating a first queue comprising a first plurality of verification tasks associated with the verification of the first source code by the set of verification tools;
instantiating the first plurality of virtual resources according to the first configuration; and
while at least one of the first plurality of verification tasks is in the first queue:
removing a next verification task from the first queue;
causing a first virtual resource of the first plurality of virtual resources to perform the next verification task using the set of verification tools;
receiving a first result of the next verification task; and
outputting the first result.

8. The method of claim 7 , further comprising:
generating a second queue comprising the first plurality of verification tasks; and
while at least one of the first plurality of verification tasks is in the second queue:
removing a next verification task from the second queue

Assignees

• Amazon Tech Inc

Inventors

• Hortala Juan Rodriguez
• Rungta Neha
• Tuttle Mark R
• Tasiran Serdar
• Tautschnig Michael
• Nedic Andrea
• Varming Carsten
• Cook John Byron
• Mclaughlin Sean

Classifications

• G06F11/3608 Primary

  using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013) · CPC title

• G06F9/54

  Interprogram communication · CPC title

• G06F8/65

  Updates (security arrangements therefor G06F21/57) · CPC title

• G06F2201/815

  Virtual · CPC title

• G06F9/5077

  Logical partitioning of resources; Management or configuration of virtualized resources (specific details on emulation or internal functioning of virtual machines G06F9/455) · CPC title