Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[NetKAT] Add the initial frontend C++ API. Starting with Predicate. #23

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 25 additions & 0 deletions netkat/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,31 @@ cc_proto_library(
deps = [":netkat_proto"],
)

cc_library(
name = "frontend",
srcs = ["frontend.cc"],
hdrs = ["frontend.h"],
deps = [
":netkat_cc_proto",
":netkat_proto_constructors",
"@com_google_absl//absl/strings:string_view",
],
)

cc_test(
name = "frontend_test",
srcs = ["frontend_test.cc"],
deps = [
":frontend",
":netkat_cc_proto",
":netkat_proto_constructors",
"//gutil:proto_matchers",
"@com_google_absl//absl/strings:string_view",
"@com_google_fuzztest//fuzztest",
"@com_google_googletest//:gtest_main",
],
)

cc_test(
name = "netkat_test",
srcs = ["netkat_test.cc"],
Expand Down
31 changes: 31 additions & 0 deletions netkat/frontend.cc
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
#include "netkat/frontend.h"

#include <utility>

#include "absl/strings/string_view.h"
#include "netkat/netkat.pb.h"
#include "netkat/netkat_proto_constructors.h"

namespace netkat {

Predicate operator!(Predicate predicate) {
return Predicate(NotProto(std::move(predicate).ToProto()));
}

Predicate operator&&(Predicate lhs, Predicate rhs) {
return Predicate(
AndProto(std::move(lhs).ToProto(), std::move(rhs).ToProto()));
}

Predicate operator||(Predicate lhs, Predicate rhs) {
return Predicate(OrProto(std::move(lhs).ToProto(), std::move(rhs).ToProto()));
}

Predicate Predicate::True() { return Predicate(TrueProto()); }

Predicate Predicate::False() { return Predicate(FalseProto()); }

Predicate Match(absl::string_view field, int value) {
return Predicate(MatchProto(field, value));
}
} // namespace netkat
125 changes: 125 additions & 0 deletions netkat/frontend.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,125 @@
// Copyright 2024 The NetKAT 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.
//
// -----------------------------------------------------------------------------
// File: frontend.h
// -----------------------------------------------------------------------------
//
// This file contains the definitions for the frontend facing NetKAT API.
// This API is how a majority of users are expected to build and manipulate
// NetKAT related policy.
//
// Under the hood, very minimal logic is performed at this stage. This API acts
// as a set of convenient helpers to generate a valid intermediate proto
// representation (IR). See `netkat.proto`.
#ifndef GOOGLE_NETKAT_NETKAT_FRONTEND_H_
#define GOOGLE_NETKAT_NETKAT_FRONTEND_H_

#include <utility>

#include "absl/strings/string_view.h"
#include "netkat/netkat.pb.h"

namespace netkat {

// Represents a NetKAT predicate.
//
// In general terms, a NetKAT predicate is some Boolean combination of matches
// on packets. Practically speaking, it is useful to think of predicates as a
// "filter" on the sets of packets at some given point in a NetKAT program.
//
// TODO: b/377697348 - create and point to resources/tutorials for NetKAT.
//
// This class provides overloads, and therefore support, for the given boolean
// operations: `&&`, `||` and `!`. These overloads follow conventional operation
// precedence order and, as per the literature, logically behave as expected.
// These overloads allow for convenient building of Predicates, for example:
//
// Predicate allowed_packets =
// Match("port", 1) && Match("vlan", 10) || Match("dst_mac", X);
//
// NOTE: SHORT CIRCUITING DOES NOT OCCUR! The following equivalent statements
// will generate differing protos:
//
// Predicate p1 = Predicate::True() || Predicate::False();
// Predicate p2 = Predicate::True();
// assert(!MessageDifferencer::Equivalent(p1.ToProto(), p2.ToProto());
//
// Internally this class simply builds a `PredicateProto` and does not
// *currently* perform any specific optimizations of the proto as it is built.
class Predicate {
public:
// We currently only allow predicate construction through helpers, e.g.
// `Match`, `True`, `False`.
Predicate() = delete;

// Returns the underlying IR proto.
//
// Users should generally not handle this proto directly, unless done with
// policy building.
PredicateProto ToProto() const& { return predicate_; }
PredicateProto ToProto() && { return std::move(predicate_); }

// TODO(anthonyroy): Add a FromProto.

// Logical operators. These perform exactly as expected, with the
// exception of short circuiting.
//
// These objects by themselves are not intrinsically truthy, so a lack of
// short circuiting will not generate semantically different sequences.
friend Predicate operator&&(Predicate lhs, Predicate rhs);
friend Predicate operator||(Predicate lhs, Predicate rhs);
friend Predicate operator!(Predicate predicate);

// Match operation for a Predicate. See below for the full definition. We
// utilize friend association to ensure program construction is well-formed.
friend Predicate Match(absl::string_view, int);

// Predicates that conceptually represent a packet being universally accepted
// or denied/droped.
//
// Concretely this is simply a constant `Predicate(true/false)`.
static Predicate True();
static Predicate False();

private:
// Hide default proto construction to hinder building of ill-formed programs.
explicit Predicate(PredicateProto pred) : predicate_(std::move(pred)) {}

PredicateProto predicate_;
};

// Represents a match on some field in the NetKAT packet. This is typically
// referred to as a "test" in the literature.
//
// Matches may be on any concrete packet field, switch local meta-fields, NetKAT
// specific fields (e.g. location), or even arbitrary labels introduced only for
// the specific programs.
//
// netkat::Match("ethertype", 0x0800) // L2 Header field.
// netkat::Match("dst_ip", X) // L3 Header field.
// netkat::Match("pkt_mark", Y) // OVS metadata field.
// netkat::Match("switch", Z) // Location for the NetKAT Automata.
// netkat::Match("has_foo", 0) // Custom program label.
//
// TODO: b/377704955 - Add type safety.
//
// Field verification is currently limited when using raw strings, both in type
// safety and naming. Prefer to use either enum<>string mappings OR constants
// rather than re-typing strings for field names.
Predicate Match(absl::string_view field, int value);

} // namespace netkat

#endif // GOOGLE_NETKAT_NETKAT_FRONTEND_H_
80 changes: 80 additions & 0 deletions netkat/frontend_test.cc
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
#include "netkat/frontend.h"

#include "absl/strings/string_view.h"
#include "fuzztest/fuzztest.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
#include "gutil/proto_matchers.h"
#include "netkat/netkat.pb.h"
#include "netkat/netkat_proto_constructors.h"

namespace netkat {
namespace {

using ::fuzztest::Arbitrary;
using ::fuzztest::Just;
using ::fuzztest::Map;
using ::fuzztest::OneOf;

void MatchToProtoIsCorrect(absl::string_view field, int value) {
EXPECT_THAT(Match(field, value).ToProto(),
EqualsProto(MatchProto(field, value)));
}
FUZZ_TEST(FrontEndTest, MatchToProtoIsCorrect);

TEST(FrontEndTest, TrueToProtoIsCorrect) {
EXPECT_THAT(Predicate::True().ToProto(), EqualsProto(TrueProto()));
}

TEST(FrontEndTest, FalseToProtoIsCorrect) {
EXPECT_THAT(Predicate::False().ToProto(), EqualsProto(FalseProto()));
}

// Returns a FUZZ_TEST domain that returns an arbitrary Match, True or False
// predicate. This allows us to provide fuzz tests with arbitrary Predicates to
// test on.
fuzztest::Domain<Predicate> SingleLevelPredicateDomain() {
return OneOf(Just(Predicate::True()), Just(Predicate::False()),
Map(Match, Arbitrary<absl::string_view>(), Arbitrary<int>()));
}

void NegateToProtoIsCorrect(Predicate predicate) {
Predicate negand = !predicate;
EXPECT_THAT(negand.ToProto(), EqualsProto(NotProto(predicate.ToProto())));
}
FUZZ_TEST(FrontEndTest, NegateToProtoIsCorrect)
.WithDomains(SingleLevelPredicateDomain());

void AndToProtoIsCorrect(Predicate lhs, Predicate rhs) {
Predicate and_pred = lhs && rhs;
EXPECT_THAT(and_pred.ToProto(),
EqualsProto(AndProto(lhs.ToProto(), rhs.ToProto())));
}
FUZZ_TEST(FrontEndTest, AndToProtoIsCorrect)
.WithDomains(/*lhs=*/SingleLevelPredicateDomain(),
/*rhs=*/SingleLevelPredicateDomain());

void OrToProtoIsCorrect(Predicate lhs, Predicate rhs) {
Predicate or_pred = lhs || rhs;
EXPECT_THAT(or_pred.ToProto(),
EqualsProto(OrProto(lhs.ToProto(), rhs.ToProto())));
}
FUZZ_TEST(FrontEndTest, OrToProtoIsCorrect)
.WithDomains(/*lhs=*/SingleLevelPredicateDomain(),
/*rhs=*/SingleLevelPredicateDomain());

void OperationOrderIsPreserved(Predicate a, Predicate b, Predicate c) {
Predicate abc = !(a || b) && c || a;
EXPECT_THAT(
abc.ToProto(),
EqualsProto(OrProto(
AndProto(NotProto(OrProto(a.ToProto(), b.ToProto())), c.ToProto()),
a.ToProto())));
}
FUZZ_TEST(FrontEndTest, OperationOrderIsPreserved)
.WithDomains(/*a=*/SingleLevelPredicateDomain(),
/*b=*/SingleLevelPredicateDomain(),
/*c=*/SingleLevelPredicateDomain());

} // namespace
} // namespace netkat
Loading