p4gauntlet/gauntlet

Finding bugs in P4 compilers using translation validation.

The Gauntlet Tool Suite

• Requirements
  • Frameworks for Model-Based Testing
• Instructions
  • Generating a Random Program
  • Retrieving Gauntlet Semantics for a P4 Program
  • Validating a P4C Program
  • Model-Based Testing
  • Fuzz-Testing at Scale
• Fuzz-Testing Support Matrix
• Bugs Found in P4 Compilers
• Citing This Project

DISCLAIMER: This project recently switched to a C++-based interpreter, which is not as feature-complete. For example, parser loops and the core extern functions are not implemented yet. The parser semantics are also not well tested. If you are interested in the original and comprehensive Python-based interpreter, please check out the old branch.

Gauntlet is a set of tools designed to find bugs in programmable data-plane compilers. More precisely, Gauntlet targets the P4 language ecosystem and the P4-16 reference compiler (p4c).

The goal is to ensure that a P4 compiler correctly translates a given input P4 program to its target-specific binary. The compiler must not crash and preserve the semantics of the program as originally written. The suite has three major components:

1. Bludgeon, a fuzz tester that generates random P4 programs using libraries repurposed from p4c.

2. Translation Validation, which analyzes the intermediate representation of a program after each compiler pass and identifies potential discrepancies. We support translation validation for the open-source p4c compiler front- and mid-end libraries.

3. Model-based Testing, which infers input and and corresponding output for a particular P4 program and generates end-to-end test packets. We have currently implemented model-based testing for the bmv2 simple-switch and the Tofino hardware switch.

For more details and a broad overview of the concepts in Gauntlet, refer to our OSDI paper.

Requirements

This repository run best with a recent version of Ubuntu (18.04+). The minimum required Python version is 3.6 (f-strings).

All tools require p4c to be installed. The fuzz tester and P4-to-Z3 converter are also p4c extensions which need to be copied or symlinked into the extensions folder of the compiler. The do_install.sh contains detailed command instructions. Most dependencies can be installed by running ./do_install.sh in the source folder (Careful, the installation assumes root privileges and installs several large packages).

To check whether everything has been installed correctly you can run python3 -m pytest test.py -vrf. This will take about 30 minutes.

Frameworks for Model-based Testing

Model-based testing requires a full test harness. Gauntlet currently supports the bmv2 simple-switch and the Tofino packet test framework. The behavioral model can be installed running the installation script with the option ./do_install.sh INSTALL_BMV2=ON.

The Tofino test framework requires access to the SDK and a manual setup. Gauntlet's scripts assume that the folder is installed under tofino/bf_src. We typically run the installation script as ./tofino/bf_src/p4studio_build/p4studio_build.py --use-profile p416_examples_profile.

Instructions

Generating a Random Program

After successful installation, you can generate a random P4 program via the modules/p4c/build/p4bludgeon out.p4 --arch top command. To generate Tofino code, the flag needs to be set to modules/p4c/build/p4bludgeon --output out.p4 --arch tna. A typical crash checking workflow might be:

modules/p4c/build/p4bludgeon --output out.p4 --arch top && modules/p4c/build/p4test out.p4

Retrieving Gauntlet Semantics for a P4 Program

For debugging purposes, you can run

bin/get_p4_semantics out.p4

to retrieve the semantic representation of a particular P4 program. This will print the Z3 formula of each pipe in the package. These semantics can be used for equality comparison or test-case inference.

Validating a P4C Program

To validate that a program is compiled correctly by p4c, you can run

 modules/p4c/build/p4bludgeon --output out.p4 --arch top && bin/validate_p4_translation out.p4

bin/validate_p4_translation checks if a sequence of P4 programs are all equivalent to each other using the bin/check_prog_equality program as a sub routine. This sequence is produced by running p4c on an input P4 program. When p4c is run on an input P4 program, it produces a sequence of P4 programs, where each P4 program corresponds to the version of the input P4 program after a p4c optimization pass. This allows us to validate whether compilation/translation is working correctly and to pinpoint the faulty optimization pass if it isn't working correctly.

