Allow routers to own a subset of the interfaces of their AS - #439
Merged
Conversation
'WellConfigured' and 'PreWellConfigured' required the domain of 'neighborIAs' to be equal to the domain of 'external', i.e., they required every router to terminate all of the interfaces of its AS. This does not match the configuration that the control plane produces for an AS that is served by more than one border router: the loop in 'control.confExternalInterfaces' visits every interface of the topology and calls 'Connector.AddExternalInterface', which registers the link type and the neighboring IA of the interface before it splits on whether the interface is owned by this router, adding it either to 'external' or, when a sibling router terminates it, to 'internalNextHops'. The old condition was satisfiable, but only by configurations that the control plane never produces. The model dataplane of 'dataplane_spec_test.gobra' was one: it gave interface 4 a next hop without a link type and without a neighboring IA, which is the only way a router could hold a next hop for an interface of its AS under the old condition. Under the old condition, the link type of an interface terminated by a sibling router is absent from 'linkTypes', so the lookup in 'validateEgressID' yields 'topology.Unset' and the packet is rejected as malicious instead of being forwarded over the internal interface to that sibling. Note that this is a statement about the configurations the predicates describe, not about the proof: Gobra does not derive that the AS transit branch of 'process' is unreachable under the old condition (an 'assert false' placed there fails), because at the call site only the contract of 'validateEgressID' is available and it says nothing about 'linkTypes'. The obligations in that branch were, and remain, discharged non-vacuously. Both predicates now require the interfaces of this router and those of its siblings to be contained in the domain of 'neighborIAs' (which still coincides with the domain of 'linkTypes'), instead of requiring the domain of 'external' and that of 'neighborIAs' to be equal. This is not a weakening of the old condition, but a different one: since the old condition equated the domains of 'external' and 'neighborIAs' while keeping 'external' and 'internalNextHops' disjoint, requiring 'internalNextHops' to be contained in 'neighborIAs' now rejects every configuration that the old condition admitted with a non-empty 'internalNextHops'. No guarantee is weakened by this, as no caller relies on the direction that was dropped, and the postconditions of the router are unchanged. Neither condition is established by verified code. 'Connector' and the 'control' package are not verified, so 'PreWellConfigured' is a trusted assumption on the configuration that the control plane hands to a router, and 'testRun' is the only witness that it is satisfiable. This is why the model dataplane is updated here as well: it now models a router that terminates interfaces 1, 2, and 3, while interface 4 of the same AS is terminated by a sibling router. The two new lemmas 'KnownIfIDLemma' and 'getDomInternalNextHopsLemma' expose the resulting property that the link type of an egress interface is known whether the interface is terminated by this router or by a sibling, and 'validateEgressID' now uses them. Verified with Gobra (member isolation via '-i <file>@<line>'): every member whose contract mentions these predicates, namely 'Run', 'processSCION', 'processEPIC', 'processOHP', 'validateEgressID', 'process' and 'initMetrics', together with the two new lemmas and the model dataplane, reports 0 errors. Verifying the package as a single job is left to CI, as member isolation does not exercise how the members compose. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014yYe1p8b2h39BXE4EQRDTB
jcp19
commented
Sep 4, 2026
jcp19
marked this pull request as ready for review
September 4, 2026 19:55
jcp19
pushed a commit
that referenced
this pull request
Sep 5, 2026
master's #439 relaxed WellConfigured and PreWellConfigured so that a router need only terminate a subset of the interfaces of its AS, and added KnownIfIDLemma and getDomInternalNextHopsLemma alongside them. The conflicting hunks in router/dataplane_spec.gobra and router/dataplane_spec_test.gobra are resolved in favour of master's content, with this branch's renames of the getDom* accessors re-applied to it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Txb3nNXx2mRUF6uae7PsRL
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.