Data plane program verification

Abstract

A method for verifying data plane programs is provided in some embodiments. Because the behavior of a data plane program (e.g., a program written in the P4 language) is determined in part by the control plane populating match-action tables with specific forwarding rules, in some embodiments, programmers are provided with a way to document assumptions about the control plane using annotations (e.g., in the form of “assertions” or “assumptions” about the state based on the unknown control plane contribution). In some embodiments, annotations are added automatically to verify common properties, including checking that every header read or written is valid, that every expression has a well-defined value, and that all standard metadata is manipulated correctly. The method in some embodiments translates programs from a first language (e.g., P4) to a second language (e.g., Guarded Command Language (GCL)) for verification by a satisfiability modulo theory (SMT) solver.

What is claimed is: 
     
       1. A non-transitory machine-readable medium storing a verification program for execution by a set of processing units, the verification program for verifying the correctness of a forwarding-element program to be executed by a control-plane circuit to configure a data-plane circuit of a forwarding element to forward data messages, the forwarding-element program specifying at least one element that is populated during execution by a control plane circuit, the verification program comprising a set of instructions that when executed by the set of processing units results in performance of operations comprising:
 receiving the forwarding-element program; 
 annotating the forwarding-element program to reflect assumptions regarding control-plane behavior; 
 translating the forwarding-element program and annotations into a different programming language that incorporates non-deterministic choice based on the assumptions regarding control plane behavior; and 
 using the translated program to verify the correctness of the forwarding-element program and assumptions regarding the control plane behavior; 
 wherein:
 the data-plane circuit comprises a plurality of programmable packet processing stages that comprise match-action tables that are to be configured by the control-plane circuit for use in forwarding the data messages; and 
 the using the translated program to verify the correctness of the forwarding-element program and the assumptions regarding the control-plane behavior comprises verifying whether entries in the match-action tables depend on each other. 
 
 
     
     
       2. The non-transitory machine readable medium of  claim 1 , wherein the forwarding-element program specifies a set of tables to be executed by the data plane circuit, wherein the set of tables is populated by the control plane. 
     
     
       3. The non-transitory machine readable medium of  claim 2 , wherein for each table in the set of tables, a set of actions is specified in the forwarding-element program based on whether a match is found in the table. 
     
     
       4. The non-transitory machine readable medium of  claim 3 , wherein particular assumptions regarding control-plane behavior are assumptions regarding whether a match is found in a particular control-plane-populated table, wherein the set of non-deterministic choices reflect the different actions in the set of actions for the particular table. 
     
     
       5. The non-transitory machine readable medium of  claim 2 , wherein the translation and verification are performed before the tables are populated by the control plane. 
     
     
       6. The non-transitory machine readable medium of  claim 5 , wherein the correctness of the received forwarding-element program depends on the values used to populate, by the control plane, the tables specified in the forwarding-element program. 
     
     
       7. The non-transitory machine readable medium of  claim 1 , wherein the different programming language is guarded command language (GCL). 
     
     
       8. The non-transitory machine readable medium of  claim 7 , wherein the data-plane program is programmed in the P4 language. 
     
     
       9. The non-transitory machine readable medium of  claim 1 , wherein translating the received forwarding-element program comprises:
 parsing the received forwarding-element program to identify a set of variables in the forwarding-element program; and 
 identifying, for the different programming language, the corresponding type of each variable in the set of variables to apply in translating the forwarding-element program. 
 
     
     
       10. The non-transitory machine readable medium of  claim 1 , wherein translating the received forwarding-element program comprises translating assumptions included in the received forwarding-element program into a set of assumptions in the different programming language. 
     
     
       11. The non-transitory machine readable medium of  claim 1 , wherein translating the received data-plane program further comprises adding variables in the translated program that track the execution of tables and actions to be used in verifying the correctness of the forwarding-element program. 
     
     
       12. The non-transitory machine readable medium of  claim 11 , wherein added variables that track the execution of a table record at least one of (i) whether the table was reached, (ii) which values were read by the table, (iii) whether the packet hit or missed, (iv) which action was executed, and (v) which action data was supplied to the action. 
     
     
       13. The non-transitory machine readable medium of  claim 12 , wherein the added variables are used to trace the operations of the received forwarding-element program. 
     
     
       14. The non-transitory machine readable medium of  claim 12 , wherein the verification program further comprises a set of instructions for:
 displaying, when a forwarding-element program fails verification, a trace of the operations that caused the failure, the trace of operations based on the added variables. 
 
     
     
       15. The non-transitory machine readable medium of  claim 1 , wherein translating the received forwarding-element program comprises inlining the received forwarding-element program to eliminate at least a set of procedure calls and generate a single piece of translated code that fully captures the semantics of the received forwarding-element program. 
     
     
       16. The non-transitory machine readable medium of  claim 1 , wherein using the translated program to verify the correctness of the forwarding-element program comprises generating a set of conditions corresponding to both the received forwarding-element program and the translated program, the set of conditions being evaluated to verify the correctness of the received data-plane program. 
     
     
       17. The non-transitory machine readable medium of  claim 16 , wherein the set of conditions is a weakest set of conditions that are sufficient to insure that no assertions included in the translated program fail. 
     
     
       18. The non-transitory machine readable medium of  claim 17 , wherein the correctness of the data-plane program is verified using a satisfactory modulo theory (SMT) solver.