Model-Based Testing [DEPRECATED]

Model-based testing requires the behavioral model or the Tofino compiler to be installed. The correct binaries and include files need to be instrumented in the src/generate_p4_test.py file. An example command is

 modules/p4c/build/p4bludgeon --output out.p4 --arch v1model && bin/generate_test_case -i out.p4 -r

This sequence of commands will first generate a random program, infer expected input and output values, convert them to a test file (in this case, they are stf files) and finally run a full test. If the observed output differs from the expected output, the tool will throw an error. The -r flag denotes randomization of the input, it is optional. To run model-based testing for the Tofino back end, sudo will have to be used.

 modules/p4c/build/p4bludgeon --output out.p4 --arch tna && sudo -E bin/generate_test_case -i out.p4 -r --arch tna

Fuzz-Testing at Scale

We also include facilities to fuzz test the compilers at scale.

bin/test_random_progs -i 1000

To generate and compile a thousand programs using P4C's p4test.

sudo -E bin/test_random_progs -i 1000 --arch tna

To generate and compile a thousand programs using the Tofino compiler.

 bin/test_random_progs -i 1000 -v

To compile and validate a thousand programs using P4C's p4test.

 bin/test_random_progs -i 1000 --arch v1model -b

To generate and fuzz test a thousand programs on the simple switch.

 sudo -E bin/test_random_progs -i 1000 --arch tna -b

To generate and fuzz test a thousand programs on the Tofino compiler.

Fuzz-Testing Support Matrix

Architecture	Compiler	Bludgeon Support	Validation Testing	Model-based Testing
psa	p4c-bm2-psa	✔️	✔️	✔️
tna	p4c-bf	✔️	❌	✔️
top	p4test	✔️	✔️	❌
v1model	p4c-bm2-ss	✔️	✔️	✔️

Bugs Found in P4 Compilers

We also track the bugs we have found. A detailed breakdown can be found in the bugs folder.

Citing This Project

To cite our work please refer to our paper:

@inproceedings {gauntlet,
  title = {Gauntlet: Finding Bugs in Compilers for Programmable Packet Processing},
  booktitle = {14th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 20)},
  year = {2020},
  url = {https://www.usenix.org/conference/osdi20/presentation/ruffy},
  publisher = {{USENIX} Association},
  month = nov,
}

gauntlet's Issues

Specific passes cause z3 crash

We currently skip the flattening passes of the P4 compiler. The reason is that both the Header and the Struct flattening pass generate a whole new set of z3 constants. We do not create a mapping of these variables and the z3 solver crashes because it does not seem to be able to handle the complexity of the comparison.

In the future, we need to find a way how to accurately translate variable renaming.

• FlattenHeaders
• FlattenInterfaceStructs
• UniqueNames
• UniqueParameters
• Inline
• InlineActions
• InlineFunctions
• NestedStructs
• ExpandLookahead

Fix h_converter

There are several issues with the h converter. The type map pulls the wrong type. Header stacks and varbits are not supported yet.

Implement lpm and ternary matches

These are currently all implemented as exact matches.

Refactor Scope

Use global and local scope for contexts

Extern types are not correctly handled

Externs can have members, which is not reflected when a function has an extern has type. Currently, extern types are just generic sorts not DataTypeRefs.

Permutations may not capture all paths

The condition inference is still incomplete, needs work.

Untagle resolve_expr and resolve_references

These two are used arbitrarily in the code right now, causing a lot of head ache. Figure out where the calls are appropriate.

Fix ternary2-bmv2.p4

Very nasty program that causes p4z3 to emit a false positive. Involves action assignments using the out qualifier and ternary matching.

Implement methods defined in the spec

Add special case handling for extract and lookahead for example.

