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.