Computer Science
Computer Science-2021.gz:143490
Computer Science
0e1fd92db864f2ff980108d955c25d47271af8eb
Component-Based Error Detection of P4 Programs∗

P4 is a domain-specific language to develop the packet processing of network devices. These programs can easily hide errors, therefore we give a solution to analyze them and detect predefined errors in them. This paper shows the idea, which works with the P4 code as a set of components and processes them one by one, while calculating their preand postconditions. This method does not only detect errors between the components and their connections, but it is capable to reveal errors, which are hidden in the middle of a component. The paper introduces the method and shows its calculation in an example.


Introduction
We introduce a component-based formal method to detect errors in P4 programs. The antecedent of the method is an error detection, which is based on a rule system [13]. With this idea, we approach the detection from backward and process the code from the smallest units to the biggest ones. This solution can not only check the error possibilities but give additional information about the code for the developer. The prototype of the tool, which is based on the method, is being implemented 1 .
P4 programs We work with the P4 language [5,2,6,1], which is a domainspecific programming language to develop the packet processing of network devices. When a packet arrives at a device as a bitstream, the P4 program gets that bitstream as the input and starts to work with it. In Figure 1 there is an example program. P4 programs work with the header information of a network packet. The developers can define what kind of header information they work with (rows 1-16). P4 programs have three main processing parts: parser, modifier, and deparser. The

Related Work
There are different approaches to analyze P4 programs.
There are tools, which work with the previous version of P4 -the P4 14 -although the main concept of these projects is similar to the new version. One of them is P4V [9], which deals with errors caused by reading or writing of invalid headers, the arithmetic overflow, and proper accessing of header stacks. It creates an annotated program from the input source and verifies it by checking the correctness of a first-order formula, which describes the execution of the program.
Vera [11] is another one, which works with symbolic execution, which starts with the generation of the parsable input packet, and then checks all possible execution path with the Symnet [12] static analysis tool. They investigate similar error cases, for example, header validity, implicit drops.
Assert-P4 [8] also works with P4 14 , and uses symbolic execution too, although they check program-specific errors, which can be described by the developer. Therefore it can check errors, which can not be detected only from the simple P4 source, but from an annotated P4 code. It translates the annotated P4 code to a C-model, and then it checks the different properties, which were given in the code, with symbolic execution.
There are other tools, which work with the actual version of P4 -the P4 16 . There is an approach, which does data flow analysis of P4 programs [4]. In this research, they used an extended version of a control-flow graph, the def-use graph. For all possible execution paths, they execute the data flow analysis, which collects the usage of the different variables and header information. Based on this collected data, their solution can detect errors like using an undefined field.
Although the previous projects are based on static analyzes, there are other solutions too. P4RL [10] does runtime verification, therefore it is able to analyze behaviors which are come from the control plane. The behavior of the network should be described by the user, therefore it can check if all of them are correct during the execution.
Another approach is SafeP4 [7], which is a domain-specific language, which was created to develop correct P4 programs.
Our solution works with the new version of P4 -the P4 16 . It is a static analyzer method, which uses only the P4 code as an input. Based on the code, we can extract the specification of the program, as pre-and postconditions, and we detect errors by analyzing the pre-and postconditions of the different components of the program and checking their relationship with the specification of the program. We detect errors, which can be caused by the usage of invalid header and uninitialized fields.

Motivation
P4 gives a new possibility for the protocol-independent development of the programmable switches. However developers can create more flexible programs, it is easier to make a mistake in them. That is the reason, why we need a tool, which can detect errors in our code.
As it was mentioned in the Introduction, the P4 programs do not define the whole behavior of the network, but a part of it. Therefore, some verification tools expect annotated programs and additional information about the planned behavior of the program, and they can check if those properties are correct or not. We would like to detect errors based on only the raw P4 code, therefore the developers will not have any other job besides developing the P4 program.
We would like to create a tool, based on our theoretical results, to help the developers to write correct P4 programs. In this first version of the method, we concentrate only on those errors to detect, which are caused by using invalid headers and uninitialized fields. Using them can cause undefined behavior by unknown values. However, we still work with the subset of the P4 language, but we plan to extend the rule system to work with a bigger language and detect more error cases.
This method is based on the precondition and postcondition of the program units. As we see in Figure 1, there are different programming structures in P4: actions, tables, control functions. It works with them one by one, and calculates condition pairs for each of them, starting from the smallest ones -like actionsfinishing with the biggest ones -like control functions.

