Automated software verification service

Patent metadata

Field	Value
Publication number	US-10664379-B2
Application number	US-201816122676-A
Country	US
Kind code	B2
Filing date	Sep 5, 2018
Priority date	Sep 5, 2018
Publication date	May 26, 2020
Grant date	May 26, 2020

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 using a distributed verification service to coordinate verification activity of source code, comprising:
receiving a request to verify the source code for a program;
determining, by a first serverless function, one or more verification tools to use for verification of the source code;
determining, by the first serverless function, a plurality of verification tasks to perform for the verification of the source code;
generating a queue comprising the plurality of verification tasks;
instantiating a plurality of virtual resources comprising the one or more verification tools;
for one or more virtual resources of the plurality of virtual resources, performing the following actions:
selecting a verification task for a feature of the program from the queue;
performing the verification task selected from the queue using the one or more verification tools; and
outputting a result of the verification task;

performing a first verification task by a first virtual resource comprising a first combination of verification tools;
performing the first verification task by a second virtual resource comprising a second combination of verification tools while the first verification task is performed by the first virtual resource;
determining that the first verification task has been completed by a first one of the first virtual resource and the second virtual resource; and
terminating the performance of the first verification task by a second one of the first virtual resource and the second virtual resource; and
updating a progress indication associated with the verification of the source code by a second serverless function based on results output by the one or more virtual resources.

2. The method of claim 1 , wherein the plurality of verification tasks are for a first verification stage and can be performed in parallel, and wherein results output by the one or more virtual resources together comprise one or more output artifacts that in combination define an operating state of the source code at an end of the first verification stage, the method further comprising:
storing the one or more output artifacts in a data store;
after the plurality of verification tasks in the queue are complete, adding a new plurality of verification tasks to the queue for a second verification stage; and
for the one or more virtual resources of the plurality of virtual resources, performing the following comprising:
selecting a new verification task for a next feature of the program from the queue, wherein the new verification task depends on the operating state of the source code;
performing the new verification task selected from the queue using the one or more verification tools and the operating state of the source code; and
outputting a new result of the new verification task.

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.

4. The method of claim 1 , further comprising:
searching a data store for virtual resource images comprising the one or more verification tools; and
identifying at least one virtual resource image comprising the one or more verification tools, wherein the one or more virtual resources are instantiated from the at least one virtual resource image.

5. A system comprising:
one or more memory devices; and
one or more processing devices, wherein each of the one or more processing devices is operatively coupled to at least one of the one or more memory devices, wherein the one or more processing devices are configured to:
detect that a new version of source code for a program is available;
responsive to detection that the new version of the source code is available, invoke a verification service;
automatically determine, via the verification service, one or more verification tools to use for verification of the new version of the source code from a verification specification associated with the source code;
automatically determine, via the verification service, a plurality of verification tasks to perform for the verification of the new version of the source code from the verification specification associated with the source code;

generate a queue comprising the plurality of verification tasks;
instantiate a plurality of virtual resources comprising the one or more verification tools;
for one or more virtual resources of the plurality of virtual resources, perform the following actions:
select a verification task for a feature of the program from the queue;
perform the verification task selected from the queue using the one or more verification tools; and
output a result of the verification task;

automatically perform, via the verification service, the plurality of verification tasks for the new version of the source code using the one or more verification tools;
perform a first verification task by a first virtual resource comprising a first combination of verification tools;
perform the first verification task by a second virtual resource comprising a second combination of verification tools while the first verification task is performed by the first virtual resource;
determine that the first verification task has been completed by a first one of the first virtual resource and the second virtual resource; and
terminate the performance of the first verification task by a second one of the first virtual resource and the second virtual resource; and
determine, via the verification service, whether the new version of the source code is verified.

6. The system of claim 5 , wherein the one or more processing devices are further configured to:
update a progress indication associated with the verification of the new version of the source code based on results output by the one or more virtual resources.

7. The system of claim 5 , wherein the one or more virtual resources of the plurality of virtual resources are further configured to perform the following comprising:
generate one or more output artifacts responsive to performing the verification task; and store the one or more output artifacts in a data store, wherein the one or more output artifacts are used to set a starting state for one or more further verification tasks.

8. The system of claim 5 , wherein the one or more processing devices are further configured to:
generate an object model of a verification stack, wherein the verification stack comprises a plurality of verification stages, wherein each of the verification stages comprises a different plurality of verification tasks, and wherein verification tasks in subsequent verification stages are dependent on the results of verification tasks from previous verification stages; and
perform a first plurality of verification tasks from a first verification stage; and
after completion of the first plurality of verification tasks, perform a second plurality of verification tasks from a subsequent verification stage.

9. The system of claim 5 , wherein the one or more processing devices are further configured to:
determine that a feature of the source code has a plurality of possible options; and
generate a separate verification task for two or more of the plurality of options.

10. The system of claim 5 , wherein the one or more processing devices are further configured to:
determine th

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

• G06F9/5038

  considering the execution order of a plurality of tasks, e.g. taking priority or time dependency constraints into consideration (scheduling strategies G06F9/4881 and subgroups) · CPC title

• G06F9/54

  Interprogram communication · CPC title

• G06F8/65

  Updates (security arrangements therefor G06F21/57) · 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

• G06F11/3608 Primary

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