Hi everyone,

First, I apologize if this report/question is a bit too hand-wavy at times, but while proving the correctness of the router in the context of VerifiedSCION, I noticed that something looks weird.

More concretely, in file pkg/slayers/path/scion/decoded.go, there are the following definitions, together with comments expressing a few assumptions about the structure of the scion packets:

const (
	// MaxINFs is the maximum number of info fields in a SCION path.
	MaxINFs = 3
	// MaxHops is the maximum number of hop fields in a SCION path.
	MaxHops = 64
)

While the restriction on MaxINFs looks OK, the restriction that we have at most 64 hop fields seems to not be enforced: when we decode a Base, we store in the field NumHops the sum of the lengths of all segments. The length of each segment cannot exceed 64, but their sums can. As far as I can tell, there is no check performed while forwarding a packet that NumINFs is less than 64. While processing a SCION packet, we eventually call IncPath, which has the effect of incrementing the field CurrHF in PathMeta. As far as I can tell, nothing so far prohibits this field from getting to value 64 (if its original value was 63). The problem here is that, when we serialize the output packet (including its packet), if its value is at least 64, we will only serialize its 6 least significant bits, instead of storing its full value (the operation that serializes the CurrHF is uint32(m.CurrHF&0x3F)<<24). As such, I believe that, as is, the router would allow sending packets whose paths are too long until a point when they become invalid and are dropped. Is my understanding correct?