router: strengthen the checks performed by parsePath

[jcp19]

This PR strengthens the checks performed by the parsePath method to address the issues #4524 and #4531. In particular, I added two checks:

• We check that the CurrHF field of the parsed path is compatible with the CurrINF field
• We check that non-peering segments have at least two hops

This PR is still not complete. I will add a test here after we prove, in VerifiedSCION, that these changes fix our issues. One question that I have regarding the code is whether we should return a malformedPath or a cannotRoute error. I chose the former, but I would be happy to change that if you think it makes more sense.

[jiceatscion]

This change is 

[matzf]

Thank you!
malformedPath seems perfectly appropriate to me.

Reviewed 1 of 2 files at r1, 1 of 1 files at r2, all commit messages.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @jcp19)

[matzf]

Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @jcp19)

a discussion (no related file):
There is a failing test (dataplane_test.go, TestProcessPkt/astransit_xover). Quite clearly, the path in the test setup is indeed broken (CurrINF = 0, CurrHF = 2, SegLen = {2,2,0}).
It appears that the test is still passing because the router logic accidentally still treats this as Xover -- (because CurrINF != infIndxForHF(CurrHF+1).

To fix this test case (i.e. to make it test what it should be testing), I suggest the following patch.
This fixes the order of the hop fields in the to something that seemingly makes sense and sets the starting CurrHF from 2 to 1. Also explicitly increment CurrINF instead of using incPath to make it explicit that a segment switch does occur in the test path.

diff --git a/router/dataplane_test.go b/router/dataplane_test.go
index 7750bb186..c315c75a0 100644
--- a/router/dataplane_test.go
+++ b/router/dataplane_test.go
@@ -1206,8 +1206,9 @@ func TestProcessPkt(t *testing.T) {
                                dpath := &scion.Decoded{
                                        Base: scion.Base{
                                                PathMeta: scion.MetaHdr{
-                                                       CurrHF: 2,
-                                                       SegLen: [3]uint8{2, 2, 0},
+                                                       CurrINF: 0,
+                                                       CurrHF:  1,
+                                                       SegLen:  [3]uint8{2, 2, 0},
                                                },
                                                NumINF:  2,
                                                NumHops: 4,
@@ -1219,20 +1220,23 @@ func TestProcessPkt(t *testing.T) {
                                                {SegID: 0x222, ConsDir: false, Timestamp: util.TimeToSecs(now)},
                                        },
                                        HopFields: []path.HopField{
-                                               {ConsIngress: 0, ConsEgress: 1},  // IA 110
                                                {ConsIngress: 31, ConsEgress: 0}, // Src
-                                               {ConsIngress: 0, ConsEgress: 51}, // Dst
+                                               {ConsIngress: 0, ConsEgress: 51}, // IA 110
                                                {ConsIngress: 3, ConsEgress: 0},  // IA 110
+                                               {ConsIngress: 0, ConsEgress: 1},  // Dst
                                        },
                                }
-                               dpath.HopFields[2].Mac = computeMAC(t, key, dpath.InfoFields[0], dpath.HopFields[2])
-                               dpath.HopFields[3].Mac = computeMAC(t, key, dpath.InfoFields[1], dpath.HopFields[3])
+                               dpath.HopFields[1].Mac = computeMAC(t, key, dpath.InfoFields[0], dpath.HopFields[1])
+                               dpath.HopFields[2].Mac = computeMAC(t, key, dpath.InfoFields[1], dpath.HopFields[2])

                                if !afterProcessing {
-                                       dpath.InfoFields[0].UpdateSegID(dpath.HopFields[2].Mac)
+                                       dpath.InfoFields[0].UpdateSegID(dpath.HopFields[1].Mac)
                                        return toMsg(t, spkt, dpath)
                                }
-                               require.NoError(t, dpath.IncPath())
+
+                               dpath.PathMeta.CurrHF++
+                               dpath.PathMeta.CurrINF++
+
                                ret := toMsg(t, spkt, dpath)
                                ret.Addr = &net.UDPAddr{IP: net.ParseIP("10.0.200.200").To4(), Port: 30043}
                                ret.Flags, ret.NN, ret.N, ret.OOB = 0, 0, 0, nil

---

[jcp19]

Hi @matzf, thank you for the guidance in fixing the test :)

Since the first version of this PR, I strengthened the check performed in parsePath -- turns out that the version I had before (which only checked that the current segment had at least two hops) would not reject packets for which the two following conditions hold simultaneously:

1. IncPath is called twice during processing (one in doXover and the other in processEgress)
2. the core segment has size one

In this setting, we would essentially be performing two Xovers and miss the check on the core segment.

We are now confident that this solution is correct but we need to finish the proof to be sure -- the proof is available here as a draft PR and it is currently failing on a lemma that broke due to changes in related definitions. I hope to fix this in the next days.

[jiceatscion]

Reviewed 2 of 2 files at r3, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @jcp19 and @matzf)

[matzf]

Oh nice catch.

Reviewed 2 of 2 files at r3, 2 of 2 files at r4, all commit messages.
Reviewable status: all files reviewed, 2 unresolved discussions (waiting on @jcp19)

---

router/dataplane_test.go line 1222 at r4 (raw file):

				dpath.PathMeta.CurrHF++
				dpath.PathMeta.CurrINF++

Small merge issue (causing the test to fail); the logic for "afterProcessing" was moved (as part of some restructuring in #4539). Previously this logic was here after if !afterProcessing { ... return }, now it is in the if block, if afterProcessing { _here_ } .
Replace require.NoError(t, dpath.IncPath() a few lines above, inside the if block, with these dpath.PathMeta.CurrHF/INF++ statements.

[jcp19]

@matzf Should be ready to merge now :)

[matzf]

Reviewed 1 of 1 files at r5, all commit messages.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @jcp19)

[jcp19]

Reviewed 1 of 2 files at r1, 1 of 2 files at r4, 1 of 1 files at r5, all commit messages.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @jcp19)