Code coverage

Instrument a script that measures how much of a p4c pass we are actually covering with a P4 program. This gives useful information about lack of coverage in some places.

Parser Loops not correctly implemented

^

Method overloading not supported

Clean up Type_Declaratios and Declarations

Tables Actions Methods etc are all Declarations, we should not need an extra P4Declaration object.
Same goes for Type_Declarations

Clean up Tables and Switch Statements

Because of several new features tables and switch statements have becoming really mess. Just clean this up.

Redesign the Interpreter

No use of z3 anywhere. Only use z3 at the end when a state object is returned.

Clarify use of directionless parameters in actions and random code generation

Fix constructorcallexpressions

Those are not correctly implemented.

Header Stacks not implemented

Header Unions and Stacks incorrectly implemented

Validity is not properly handled in unions, stacks should not need perform book-keeping on the next variable.

Scoping does not always work correctly.

There are some cases where scoping is incorrect. The tests have been added in tests/imported.

Clean up how tables are generated by the toz3 generator

Add check for correct inline handling

Detect missed optimizations

It would be nice if we can detect missed optimizations with this tool. One approach is to stop simplifying in Z3 and compare the non-simplified representation to the Z3-optimized version. If there is a difference we know there might be room for improvement. This approach is very imprecise, however.

Fix Type Inference

Gauntlet should do proper type inference. Right now we have a customized solution, which easily breaks and adds unnecessary complexity. Type inference should be done as a preliminary pass in toZ3.

Get rid of integers and booleans

Integers and booleans make everything unnecessary complex and hard to debug because of z3 type-checking issues. It would be nice if we only used bit vectors. However, this might require instrumenting the type map in the p4 compiler.

Handle SubSat and AddSat correctly

We ignore over and underflows currently. Need to implement expressions that are capable of checking boundary violations.

Type_control and type_parser should not be of type_extern

Cleaning this up might reduce the complexity of the code by a lot.

Test Case Reduction

Introduce a tool that is able reduce bugs we find in a reliable fashion.

Implement tests that check for variable shadowing

Mux can return P4ComplexTypes

Mux is an expression which can return two different variables depending on the input condition. Because Mux is an expression it can occur in assignment statements or function parameters, which do not support this type of branching. We need to find a good way to model state forking with expressions.

Fix enums

Enum still causes issues, the datatype must be able to return individual integer values while being interpretable as BitVecRef.

P4Index is broken

The way we handle semantic indexing is broken (for example, method calls do not work and we evaluate side effects twice). This should be fixed if we want to handle more complex, randomly generated programs.

StructInitializer not implemented

Types are messy.

The type handling in both the compiler and the python z3 generator are extremely messy right now. We have to take a closer look on how to structure and pass types to actions, declarations, and type definitions. All this should be consistent and should not really on specific type checks in the python code.

This has been a persistent issue and causes most issues in the z3 generator as of now.

Optimize tail recursion

The recursive approach we have to handle branching is nearing its limits. Python allows a recursion depth of a max 1000 which we occasionally hit. To optimize performance we need to clean up the recursion in the step() operation.

Use quantifier-free undefined checks

Sometimes we want to ignore differences in undefined behavior. For this we can use quantifiers. However, those checks can be very slow in Z3. Find a better way to work around undefined variables without assigning explicit semantics.

Varbits not handled

It is complicated to support varbits in z3. For now we convert varbit types to bits and evaluate them as such.
In the future, we need to add a data structure that will test every possible bit length for varbits.

Externs do not respect call order

There is no variable tracking the amount of calls regarding externs. This is a sideeffect we currently disregard

Fix generic types.

We need to perform lazy type lookups, otherwise we cannot handle generics in control and parsers properly.

Check that union validity is handled correctly

Overloading not fully implemented

There are some cases where method overloading leads to a crash. Mostly, when overloaded method are not part of an extern but global.

Implement header unions correctly

