Potential Issue with CurrHF and CurrINF Relationship After Decoding

[mlimbeck]

Hi everyone,
CC: @jcp19

While proving the correctness of the router in the context of VerifiedSCION, I tried to confirm that the current Infofield (CurrINF) and the current Hopfield (CurrHF) point to the same segment after decoding. Within the codebase, there exists the following function:

func (s *Base) infIndexForHF(hf uint8) uint8 {
	switch {
	case hf < s.PathMeta.SegLen[0]:
		return 0
	case hf < s.PathMeta.SegLen[0]+s.PathMeta.SegLen[1]:
		return 1
	default:
		return 2
	}
}

However, this function is only used in incPath, which is called either when the packet leaves the AS or a segment switch is performed. This happens very late in the processing of a packet. This could lead to potential problems in the router. In particular, the checks validateHopExpiry() and verifyCurrentMAC() could be performed with the wrong Infofield.

I am not sure if it is possible to satisfy verifyCurrentMAC() in this way, but if it is, the router would incorrectly perform an xover step, which is not supposed to happen.

So far, I haven't found a concrete counterexample, but it seems that the missing check can have a significant impact. Do you think such a check is necessary, or was it intentionally left out?

Thank you for your help.

[jcp19]

More generally, at the moment, the router seems to assume that the path is valid if parsePath returns successfully. After that point, the router might use that path, e.g., it may reverse it and use the result as the path of a SCMP packet. If we don't check the property above, the router might essentially produce packets with invalid paths.

[matzf]

As the info field and hop field information together is protected by the MAC, I think that this can't be exploited to circumvent path authorization. Still, I agree that it would seem prudent to check for this, to avoid forwarding (or replying to) packets with malformed path data.
We already have a issue to add general validation to the parsing layer, #4278. I've updated that to note that CurrHF should be checked to be in range for the CurrINF. In the meantime, it would seem appropriate to add a specific check for this into parsePath, as you're alluding to.

By the way; the path parser currently rejects truncated paths (length shorter than required for indicated number of hop fields), but allows longer paths (i.e paths with trailing garbage). I wonder if this should be forbidden for the same reason.

[jcp19]

By the way; the path parser currently rejects truncated paths (length shorter than required for indicated number of hop fields), but allows longer paths (i.e paths with trailing garbage). I wonder if this should be forbidden for the same reason.

For the time being, we haven't found any case where trailing garbage in the path is problematic for the router. However, we are currently addressing/verifying the last assumptions in the router, so we should be able to tell soon if that is actually the case.

[matzf]

Fixed by #4556