Method of detection
The input of the method is the source code that will be checked. The whole process contains three main phases: the Pipeline Analyzer, the Parser/Deparser Analyzer, and the Final Checker. The Pipeline Analyzer has two parts: the call graph, and the Condition calculator. The Pipeline Analyzer checks all of the componentsactions, tables, and control functions -in the P4 source and calculates pre-and postcondition pairs for them while checking their correctness. The Parser/Deparser Analyzer works with the parser -gets the main precondition from it -and the deparser -gets the main postcondition from it. The Final Checker works with the calculated pieces of condition and checks that if every main precondition matches with at least one needed precondition. If the matching is not correct then it means that there are some errors in the code, because after the given parsing -which is described by the main precondition -there is not any execution path, which could work properly. However, if the matching is right in the preconditions then it checks the same with the postconditions.

Pipeline Analyzer
The analyzer consists of a call graph and the Condition Calculator. The call graph contains the relationship of the call between the control functions, tables, and actions. Based on the graph it will make an order of these components to be processed by the Condition Calculator. The Condition Calculator goes through all of them and creates their pairs of pre-and postcondition, which describes the correct working of the program.
This phase processes the modifier part of the P4 code, and calculate pre-and postconditions for the different components. The result of this phase shows the claim -what kind of header information it needs to work well -and the offering -what kind of header information it will create after the processing -of the component.

