diff --git a/netkat/BUILD.bazel b/netkat/BUILD.bazel index dfea3d7..eda5106 100644 --- a/netkat/BUILD.bazel +++ b/netkat/BUILD.bazel @@ -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"], diff --git a/netkat/frontend.cc b/netkat/frontend.cc new file mode 100644 index 0000000..c649242 --- /dev/null +++ b/netkat/frontend.cc @@ -0,0 +1,31 @@ +#include "netkat/frontend.h" + +#include + +#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 diff --git a/netkat/frontend.h b/netkat/frontend.h new file mode 100644 index 0000000..d525f2d --- /dev/null +++ b/netkat/frontend.h @@ -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 + +#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_ diff --git a/netkat/frontend_test.cc b/netkat/frontend_test.cc new file mode 100644 index 0000000..dd14eea --- /dev/null +++ b/netkat/frontend_test.cc @@ -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 SingleLevelPredicateDomain() { + return OneOf(Just(Predicate::True()), Just(Predicate::False()), + Map(Match, Arbitrary(), Arbitrary())); +} + +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