diff --git a/netkat/BUILD.bazel b/netkat/BUILD.bazel index ff33fa3..0859015 100644 --- a/netkat/BUILD.bazel +++ b/netkat/BUILD.bazel @@ -276,14 +276,32 @@ cc_library( hdrs = ["paged_stable_vector.h"], ) +cc_library( + name = "counter_example", + srcs = ["counter_example.cc"], + hdrs = ["counter_example.h"], + deps = [ + ":evaluator", + ":packet_set", + ":packet_transformer", + "@com_google_absl//absl/container:flat_hash_set", + "@com_google_absl//absl/log:check", + "@com_google_absl//absl/status", + "@com_google_absl//absl/status:statusor", + ], +) + cc_library( name = "analysis_engine", srcs = ["analysis_engine.cc"], hdrs = ["analysis_engine.h"], deps = [ + ":counter_example", ":frontend", ":packet_set", ":packet_transformer", + "@com_google_absl//absl/log:check", + "@com_google_absl//absl/status:statusor", ], ) diff --git a/netkat/analysis_engine.cc b/netkat/analysis_engine.cc index 0996018..df2ffdd 100644 --- a/netkat/analysis_engine.cc +++ b/netkat/analysis_engine.cc @@ -14,6 +14,9 @@ #include "netkat/analysis_engine.h" +#include "absl/log/check.h" +#include "absl/status/statusor.h" +#include "netkat/counter_example.h" #include "netkat/frontend.h" #include "netkat/packet_set.h" #include "netkat/packet_transformer.h" @@ -26,9 +29,24 @@ bool AnalysisEngine::CheckEquivalent(const Predicate& left, packet_transformer_manager_.Compile(Filter(right).ToProto()); } -bool AnalysisEngine::CheckEquivalent(const Policy& left, const Policy& right) { - return packet_transformer_manager_.Compile(left.ToProto()) == - packet_transformer_manager_.Compile(right.ToProto()); +SuccessOrCounterExample AnalysisEngine::CheckEquivalent(const Policy& left, + const Policy& right) { + PacketTransformerHandle left_packet_transformer = + packet_transformer_manager_.Compile(left.ToProto()); + PacketTransformerHandle right_packet_transformer = + packet_transformer_manager_.Compile(right.ToProto()); + if (left_packet_transformer == right_packet_transformer) { + return SuccessOrCounterExample(); + } + absl::StatusOr counter_example = + CounterExample::CreateEquivalenceCounterExample( + left_packet_transformer, right_packet_transformer, + &packet_transformer_manager_); + // This is expected to succeed since we already checked that the policies are + // not the same and the Analysis Engine owns the PacketTransformerManager, so + // this cannot be out of scope when creating the CounterExample. + CHECK_OK(counter_example.status()); // Crash OK + return SuccessOrCounterExample(*counter_example); } bool AnalysisEngine::ProgramForwardsAnyPacket(const Policy& program, diff --git a/netkat/analysis_engine.h b/netkat/analysis_engine.h index 89ad63e..bfffc8c 100644 --- a/netkat/analysis_engine.h +++ b/netkat/analysis_engine.h @@ -21,6 +21,7 @@ #ifndef GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_ #define GOOGLE_NETKAT_NETKAT_ANALYSIS_ENGINE_H_ +#include "netkat/counter_example.h" #include "netkat/frontend.h" #include "netkat/packet_transformer.h" @@ -49,7 +50,22 @@ class AnalysisEngine { // Checks whether two policies are "equivalent", meaning they have the same // packets transformations, meaning Evaluate(left, packet) == Evaluate(right, // packet) for all packets. - bool CheckEquivalent(const Policy& left, const Policy& right); + // + // Returns a counter example (i.e. an object demonstrating the difference + // between the two policies) for the given `left` and `right` policies if the + // policies are not equivalent, or `Success` if the policies are equivalent. + // + // Example: + // SuccessOrCounterExample result = CheckEquivalent(l,r); + // if(!result.IsSuccess()) { + // CounterExample counter_example = result->GetCounterExampleOrDie(); + // ASSIGN_OR_RETURN(Packet input_from_left_but_not_right, + // counter_example.GetInputPacketInLeftButNotRight()); + // ... + // } + // + SuccessOrCounterExample CheckEquivalent(const Policy& left, + const Policy& right); // Returns whether any given packet, represented by the set of packets in // `packets`, is forwarded by `program`. A packet is considered "forwaded" if diff --git a/netkat/analysis_engine_test.cc b/netkat/analysis_engine_test.cc index 462e2f0..a525308 100644 --- a/netkat/analysis_engine_test.cc +++ b/netkat/analysis_engine_test.cc @@ -60,45 +60,54 @@ TEST(AnalysisEngineTest, CheckEquivalentSmokeTests) { TEST(AnalysisEngineTest, CheckPolicyEquivalentSmokeTests) { AnalysisEngine analyzer; // Checks Deny and Accept are equivalent to themselves but not each other. - EXPECT_TRUE(analyzer.CheckEquivalent(Policy::Deny(), Policy::Deny())); - EXPECT_TRUE(analyzer.CheckEquivalent(Policy::Accept(), Policy::Accept())); - EXPECT_FALSE(analyzer.CheckEquivalent(Policy::Accept(), Policy::Deny())); - EXPECT_FALSE(analyzer.CheckEquivalent(Policy::Deny(), Policy::Accept())); + EXPECT_TRUE( + analyzer.CheckEquivalent(Policy::Deny(), Policy::Deny()).IsSuccess()); + EXPECT_TRUE( + analyzer.CheckEquivalent(Policy::Accept(), Policy::Accept()).IsSuccess()); + EXPECT_FALSE( + analyzer.CheckEquivalent(Policy::Accept(), Policy::Deny()).IsSuccess()); + EXPECT_FALSE( + analyzer.CheckEquivalent(Policy::Deny(), Policy::Accept()).IsSuccess()); // Checks different policies are equivalent to themselves but are not // equivalent to each other. const Policy p1 = Sequence(Filter(Match("port", 10)), Modify("port", 20)); const Policy p2 = Sequence(Filter(Match("switch", 42)), Modify("port", 21)); - EXPECT_TRUE(analyzer.CheckEquivalent(p1, p1)); - EXPECT_TRUE(analyzer.CheckEquivalent(p2, p2)); - EXPECT_FALSE(analyzer.CheckEquivalent(p1, p2)); - EXPECT_FALSE(analyzer.CheckEquivalent(p2, p1)); + EXPECT_TRUE(analyzer.CheckEquivalent(p1, p1).IsSuccess()); + EXPECT_TRUE(analyzer.CheckEquivalent(p2, p2).IsSuccess()); + EXPECT_FALSE(analyzer.CheckEquivalent(p1, p2).IsSuccess()); + EXPECT_FALSE(analyzer.CheckEquivalent(p2, p1).IsSuccess()); // Checks Union of Policies are commutative. - EXPECT_TRUE(analyzer.CheckEquivalent(Union(p1, p2), Union(p2, p1))); + EXPECT_TRUE( + analyzer.CheckEquivalent(Union(p1, p2), Union(p2, p1)).IsSuccess()); // Check Union of Policies are associative. const Policy p3 = Filter(Match("dst_mac", 30)); - EXPECT_TRUE(analyzer.CheckEquivalent(Union(p1, Union(p2, p3)), - Union(Union(p1, p2), p3))); + EXPECT_TRUE( + analyzer + .CheckEquivalent(Union(p1, Union(p2, p3)), Union(Union(p1, p2), p3)) + .IsSuccess()); // Some Sequence of Policies are not commutative: modifying the same field // with different values in different order would result in different // policies. const Policy modify_port_1 = Modify("port", 10); const Policy modify_port_2 = Modify("port", 20); - EXPECT_FALSE( - analyzer.CheckEquivalent(Sequence(modify_port_1, modify_port_2), - Sequence(modify_port_2, modify_port_1))); + EXPECT_FALSE(analyzer + .CheckEquivalent(Sequence(modify_port_1, modify_port_2), + Sequence(modify_port_2, modify_port_1)) + .IsSuccess()); // Sequence(p1, p2) can be equivalent to Sequence(p2, p1) depending // on what's p1 and p2: e.g., modifying different fields in different order // would result in equivalent policies. // This is the PA-MOD-MOD-COMM axiom in the NetKAT paper. const Policy modify_dst_mac = Modify("dst_mac", 1); - EXPECT_TRUE( - analyzer.CheckEquivalent(Sequence(modify_dst_mac, modify_port_1), - Sequence(modify_port_1, modify_dst_mac))); + EXPECT_TRUE(analyzer + .CheckEquivalent(Sequence(modify_dst_mac, modify_port_1), + Sequence(modify_port_1, modify_dst_mac)) + .IsSuccess()); } // A netkat::Policy representing the given topology @@ -115,17 +124,21 @@ TEST(AnalysisEngineTest, TopologyTraversalIsAccepted) { Policy traverse_topo_from_s1 = Sequence( Modify("switch", 1), Iterate(topology), Filter(Match("switch", 3))); EXPECT_TRUE( - analyzer.CheckEquivalent(traverse_topo_from_s1, Modify("switch", 3))); + analyzer.CheckEquivalent(traverse_topo_from_s1, Modify("switch", 3)) + .IsSuccess()); Policy traverse_topo_from_s2 = Sequence( Modify("switch", 2), Iterate(topology), Filter(Match("switch", 3))); EXPECT_TRUE( - analyzer.CheckEquivalent(traverse_topo_from_s2, Modify("switch", 3))); + analyzer.CheckEquivalent(traverse_topo_from_s2, Modify("switch", 3)) + .IsSuccess()); Policy traverse_from_non_existing_switch = Sequence( Modify("switch", 42), Iterate(topology), Filter(Match("switch", 3))); - EXPECT_TRUE(analyzer.CheckEquivalent(traverse_from_non_existing_switch, - Policy::Deny())); + EXPECT_TRUE( + analyzer + .CheckEquivalent(traverse_from_non_existing_switch, Policy::Deny()) + .IsSuccess()); } // TODO(anthonyroy): Consider fuzzing some of these tests. Doing so requires a diff --git a/netkat/counter_example.cc b/netkat/counter_example.cc new file mode 100644 index 0000000..dfd7c09 --- /dev/null +++ b/netkat/counter_example.cc @@ -0,0 +1,105 @@ +// Copyright 2025 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. + +#include "netkat/counter_example.h" + +#include + +#include "absl/log/check.h" +#include "absl/status/status.h" +#include "absl/status/statusor.h" +#include "netkat/evaluator.h" +#include "netkat/packet_set.h" +#include "netkat/packet_transformer.h" + +namespace netkat { + +absl::StatusOr CounterExample::CreateEquivalenceCounterExample( + PacketTransformerHandle left_policy, PacketTransformerHandle right_policy, + PacketTransformerManager* packet_transformer_manager) { + if (left_policy == right_policy) { + return absl::InvalidArgumentError( + "Left and right policies are the same, cannot create a counter " + "example."); + } + if (packet_transformer_manager == nullptr) { + return absl::InvalidArgumentError( + "Packet transformer manager is null, cannot create a counter example."); + } + return CounterExample(left_policy, right_policy, packet_transformer_manager); +} + +CounterExample::CounterExample( + PacketTransformerHandle left_packet_transformer, + PacketTransformerHandle right_packet_transformer, + PacketTransformerManager* packet_transformer_manager) + : left_packet_transformer_(left_packet_transformer), + right_packet_transformer_(right_packet_transformer), + packet_transformer_manager_(packet_transformer_manager) { + // Compute the set of packets that are in L but not R, and vice versa. + PacketTransformerHandle left_diff_right_transformer = + packet_transformer_manager_->Difference(left_packet_transformer, + right_packet_transformer); + PacketTransformerHandle right_diff_left_transformer = + packet_transformer_manager_->Difference(right_packet_transformer, + left_packet_transformer); + + // Compute the input packet sets to the difference of the left and right + // policies and vice versa. + PacketSetHandle fullset = + packet_transformer_manager_->GetPacketSetManager().FullSet(); + input_packets_in_left_but_not_right_ = + packet_transformer_manager_->Pull(left_diff_right_transformer, fullset); + input_packets_in_right_but_not_left_ = + packet_transformer_manager_->Pull(right_diff_left_transformer, fullset); +} + +PacketTransformerHandle CounterExample::GetLeftTransformer() const { + return left_packet_transformer_; +} +PacketTransformerHandle CounterExample::GetRightTransformer() const { + return right_packet_transformer_; +} + +absl::StatusOr CounterExample::GetInputPacketInLeftButNotRight() const { + if (packet_transformer_manager_ == nullptr) { + return absl::InvalidArgumentError( + "Packet transformer manager is null, cannot get input packets in left " + "but not right."); + } + std::vector input_packets = + packet_transformer_manager_->GetPacketSetManager().GetConcretePackets( + input_packets_in_left_but_not_right_); + if (input_packets.empty()) { + return absl::NotFoundError("No input packets in left but not right found."); + } + return input_packets[0]; +} + +absl::StatusOr CounterExample::GetInputPacketInRightButNotLeft() const { + if (packet_transformer_manager_ == nullptr) { + return absl::InvalidArgumentError( + "Packet transformer manager is null, cannot get input packets in right " + "but not left."); + } + std::vector input_packets = + packet_transformer_manager_->GetPacketSetManager().GetConcretePackets( + input_packets_in_right_but_not_left_); + if (input_packets.empty()) { + return absl::NotFoundError("No input packets in right but not left found."); + } + return input_packets[0]; +} + +} // namespace netkat diff --git a/netkat/counter_example.h b/netkat/counter_example.h new file mode 100644 index 0000000..2d9d67e --- /dev/null +++ b/netkat/counter_example.h @@ -0,0 +1,105 @@ +// Copyright 2025 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. + +#ifndef GOOGLE_NETKAT_NETKAT_COUNTER_EXAMPLE_H_ +#define GOOGLE_NETKAT_NETKAT_COUNTER_EXAMPLE_H_ + +#include +#include + +#include "absl/container/flat_hash_set.h" +#include "absl/log/check.h" +#include "netkat/evaluator.h" +#include "netkat/packet_set.h" +#include "netkat/packet_transformer.h" + +namespace netkat { + +using OutputPackets = absl::flat_hash_set; + +// A counter example contains the difference between two policies and the +// corresponding input/output packets that belong to one policy, but not the +// other and vice versa. +// +// Note: The lifetime of `CounterExample` is dependent on the +// lifetime of the `PacketTransformerManager` that created it. +class CounterExample { + public: + // Creates a counter example for the given `left_policy` and `right_policy`. + // The counter example is defined as: + // counter example := Pull(left policy - right policy, FullSet) or + // counter example := Pull(right policy - left policy, FullSet). + // + // Returns an error if the `packet_transformer_manager` is null or if the + // `left_policy` and `right_policy` are the same. + static absl::StatusOr CreateEquivalenceCounterExample( + PacketTransformerHandle left_policy, PacketTransformerHandle right_policy, + PacketTransformerManager* packet_transformer_manager); + + PacketTransformerHandle GetLeftTransformer() const; + PacketTransformerHandle GetRightTransformer() const; + + // Returns the first arbitrary input packet that produces an output packet + // when run through the left transformer, but no output packet when run + // through the right transformer. Will return an error if the packet + // transformer manager is null or if the packet set is empty. + // The counterexample packet set is represented by the following: + // PacketSetHandle := Pull(left policy - right policy, FullSet). + absl::StatusOr GetInputPacketInLeftButNotRight() const; + + // Returns the first arbitrary input packet that produces an output packet + // when run through the right transformer, but no output packet when run + // through the left transformer. Will return an error if the packet + // transformer manager is null or if the packet set is empty. + // transformer. The counterexample is represented by the following: + // PacketSetHandle := Pull(right policy - left policy, FullSet). + absl::StatusOr GetInputPacketInRightButNotLeft() const; + + private: + CounterExample(PacketTransformerHandle left_packet_transformer, + PacketTransformerHandle right_packet_transformer, + PacketTransformerManager* packet_transformer_manager); + + PacketTransformerHandle left_packet_transformer_; + PacketTransformerHandle right_packet_transformer_; + PacketTransformerManager* packet_transformer_manager_; + PacketSetHandle input_packets_in_left_but_not_right_; + PacketSetHandle input_packets_in_right_but_not_left_; +}; + +// A success or counter example is a wrapper around a counter example. +// If the two policies compared in the analysis engine are the same, the +// SuccessOrCounterExample should have no counter example and return true when +// IsSuccess is called. Otherwise, if IsSuccess returns false, then the +// SuccessOrCounterExample will contain a counter example. +class SuccessOrCounterExample { + public: + SuccessOrCounterExample() = default; + explicit SuccessOrCounterExample(CounterExample counter_example) + : counter_example_(std::move(counter_example)) {} + + bool IsSuccess() const { return !counter_example_.has_value(); } + + const CounterExample& GetCounterExampleOrDie() const { + CHECK(counter_example_.has_value()); + return *counter_example_; + } + + private: + std::optional counter_example_; +}; + +} // namespace netkat + +#endif // GOOGLE_NETKAT_NETKAT_COUNTER_EXAMPLE_H_ diff --git a/netkat/switch_test.cc b/netkat/switch_test.cc index 73ffe91..99c4b84 100644 --- a/netkat/switch_test.cc +++ b/netkat/switch_test.cc @@ -81,9 +81,11 @@ TEST(NetkatSwitchTest, SingleStageSwitchReturnsCorrectPolicy) { EXPECT_CALL(*mock_stage, CleanUp()).WillOnce(Return(Modify("vrf", -1))); netkat::AnalysisEngine engine; - EXPECT_TRUE(engine.CheckEquivalent( - nk_switch.GetPolicy(), - Sequence(Filter(Match("vlan_id", 1)), Modify("vrf", -1)))); + EXPECT_TRUE(engine + .CheckEquivalent( + nk_switch.GetPolicy(), + Sequence(Filter(Match("vlan_id", 1)), Modify("vrf", -1))) + .IsSuccess()); } TEST(NetkatSwitchTest, MultiStageSwitchReturnsCorrectPolicy) { @@ -109,10 +111,13 @@ TEST(NetkatSwitchTest, MultiStageSwitchReturnsCorrectPolicy) { // The VLAN sets a VRF, the VRF remaps the VLAN. The resulting policy should // be as-if the VLAN is simply remapped... plus the metadata cleanup. netkat::AnalysisEngine engine; - EXPECT_TRUE(engine.CheckEquivalent( - nk_switch.GetPolicy(), - Sequence(Filter(Match("vlan_id", 1)), Modify("vlan_id", 2), - Modify("vrf", -1), Modify("rnd_tag", -1)))); + EXPECT_TRUE( + engine + .CheckEquivalent( + nk_switch.GetPolicy(), + Sequence(Filter(Match("vlan_id", 1)), Modify("vlan_id", 2), + Modify("vrf", -1), Modify("rnd_tag", -1))) + .IsSuccess()); } } // namespace diff --git a/netkat/table_test.cc b/netkat/table_test.cc index b69fa8a..f6fcb64 100644 --- a/netkat/table_test.cc +++ b/netkat/table_test.cc @@ -215,7 +215,8 @@ TEST(NetkatTable, MergeWithSameTableIsSemanticNoop) { AnalysisEngine engine; EXPECT_TRUE( - engine.CheckEquivalent(merged_table->GetPolicy(), table.GetPolicy())); + engine.CheckEquivalent(merged_table->GetPolicy(), table.GetPolicy()) + .IsSuccess()); } TEST(NetkatTable, MergeWithCopiedTableIsEquivalentToMergeWithSameTable) { @@ -235,10 +236,14 @@ TEST(NetkatTable, MergeWithCopiedTableIsEquivalentToMergeWithSameTable) { NetkatTable::Merge(copy_ctor_table, copy_ctor_table)); AnalysisEngine engine; - EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), - copy_assign_merged_table->GetPolicy())); - EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), - copy_ctor_merged_table->GetPolicy())); + EXPECT_TRUE(engine + .CheckEquivalent(merged_table->GetPolicy(), + copy_assign_merged_table->GetPolicy()) + .IsSuccess()); + EXPECT_TRUE(engine + .CheckEquivalent(merged_table->GetPolicy(), + copy_ctor_merged_table->GetPolicy()) + .IsSuccess()); } TEST(NetkatTable, MergeWithDifferentTablesIsCorrect) { @@ -263,12 +268,12 @@ TEST(NetkatTable, MergeWithDifferentTablesIsCorrect) { Sequence(Filter(Match("port", 2)), Modify("vrf", 3)), Sequence(Filter(Match("port", 3)), Modify("vrf", 4))); AnalysisEngine engine; - EXPECT_TRUE( - engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy)); + EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy) + .IsSuccess()); ASSERT_OK_AND_ASSIGN(merged_table, NetkatTable::Merge(table2, table1)); - EXPECT_TRUE( - engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy)); + EXPECT_TRUE(engine.CheckEquivalent(merged_table->GetPolicy(), expected_policy) + .IsSuccess()); } TEST(NetkatTable, MergeWithNonDeterminismIsError) {