Call Graph
The call graph handles the modifier part of the input. Its vertices are the components of this part -the control functions, match-action tables, and actions -and the directed edges describe a calling relation between them.
The processing of the modifier part, in this version of the method, is the simplest packet processing path, where there is only an ingress pipeline. Therefore there is an initial vertex, which is the main ingress control function. The forwarding steps to process the whole control flow and whenever a component calls a componentif that has not been added to the graph as a vertex, it will create a vertex for itand will give an edge from the vertex of the calling component and the vertex of the called one.
After the processing of the code, it will create a list of the components. This list starts with those components, which do not depend on any other components,they have no outgoing edges -, it continues with components, which calls the components, which have already been added to the list, until the last two components, which will be the main function of the ingress. In the call graph there can not be any loop, because of the specification of the P4 language [6], which defines that neither direct recursion nor mutual recursion can be between actions and controls.
Condition calculator The list of the components gives a hint for the Condition Calculator in which order it should process the components, therefore whenever a command of a component's calling is processed, the condition of that component will have been calculated. During the processing of the components, it uses a rule system, which will calculate a ConditionState. Every condition consists of a valid and an invalid container, both of them contain a list of headers' and fields' names. During the method, we use the valid word as a synonym of the property of initialized fields. The Condition Calculator is defined by the operator , the type of which can be seen in Figure 4. It works with a known ConditionState, a name of a component -the one, that is processed when it uses this rule -and the program code. The rules are based on the structure of the program, therefore they have a deterministic usage. In this version of our method, we only work with the main structures of the program, therefore the rules only use a subset of the P4 language.
We define the behavior of the Condition Calculator with a rule system. It uses rewriting rules -we have an expression in the bottom and we rewrite it to the top of the rule. In Figure 5, there are the basic rules, which can be used for the subset of the P4 program. The rules for the assignment, sequence, table, skip, branch, table calling, and validity settings.
The preprocessing of the usage of the rules is to create the initial ConditionState. It is an empty state, where all of the components are stored, but all of them have only one condition, which says that the drop is invalid in the postcondition. The drop is a unique name in the conditions, which shows if the packet is dropped -it is valid, if it is dropped, and invalid if it is not dropped.
In the rules, we use some notations: • (A B) shows a rewriting from A to B. If the rewrote element has already been in a set, then it will be deleted from that place, and it will be only in the new set.
• ids means the type of the identifications. For example {ipv4, ipv4.ttl} is a set of ids i.e. {ids}.
• Ids is a function, which gives the names from an expression. For example the Ids of the "ipv4 .ttl − 1" is a {ipv4, ipv4.ttl}, which contains the identification of the header and the field of the expression.
• newIds is a function, which gives a subset of the Ids. These elements have not been used in any condition state.
• oldIds is a function, which gives a subset of the Ids. These elements have already been used in a condition state.
• f ields is a set of the identification of the fields of the given expression.
• header is a set of the identification of the headers of the given expression.
• C(conditionState, condition) calculates those pairs from the condition state, which fit to the condition.
• H.n shows the pre-and postcondition pairs of the component named n in the Condition State H.
• Empty(H.n) creates an empty block for the new component. * × merges the given conditions. If there is an ↑ in one side of the merging it means to use that condition as a prior one -if there is a header information, which appears in both conditions, the condition with the ↑ will be stored.
The rules The rules are based on the structure of the program, therefore the calculation is deterministic. On the sides of the rules, we can see two types of possible calculations. In the rules, there is the form H, n S, where H is a ConditionState, n is the name of the processed component and S is the P rogram that it processes. In one case, these rules can be recursively rewritten by the same form of expression -like in Rules 2, 6 -or in the other case it can be rewritten with a ConditionState -as in Rules 1, 3, 4, 5, 7, 8.
Rule 1 shows that the Skip does nothing, therefore the result will be the calculated condition state.
Rule 2 defines the processing of the sequence construct with composition -first, it processes the S1 program, and from the result of this calculation it processes the S2 program.
Rule 3 describes the assignment. Here we can see a side condition of the rule, which says to check if the identification of the expression expr -right side -and the header of the e -left side of the assignment -is valid. The side condition in this usage means, it will continue the calculation with those pairs of conditions, which are correct based on the side condition -in the pairs of conditions, where the side-condition is false, the process shows an error case. If the condition is true  Rule 6 gives the calculation of the branches. It needs to work with two different execution path -one where the condition is true, and one where it is false. If we check the actual condition state, it may contain several pairs of pre-and postcondition, therefore it describes both of the possible executions. In this rule, the calculation divides into two ways, these are calculated separately and their result will be joint.
Rule 7 calculates the conditions for the tables. It is important for the tables to read valid headers and initialized fields as keys. Although when this rule is used, we process a fresh component, therefore it does not need to use any sidecondition, because this condition will be described in the precondition.

Parser/Deparser Analyzer
The Parser/Deparser Analyzer is based on our previous paper [13]. It uses the parser to describe the main preconditions and the deparser to defines the main postconditions of the whole program. Therefore it describes the possible header information of the input and the output packets. The result of this is not pairs of conditions, but sets of pre-and postconditions. These conditions are not connected -are not in pairs -, they describe that what kind of initial states we would like to start our program and which final states are proper for the end.
There can be more main pre-and postconditions because parser and deparser can contain branches. In the main postconditions besides the conditions from the branches, there is another unique condition, which describes the case, when the packet is dropped. In this case, the drop is valid, and the validity of the other header information is irrelevant.

Final Checker
The task of the Final Checker to verify if the expected main pre-and postconditions of the program -which come from the Parser/Deparser Analyzer -and the actual pre-and postconditions fit well to each other. For this calculation we can generate a formula - Figure 6 from the calculated conditions and check if the formula is valid.  If there is an actual precondition, which does not fit the main precondition, it means, there is an execution path, which will not work properly. If there is an actual precondition, which fits a main precondition, but the postconditions are not fitting, it means, during the calculation of that execution path, there will not be any problem, but the final state will not be correct for the specification of the program -in this case, the deparser of the program.