Header unions are just another header right now. This mostly leads to correct comparisons but is a technically incorrect implementation. Fix this by implementing a notion of "union" in z3 and python. Most of the complexity comes from the exclusivity of validity.

Get the actions right.

There is a bunch of confusion around pass by value and pass by reference which causes false positives in the z3 comparison stage.

First, we need to understand when values are pass by reference and adapt the z3 code generation accordingly.

Make parameters and type parameters a data class

For my sanity's sake...

Add flag that allows us to ignore specific programs from the command line

Makes the tool a bit more flexible, so that I do not have to maintain the failing tests all the time.

Table Properties not handled

• size
• meters
• counters
• implementation
• psa_implementation
• psa_direct_counter
• psa_direct_meter
• junk

CLean up tables and switch statements

Interaction between these is a bit messy right now and is painful to maintain. Ideally, switch statements should just proceed with the output of the switch statement.

Bug running generate testcase

Bug running generate testcase

Good afternoon,
I was trying to run the generate_test_case executable and there seems to be a problem. Can you please clarify if the problem is on my end?

Best regards,
Duarte Dias.

tldart@ubuntu:~/gauntlet$ sudo -E bin/generate_test_case -i out.p4 -r --arch tna
INFO:Converting p4 to z3 python with command /home/tldart/gauntlet/modules/p4c/build/p4toz3 out.p4 --output /home/tldart/gauntlet/validated/out/out.py -I /home/tldart/gauntlet/tofino/bf_src/install/share/p4c/p4include/  
ERROR:BEGIN ########################################
ERROR:Failed while executing:
/home/tldart/gauntlet/modules/p4c/build/p4toz3 out.p4 --output /home/tldart/gauntlet/validated/out/out.py -I /home/tldart/gauntlet/tofino/bf_src/install/share/p4c/p4include/  (...)

ERROR:Output:
[--Werror=unknown] error: Unknown option --output
/home/tldart/gauntlet/modules/p4c/build/p4toz3: Compile a P4 program
--help                                  Print this help message
--version                               Print compiler version
-I path                                 Specify include path (passed to preprocessor)
-D arg=value                            Define macro (passed to preprocessor)
-U arg                                  Undefine macro (passed to preprocessor)
-E                                      Preprocess only, do not compile (prints program on stdout)
-M                                      Output `make` dependency rule only (passed to preprocessor)
-MD                                     Output `make` dependency rule to file as side effect (passed to preprocessor)
-MF file                                With -M, specify output file for dependencies (passed to preprocessor)
-MG                                     with -M, suppress errors for missing headers (passed to preprocessor)
-MP                                     with -M, add phony target for each dependency (passed to preprocessor)
-MT target                              With -M, override target of the output rule (passed to preprocessor)
-MQ target                              Like -Mt, override target but quote special characters (passed to preprocessor)
--std {p4-14|p4-16}                     Specify language version to compile.
--nocpp                                 Skip preprocess, assume input file is already preprocessed.
--disable-annotations[=annotations]     Specify a (comma separated) list of annotations that should be ignored by
                                        the compiler. A warning will be printed that the annotation is ignored
