p4-constraints

p4-constraints extends the P4 language with support for constraint annotations. These constraints can be enforced at runtime using the p4-constraints library.

The project currently provides two main artifacts:

1. A C++ library for parsing and checking constraints.
2. A command line interface (CLI) that takes as input a P4 program with constraints and a set of table entries, and reports if the table entries satisfy the constraints placed on their respective tables or not. (Note that the CLI is intended for testing and experimentation, not for production use.)

Check out these slides for a tour of p4-constraints (up to date as of May 2020).

Example - Entry Restrictions

An entry restriction is a constraint specifying what entries are allowed to be placed in a P4 table. Here is an example:

@entry_restriction("
  // Only match on IPv4 addresses of IPv4 packets.
  hdr.ipv4.dst_addr::mask != 0 ->
    hdr.ethernet.ether_type == IPv4_ETHER_TYPE;

  // Only match on IPv6 addresses of IPv6 packets.
  hdr.ipv6.dst_addr::mask != 0 ->
    hdr.ethernet.ether_type == IPv6_ETHER_TYPE;

  // Either wildcard or exact match (i.e., "optional" match).
  hdr.ipv4.dst_addr::mask == 0 || hdr.ipv4.dst_addr::mask == -1;
")
table acl_table {
  key = {
    hdr.ethernet.ether_type : ternary;
    hdr.ethernet.src_addr : ternary;
    hdr.ipv4.dst_addr : ternary;
    standard_metadata.ingress_port: ternary;
    hdr.ipv6.dst_addr : ternary;
    hdr.ipv4.src_addr : ternary;
    local_metadata.dscp : ternary;
    local_metadata.is_ip_packet : ternary;
  }
  actions = { ... }
}

The @entry_restriction says that a valid ACL table entry must meet three requirements:

1. It can only match on the IPv4 destination address of IPv4 packets.
2. It can only match on the IPv6 destination address of IPv6 packets.
3. It can only perform a wildcard or an exact match on the IPv4 address.

The first two requirements are to rule out undefined behavior. The third requirement captures the intent of the P4 programmer that the ACL table should not require general ternary matches on the destination address; the constraint documents this intent and let's us catch accidental ternary matches installed by the control plane at runtime.

Example - Action Restrictions

An action restriction is similar to an entry restriction, but is placed on a P4 action:

// Disallow multicast group ID 0, since it indicates "no multicast" in 
// `v1model.p4`.
@action_restriction("multicast_group_id != 0")
action multicast(bit<16> multicast_group_id) {
  standard_metadata.mcast_grp = multicast_group_id;
}

API

At a high level, p4-constraint's API consists of only two functions: one function for parsing constraints and one function for checking them.

/* p4_constraints/backend/constraint_info.h */

// Translates `P4Info` to `ConstraintInfo`.
//
// Parses all tables and actions and their p4-constraints annotations into an
// in-memory representation suitable for constraint checking. Returns parsed
// representation, or an error status if parsing fails.
absl::StatusOr<ConstraintInfo> P4ToConstraintInfo(
    const p4::config::v1::P4Info &p4info);

/* p4_constraints/backend/interpreter.h */

// Checks if a given table entry satisfies the constraints attached to its
// associated table/action.
//
// Returns the empty string if this is the case, or a human-readable nonempty
// string explaining why it is not the case otherwise. Returns an
// `InvalidArgument` if the entry's table or action is not defined in
// `ConstraintInfo`, or if `entry` is inconsistent with these definitions.
absl::StatusOr<std::string> ReasonEntryViolatesConstraint(
    const p4::v1::TableEntry& entry, const ConstraintInfo& constraint_info);

For those who seek more fine-grained control, the API also offers more low-level functions that are documented in the various header files.

Use cases

p4-constraints can be used as follows:

• As a specification language to further clarify the control plane API.
• In P4Runtime server implementations to reject ill-formed table entries.
• In the controller as a defense-in-depth check.
• During testing to check for valid vs invalid table entries.
  • To guide a fuzzer to valid table entries.

Building

Building p4-constraints requires Bazel, a C++11 compiler (or newer), and GMP. The latter can be installed on Ubuntu as follows:

apt-get install libgmp-dev

We inherit a few additional dependencies (Bison and Flex) from p4c; these are required for golden testing only and can be installed on Ubuntu as follows:

apt-get install bison flex libfl-dev

To build, run

bazel build //p4_constraints/...

To run all tests except golden tests, run

bazel test //p4_constraints/...

To run all tests including golden tests, run

bazel test //...

This may take a while when executed for the first time, as it will build p4c from source.

To see the output of a failed test, invoke it using bazel run like so:

bazel run //p4_constraints/frontend:lexer_test

MacOS

While building under MacOS is not officially supported, it currently works after executing the following commands, using Homebrew to install GMP:

# Install GMP.
brew install gmp && brew link gmp
# Tell linker (ld) where to find GMP so '-lgmp' works.
echo "build --linkopt='-L/usr/local/brew/lib'" > user.bazelrc

Docker

You can also build p4-constraint in a Docker container, for example:

docker build --tag p4-constraints .                 # Time to get coffee...
docker run --tty --interactive p4-constraints bash  # Open shell in container.
bazel test //...                                    # Run tests in container.

Golden tests

The easiest way to experiment with p4-constraints is to write a golden test. We provide Bazel rules run_p4check and diff_test to make this convenient. See the e2e_test/ folder -- in particular e2e_test/BUILD.bazel -- for examples of how to use them.

To run all golden tests, execute

bazel test //e2e_test/...

Recall that this will build p4c and requires Bison and Flex to be installed.

To see the output of a failed test, invoke it using bazel run like so:

bazel run //e2e_test:invalid_constraints_test

p4check

The p4check CLI allows invoking the p4-constraints library from the command line. The most convenient way to run p4check is using the run_p4check-rule, as is done for golden testing.

To learn how to invoke p4check manually, consult the source file or run

bazel run p4_constraints/cli:p4check -- --help

Constraint language

See docs/language-specification.md for a documentation of the constraint languages, or look at some example constraints in the .p4-files in the e2e_test folder.

Contributing

Feedback, suggestions, and contributions in the form of GitHub issues and pull requests are welcome and encouraged.

Source Code Headers

Please note that every file containing source code must include the following copyright header:

Copyright 2020 The P4-Constraints Authors

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

This can be done automatically using addlicense as follows:

addlicense -c "The P4-Constraints Authors" -l apache ./p4_constraints