Error detection cases
The method can detect error cases in four different ways. In the left one, act1 and act2 contains inside errors, which come from the bad usage of the method setValid () and setInvalid (). The side-effect of both methods is to change the uninitialized fields of the header. Therefore in the first case, when it would like to read the right side of the assignment, it will get a valid header and uninitialized field, so the read value is unknown. In the second case, on the left side of the assignment, it would like to write a field of an invalid header, which is an error case too. Both of them will be detected when it uses Rule 3, when the side-condition will be false in the process of the assignment.

Condition Calculator
On the right side of Figure 7, there is an example of the components, which are not matching. There are two components: the table t and a control function. The precondition of the table t is: V alid(ipv4, ipv4.dstAddr), because it reads the ipv4 .dstAddr field, so it need a valid header and initialized field. Although the true case of the branch says that the ipv4 is invalid -the postcondition of the control function stores it. Therefore when it uses Rule 8, it will not be able to merge the conditions, because the precondition of the table and the postcondition of the control function will not fit.  The first case is when the preconditions -of the main and the actual conditions -are matching, but there is no main postcondition, which fits the actual postcondition. In this case, although the program can start the execution from a good state, it will reach a state, which is not expected by the deparser -the calculated header information will be not correct for the program.
The second case is when there is no matching actual precondition for the main precondition. This means that starting from that input header information, the program will reach an error, the execution will be incorrect.   Based on the order of the list, the Condition Calculator starts the calculation from the expression, which is in Figure 10, where Empty is an initial ConditionState, which can be seen in Figure 9, which is mentioned in section 4.1.

Case study
(((Empty, "ipv4 create1" ipv4 create1), "ipv4 create2" ipv4 create2), "drop" drop), "t" t), "MyIngress" MyIngress Condition calculator The action ipv4 create1 consists of sequences -Rule 2 -of two assignments -Rule 3 -and one setting of validity -Rule 4. Therefore there will be three rewritings of the conditions. When it starts the processing, there is only one pre-and postcondition pair, where the only condition says that the drop is invalid. The process of the first assignment -hdr .ipv4 .srcAddr = hdr .ethernet.dstAddr -does not contain any side-condition, because it has just started the calculation. Therefore it will add the ethernet, ethernet.dstAddr and ipv4 to the Valid conditions in both of the pre-and postcondition -because it would read the right side, and it can only give value to a field of a valid header in the left side of the assignment. During the calculation, the postcondition describes the actual state. Therefore we will try to continue the process with the second assignment -hdr .ipv4 .dstAddr = dstAddr . The side-condition checks, if the header of the written field is valid -ipv4 is valid in the actual state or in the postcondition -, and if the read expression is valid -dstAddr is the parameter of the action, therefore the side-condition is not working with it. The validity is correct, so it adds the ipv4 .dstAddr to the Valid side of the postcondition -because after the assignment, its value will be initialized. After the assignments, the program tries to set the validity of the header ipv4 to valid. It changes only the postcondition by make all of the fields of ipv4 -ipv4 .srcAddr , ipv4 .dstAddr and ipv4 .ttl -invalid.
The calculation of the other actions similar to it, their results can be seen in Figure 11. After the actions, it processes the table t. It has one key, so first, it sets its header ethernet and field ethernet.dstAddr to Valid, as a precondition, because the program would like to read them -and of course, as a postcondition too, because that shows the actual condition. Then it checks and merges its conditions and the conditions of the actions together. Therefore there will be three pairs of conditions -because of the three actions. The precondition of action ipv4 create1 matches with the newly defined precondition of the table, therefore it can create the merged pre-and postcondition, where the condition of the action is the stronger one -in this case there is no conflict, so the condition pair of the action will be one of the table conditions.
The process of the other actions is similar. Their preconditions fit the precondition of the table, therefore it can merge their conditions. The conditions of the ingress MyIngress are the same as the table because it just simply calls it. The conditions of the table and ingress pipeline can be seen in Figure 12.
Parser/Deparser Analyzer The specification of the program is calculated from the parser and deparser. Both the parser and the deparser are really simple. None of them contains any branch, therefore there is only one possible precondition and two postconditions - Figure 13. The precondition describes the case when the parser extracts only the ethernet header, therefore this header and all of its fields will be valid, and the other header ipv4 and its fields will be invalid.
There can be two postconditions. One, which is defined by the deparser, where the packet is not dropped and both of the headers ethernet and ipv4 and all of their fields are valid -because the program will use their value for the new packet. The other case is when the packet is dropped. The main precondition assures only valid ethernet header information, although the first condition pair -rows 2-7. Figure 12 -of the actual condition needs a valid ipv4 header too. The first part of the formula is false, therefore the method can detect an error, which shows that this execution path of the program will not be able to execute well, because of the invalid ipv4 header.
In the second condition pair -rows 8-14. Figure 12-, the precondition fit to the main precondition, therefore it needs to check if the actual postcondition assures one of the main postconditions. The actual condition describes an execution when the packet was not dropped, therefore only the first main postcondition can be good, but we can see that in the actual postcondition the ipv4 .ttl field is invalid, but the main postcondition needs a valid one. It is another error case, which is detected and it shows the case when the execution is correct, but the final header information which is calculated does not match with the expected result by the deparser.
In the third condition pair -rows 15-20. Figure 12, the preconditions fit, and this is the case when the packet was dropped during the execution, therefore its postcondition will ensure the second main postcondition. This path shows a correct execution path.

