Clarification on Minimum Segment Length Requirement

[mlimbeck]

CC: @jcp19

While verifying the correctness of the router within the context of VerifiedSCION, I encountered a discrepancy between the documentation in the SCION book and the actual implementation. The book states, "Additionally, all segments without the Peering flag need to consist of at least two HFs. ... A SCION router therefore must verify that these rules were followed correctly, see §5.6.3." (§5.5 Path Construction, p.104). However, this requirement does not appear to be enforced in the code.

This could potentially result in routing issues. For example, consider a network configuration where A connects to B, B connects to C, and B serves as the parent for both A and C (A <-- B --> C). If the rule requiring a minimum segment length of two is not enforced, a valid packet routing from A to C could contain three segments:

Pkt { 
  [A, B]
  [B]
  [B, C]
}

In this scenario, at AS B, there would be two segment switches: one at the ingress router (p.doXover()) and another at the egress router (p.processEgress()). This situation violates our formal models of the protocol and §5.6.3 in the book, which states that the CurrINF is only allowed to be increased (segment switch) at the ingress router and not at the egress router (p.119 and p.120).

Could you confirm whether this check is indeed missing, or if it is enforced in another part of the system? Any clarification would be greatly appreciated.

Thank you for your help.

[mlimbeck]

I wanted to check if you've had a chance to look into the issue and could provide any clarification?

[matzf]

Hey @mlimbeck, thanks for reporting this! I think you're right, this is indeed a bug. I was able to create a packet with such a path that is forwarded by the router.

Below is a hacky patch that mis-purposes an existing test case to create such a packet. This patched test fails, confirming the bug (run bazel test //acceptance/router_multi:test_nobfd).

test-4524.patch

diff --git a/tools/braccept/cases/child_to_child_xover.go b/tools/braccept/cases/child_to_child_xover.go
index 74ec549e9..801c2b13f 100644
--- a/tools/braccept/cases/child_to_child_xover.go
+++ b/tools/braccept/cases/child_to_child_xover.go
@@ -67,10 +67,10 @@ func ChildToChildXover(artifactsDir string, mac hash.Hash) runner.Case {
 			PathMeta: scion.MetaHdr{
 				CurrHF:  1,
 				CurrINF: 0,
-				SegLen:  [3]uint8{2, 2, 0},
+				SegLen:  [3]uint8{2, 1, 2},
 			},
-			NumINF:  2,
-			NumHops: 4,
+			NumINF:  3,
+			NumHops: 5,
 		},
 		InfoFields: []path.InfoField{
 			// up seg
@@ -79,6 +79,12 @@ func ChildToChildXover(artifactsDir string, mac hash.Hash) runner.Case {
 				ConsDir:   false,
 				Timestamp: util.TimeToSecs(time.Now()),
 			},
+			// core seg
+			{
+				SegID:     0x333,
+				ConsDir:   false,
+				Timestamp: util.TimeToSecs(time.Now()),
+			},
 			// down seg
 			{
 				SegID:     0x222,
@@ -89,6 +95,7 @@ func ChildToChildXover(artifactsDir string, mac hash.Hash) runner.Case {
 		HopFields: []path.HopField{
 			{ConsIngress: 511, ConsEgress: 0},
 			{ConsIngress: 0, ConsEgress: 151},
+			{ConsIngress: 141, ConsEgress: 0},
 			{ConsIngress: 0, ConsEgress: 141},
 			{ConsIngress: 411, ConsEgress: 0},
 		},
@@ -96,6 +103,7 @@ func ChildToChildXover(artifactsDir string, mac hash.Hash) runner.Case {
 	sp.HopFields[1].Mac = path.MAC(mac, sp.InfoFields[0], sp.HopFields[1], nil)
 	sp.InfoFields[0].UpdateSegID(sp.HopFields[1].Mac)
 	sp.HopFields[2].Mac = path.MAC(mac, sp.InfoFields[1], sp.HopFields[2], nil)
+	sp.HopFields[3].Mac = path.MAC(mac, sp.InfoFields[2], sp.HopFields[3], nil)
 
 	scionL := &slayers.SCION{
 		Version:      0,
@@ -130,34 +138,12 @@ func ChildToChildXover(artifactsDir string, mac hash.Hash) runner.Case {
 		panic(err)
 	}
 
-	// Prepare want packet
-	want := gopacket.NewSerializeBuffer()
-	ethernet.SrcMAC = net.HardwareAddr{0xf0, 0x0d, 0xca, 0xfe, 0x00, 0x14}
-	ethernet.DstMAC = net.HardwareAddr{0xf0, 0x0d, 0xca, 0xfe, 0xbe, 0xef}
-	ip.SrcIP = net.IP{192, 168, 14, 2}
-	ip.DstIP = net.IP{192, 168, 14, 3}
-	udp.SrcPort, udp.DstPort = udp.DstPort, udp.SrcPort
-	if err := sp.IncPath(); err != nil {
-		panic(err)
-	}
-	if err := sp.IncPath(); err != nil {
-		panic(err)
-	}
-	sp.InfoFields[0].UpdateSegID(sp.HopFields[1].Mac)
-	sp.InfoFields[1].UpdateSegID(sp.HopFields[2].Mac)
-
-	if err := gopacket.SerializeLayers(want, options,
-		ethernet, ip, udp, scionL, scionudp, gopacket.Payload(payload),
-	); err != nil {
-		panic(err)
-	}
-
 	return runner.Case{
 		Name:     "ChildToChildXover",
 		WriteTo:  "veth_151_host",
-		ReadFrom: "veth_141_host",
+		ReadFrom: "no_pkt_expected",
 		Input:    input.Bytes(),
-		Want:     want.Bytes(),
+		Want:     nil,
 		StoreDir: filepath.Join(artifactsDir, "ChildToChildXover"),
 	}
 }
diff --git a/tools/braccept/main.go b/tools/braccept/main.go
index cddeed995..a8fa363c8 100644
--- a/tools/braccept/main.go
+++ b/tools/braccept/main.go
@@ -131,6 +131,10 @@ func realMain() int {
 		cases.ChildToPeer(artifactsDir, hfMAC),
 		cases.PeerToChild(artifactsDir, hfMAC),
 	}
+	// XXX ignore above, only run single case
+	multi = []runner.Case{
+		cases.ChildToChildXover(artifactsDir, hfMAC),
+	}
 
 	if *bfd {
 		multi = []runner.Case{