--Wdisable[=diagnostic]                 Disable a compiler diagnostic, or disable all warnings if no diagnostic is specified.
--Wwarn[=diagnostic]                    Report a warning for a compiler diagnostic, or treat all warnings as warnings (the default) if no diagnostic is specified.
--Werror[=diagnostic]                   Report an error for a compiler diagnostic, or treat all warnings as errors if no diagnostic is specified.
--maxErrorCount errorCount              Set the maximum number of errors to display before failing.
-T loglevel                             [Compiler debugging] Adjust logging level per file (see below)
-v                                      [Compiler debugging] Increase verbosity level (can be repeated)
--top4 pass1[,pass2]                    [Compiler debugging] Dump the P4 representation after
                                        passes whose name contains one of `passX' substrings.
                                        When '-v' is used this will include the compiler IR.
--dump folder                           [Compiler debugging] Folder where P4 programs are dumped
--parser-inline-opt                     Enable optimization of inlining of callee parsers (subparsers).
                                        The optimization is disabled by default.
                                        When the optimization is disabled, for each invocation of the subparser
                                        all states of the subparser are inlined, which means that the subparser
                                        might be inlined multiple times even if it is the same instance
                                        which is invoked multiple times.
                                        When the optimization is enabled, compiler tries to identify the cases,
                                        when it can inline the subparser's states only once for multiple
                                        invocations of the same subparser instance.
--doNotEmitIncludes condition           [Compiler debugging] If true do not generate #include statements
--excludeFrontendPasses pass1[,pass2]   Exclude passes from frontend passes whose name is equal
                                        to one of `passX' strings.
--listFrontendPasses                    List exact names of all frontend passes
--excludeMidendPasses pass1[,pass2]     Exclude passes from midend passes whose name is equal
                                        to one of `passX' strings.
--toJSON file                           Dump the compiler IR after the midend as JSON in the specified file.
--ndebug                                Compile program in non-debug mode.
--testJson                              [Compiler debugging] Dump and undump the IR
--pp file                               Pretty-print the program in the specified file.
--p4runtime-file file                   Write a P4Runtime control plane API description to the specified file.
                                        [Deprecated; use '--p4runtime-files' instead].
--p4runtime-entries-file file           Write static table entries as a P4Runtime WriteRequest messageto the specified file.
                                        [Deprecated; use '--p4runtime-entries-files' instead].
--p4runtime-files filelist              Write the P4Runtime control plane API description to the specified
                                        files (comma-separated list). The format is inferred from the file
                                        suffix: .txt, .json, .bin
--p4runtime-entries-files files         Write static table entries as a P4Runtime WriteRequest message
                                        to the specified files (comma-separated list); the file format is
                                        inferred from the suffix. Legal suffixes are .json, .txt and .bin
--p4runtime-format {binary,json,text}   Choose output format for the P4Runtime API description (default is binary).
                                        [Deprecated; use '--p4runtime-files' instead].
--target target                         Compile for the specified target device.
--arch arch                             Compile for the specified architecture.
--loopsUnroll                           Unrolling all parser's loops
Additional usage instructions:
loglevel format is: "sourceFile:level,...,sourceFile:level"
where 'sourceFile' is a compiler source file and 'level' is the verbosity level for LOG messages in that file

ERROR:END ########################################
ERROR:Failed to translate P4 to Python.
Traceback (most recent call last):
  File "/home/tldart/gauntlet/bin/../src/generate_p4_test.py", line 652, in <module>
    main(arguments)
  File "/home/tldart/gauntlet/bin/../src/generate_p4_test.py", line 594, in main
    result = perform_blackbox_test(config)
  File "/home/tldart/gauntlet/bin/../src/generate_p4_test.py", line 536, in perform_blackbox_test
    main_formula, pkt_range = get_main_formula(config)
  File "/home/tldart/gauntlet/bin/../src/generate_p4_test.py", line 445, in get_main_formula
    pipes, result = get_prog_semantics(config)
  File "/home/tldart/gauntlet/bin/../src/generate_p4_test.py", line 141, in get_prog_semantics
    util.copy_file([p4_input, py_file], fail_dir)
  File "/home/tldart/gauntlet/src/util.py", line 40, in copy_file
    shutil.copy2(src_file, dst)
  File "/usr/lib/python3.8/shutil.py", line 435, in copy2
    copyfile(src, dst, follow_symlinks=follow_symlinks)
  File "/usr/lib/python3.8/shutil.py", line 264, in copyfile
    with open(src, 'rb') as fsrc, open(dst, 'wb') as fdst:
FileNotFoundError: [Errno 2] No such file or directory: '/home/tldart/gauntlet/validated/out/out.py'