Evaluation
We created a prototype for the Condition Calculator. The critical part of the implementation is the calls of the tables because this is the step when more and more condition states can be defined. Therefore Figure 14 shows the runtime based on different numbers of table calls. During the measurement only one table was used, which has 5 action calls -one NoAction, which is like a skip program; one drop action, which only signs the package to drop it; and three others, all of them contain sequences of simple assignments. In the graph of Figure 14, the vertical information is the number of table applications, and the horizontal data is the runtime in milliseconds. We can see three different lines because the implementation of the calculator is separated into two parts: a pre-calculator, which only prepares the obtained information; and the main condition calculator, which uses the prepared data to create the conditions. In the graph, the three different lines show the runtime of the pre-calculator (blue), the main calculator (orange), and the full time of them (grey). This graph shows the worst cases when all of the calculated conditions are different, therefore the number of the conditions is equal to the number of the actions to the power of the number of the table applications i.e. in our table there were 5 actions, and when we applied this table five times, then we could get 3125 conditions. However, we can see that, when we used 10 table applications, the runtime was only 13 seconds.
This presented data only give the worst runtime of this calculation, but when we use a normal P4 code then most of the conditions are the same, do the program will not work with this number of conditions.

Summary
In this paper, we introduced a formal method to detect errors in P4 programs by checking the pre-and postconditions. It has three main analyzers: the Parser/Deparser Analyzer, the Pipeline Analyzer, and the Final Checker. The method only works with the P4 source, therefore it extracts the specification of the program from the parser and deparser of it -by the Parser/Deparser Analyzer. The Pipeline Analyzer checks the definition of the pipeline, and calculated condition pairs for the different components of it -actions, match-action tables, and control functions. It can detect four different types of errors, which can be caused by the incorrect usage of invalid headers and uninitialized fields or components, which do not match.

Future Work
The method is a base of a full solution for P4 verification. Until this goal, we need to extend the checked subset of the P4 language, therefore we will be able to work with more programs. When both of our approach is ready -this, component-based and our previous idea [13] -, then it could be an interesting work to check which one is better in the specified error detections, and combine them for a more optimized solution. P4 programs can use different architectures. In this approach, we only showed the Protocol Independent Switch Architecture, which use a single pipeline, but there are other architecture models -for example Portable Switch Architecture [3] which can work with more pipelines. Our solution will be able to used as a part of a research, which checks if a P4 program is correct for a given architecture, while checking the correctness of a pipeline.