Spyderisk / domain-network

Network domain model
Apache License 2.0
1 stars 0 forks source link

Bug in network connectivity inference sequence #151

Open mike1813 opened 2 weeks ago

mike1813 commented 2 weeks ago

Network paths are constructed from logical segments, each of which represents a subpath between two subnets through a single gateway device. These segments come in different types, which embody routing restrictions in the set up, and depend on whether the gateway just connects to the subnets, or provides one or both subnets.

Where a device provides a subnet, the asserted relationship is Subnet-providedBy-Gateway, so there is no Gateway-connectedTo-Subnet relationship. This is added by construction pattern HprLS+c, and used in subsequent patterns that create the segments. Then later on, the network path construction sequence uses these segments, but doesn't create paths where the segment is of a type that normally doesn't allow connections to be routed through the gateway.

Most logical segments are created by a series of patterns that take into account where the subnets on each side of the gateway may be accessible. This ensures that we don't get segments connecting two subnets via a mobile device (e.g., a laptop) if the laptop cannot access both subnets from the same physical location. The only exception to this is if one of the subnets is the Internet, which is assumed to be accessible from anywhere.

This creates a problem for logical segment generation between a cellular network backhaul (the core network that connects cells together) and other networks to which it is connected. The problem arises because the core router and backhaul network aren't in any location that is likely to be represented in the system model. The reason is that these assets are inferred to exist to support the cellular network, and in most situations we don't need to worry about attacks on them or controls to counter those attacks. (At least for public cellular networks, where they are secured by the cellular network operator - see issue #152).

Because it has no location, the usual patterns won't find logical segments for routes to or from the backhaul network. To handle this, the construction sequence that creates the inferred backhaul network, base stations and radio access networks (cells) associated with each asserted cellular network also includes segment creation patterns. The problem is that two of these (L3cCrC+OSg, CrCcL3+NSg) depend on Gateway-connectedTo-Subnet relationships added by construction pattern HprLS+c, but it is part of the later sequence.

Result: we don't get logical segments for routes into and out of the backhaul network, except from/to the Internet.

mike1813 commented 2 weeks ago

Strictly not related to this is the fact that the existing patterns for constructing cellular network backbone and access networks do not handle the possibility that the system modeller user may have included them explicitly in their model. In that situation, routers within the cellular network do have locations, so the normal segment generation patterns should work correctly.

This should be taken into account when fixing the logical segment generation sequence, or we may get duplicate segments where the user has included any of the infrastructure explicitly (as asserted assets). This implies we should also fix the patterns that create the backbone and access networks so they are not triggered if those assets are asserted.

Note that the updates required to do this should also address issue #152.

mike1813 commented 4 days ago

First step in solving #151 is to create a set of test cases.

Issue #152 affects routing from external networks via the backbone router and thence via base stations into RANs. In issue #151 we are interested in other devices connected to the RAN that are themselves providing other networks. Tests for issue #151 can therefore be based on one of the test cases for #152, but with an extra subnet connected via one of the phones or base stations.

Issue-152-Test-01c: has a public cellular network '5G' covering Spaces 1 and 2 (plus the World), with an asserted router in Space 3 connected to the Internet and providing the backbone network, and an asserted base station in Space2 providing the RAN there. In Space 1 there is a phone connected to 5G, and in Space 2 there are two such phones. There is a laptop connected to the Internet in the global public space 'World'. The devices run clients and services whose connections lead to modelling errors if no network path exists between their hosts, providing a convenient means to detect which network paths exist and support connections.

Test cases for issue #151 are based on this:

This collection is attached as Issue-151-Test-Cases-asserted.zip. Issue-152-Test-01c can be found via issue #152, if needed.

Initial test results with code incorporating fixes for issues #152 and #154 reveal two problems: