Data flow tracking in program verification
Techniques for program verification are described. An exemplary method includes receiving a request to evaluate code based on a customized rule, the customized rule comprising one or more conditions for which the customized rule is applicable and one or more postconditions to indicate at least one check to perform for a given node in a graph for the code, wherein an application of the customized rule performs one or more of: an interleave between a backward analysis and forward analysis based on user-specified conditions, an analysis between sub-graphs by a query from a first sub-graph to a second sub-graph, and an operation on a sub-graph, storage of a result of the operation on the sub-graph, and usage of the stored result in a subsequent operation; generating a graph for the code; and evaluating the code by applying the customized rule to the generated graph.
1. A computer-implemented method comprising:
receiving a request to perform data flow tracking on identified code based on a customized rule comprising a first section to at least identify the customized rule, one or more preconditions to define conditions for which the customized rule is applicable, and one or more postconditions to indicate at least one check to perform, wherein the one or more preconditions and one or more postconditions are called by application programming interface (API) calls, wherein an application of the customized rule performs one or more of:
an interleave between a backward analysis and forward analysis based on user-specified conditions,
an analysis between sub-graphs by a query from a first sub-graph to a second sub-graph, and
an operation on a sub-graph, storage of a result of the operation on the sub-graph, and usage of the stored result in a subsequent operation;
generating a data flow graph for the identified code;
performing the data flow tracking on the identified code by applying the customized rule to the generated data flow graph; and
providing a result of the data flow tracking to a user.
2. The computer-implemented method of claim 1 , wherein the result comprises one or more of:
a determination of a successful rule evaluation;
a determination of whether a precondition evaluation was successful;
a last match result;
a last non-empty match result; and
an indication of a last operation evaluated, wherein a match result is a set of graph nodes matching a current step in the customized rule.
3. The computer-implemented method of claim 1 , wherein the data flow tracking comprises a forward data flow analysis in the data flow graph from a given node of the data flow graph.
4. A computer-implemented method comprising:
receiving a request to evaluate code based on a customized rule, the customized rule comprising one or more conditions for which the customized rule is applicable and one or more postconditions to indicate at least one check to perform for a given node in a graph for the code, wherein an application of the customized rule performs one or more of:
an interleave between a backward analysis and forward analysis based on user-specified conditions,
an analysis between sub-graphs by a query from a first sub-graph to a second sub-graph, and
an operation on a sub-graph, storage of a result of the operation on the sub-graph, and usage of the stored result in a subsequent operation;
generating the graph for the code; and
evaluating the code by applying the customized rule to the generated graph.
5. The computer-implemented method of claim 4 , wherein the customized rule includes a name for the customized rule and a message to be shown when evaluation of the code by applying the customized rule fails.
6. The computer-implemented method of claim 4 , wherein an output of the evaluating the graph on the code by applying the customized rule comprises one or more of:
a determination of a successful rule evaluation;
a determination of whether a precondition evaluation was successful;
a last match result;
a last non-empty match result; and
an indication of a last operation evaluated, wherein a match result is a set of graph nodes matching a current step in the customized rule.
7. The computer-implemented method of claim 4 , wherein the customized rule includes a filter to constrain which methods of the code to which the customized rule applies, wherein the filter is parameterized by a predicate and a quantifier.
8. The computer-implemented method of claim 4 , wherein the customized rule includes at least one core operation selected from an operation to separate a precondition from an associated postcondition, an operation to load intermediate match results, an operation to load intermediate match results, an operation to interleave a function into the customized rule, and an operation to limit a number of elements in a matching result, wherein the matching result is a set of graph nodes matching a current step in the customized rule.
9. The computer-implemented method of claim 4 , wherein the customized rule includes at least one transformer operation which returns a match result that potentially contains new elements.
10. The computer-implemented method of claim 4 , wherein the evaluation of the code includes performing a forward data flow analysis in the graph from a given node.
11. The computer-implemented method of claim 4 , wherein the evaluation of the code includes performing a backward data flow analysis in the graph from a given node.
12. The computer-implemented method of claim 4 , wherein the customized rule includes at least one operation which crosses a method boundary.
13. The computer-implemented method of claim 4 , wherein the request includes one or more of the customized rule, an identifier of a location of the customized rule, the code, and an identifier of a location of the code.
14. The computer-implemented method of claim 4 , wherein the customized rule is input into a graphical user interface that includes components for editing code, displaying the generated graph, and displaying violations of the customized rule in the displayed graph.
15. A system comprising:
a first one or more electronic devices to implement a code store service in a multi-tenant provider network; and
a second one or more electronic devices to implement a program verification service in the multi-tenant provider network, the program verification service including instructions that upon execution cause the program verification service to:
receive a request to evaluate code stored in the code store service based on a customized rule, wherein the customized rule comprises one or more conditions for which the customized rule is applicable and one or more postconditions to indicate at least one check to perform for a given node in a graph for the code, wherein an application of the customized rule performs one or more of:
an interleave between a backward analysis and forward analysis based on user-specified conditions,
an analysis between sub-graphs by a query from a first sub-graph to a second sub-graph, and
an operation on a sub-graph, storage of a result of the operation on the sub-graph, and usage of the stored result in a subsequent operation;
generate the graph for the code; and
evaluate the code by applying the customized rule to the generated graph.
16. The system of claim 15 , wherein the program verification service is to provide a graphical user interface that includes components for editing code, displaying the generated graph, and displaying violations of the customized rule in the displayed graph.
17. The system of claim 15 , wherein the request includes one or more of the customized rule, an identifier of a location of the customized rule, the code, and an identifier of a location of the code.
18. The system of claim 15 , wherein the customized rule includes a filter to constrain which methods of the code to which the customized rule applies.
19. The system of claim 15 , wherein the customized rule includes at least one transformer operation which returns a match result that potentially contains new elements.
20. The system of claim 15 , wherein the customized rule includes at least one core operation selected from an operation to separate a precondition from an associated postcondition, an operation to load intermediate match results, an operation to load intermediate match results, an operation to interleave a function into the customized rule, and an operation to limit a number of elements in a matching result, wherein the matching result is a set of graph nodes matching a current step in the customized rule.