Open mlimbeck opened 1 month ago
I wanted to check if you've had a chance to look into the issue and could provide any clarification?
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
).
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:
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 theCurrINF
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.