[Ufmrg] Proposal: The Verified Internet

[Hans-Dieter Hiep <[e-mail]>]

Dear Usable Formal Methods Research Group members,

Quick status update from my side, the below is a rough draft of a new 
concept I am working on: the "Verified Internet" is a full-stack formal 
model of the protocols employed to communicate on the Internet, making 
use of the Lean theorem prover [1] and seeking collaboration with the 
people working on CSlib [2].

It follows the 5 layers of the TCP/IP model where the functionality of 
each layer is formally specified. It also covers cross-layer functional 
and non-functional concerns, including security and privacy concepts 
such as confidentiality, integrity, and availability.

- Physical Layer: abstracting from the underlying physical techniques, 
most basically modeled as pushing bits/trits/etc. on some medium in 
spacetime. Scope is near-Earth, so Euclidean R^4 is fine here. No 
'intergalactic' ambitions, let's solve our Earthly problems first ;)

- Datalink Layer: abstract model for medium access control and the 
various techniques used to communicate within one network. The 
specification should be abstract enough to cover various kinds of 
implementations, such as Ethernet/Wi-Fi based networks and mesh 
networks, but also leave some room for innovation.

- Internetwork Layer: abstract model of the Internet Protocol on the 
data plane, and an abstraction that covers both BGP and SCION control 
planes, including control plane failure isolation.

- Transport Layer: abstract model of communication between ports, 
including data streams and datagrams. Again, should be broad enough to 
cover TCP, UDP, SCTP, but also MPTCP and other novel techniques applied 
at this level.

- Application Layer: end-to-end communication between processes, as if 
by a dumb pipe, including an abstract model of a BSD socket.

- Cross-layer concerns such as CIA. Abstracts from the details of 
cryptography, but should be able to cover concepts such as 'perfect 
secrecy', KQD protocols, and pre-shared keys such as PUFs.

The purpose is to *define* a formal specification of the Internet 
technology suite, already deployed widely, that allows vendors:
(a) to validate their implementation against as test oracle, and
(b) to verify/certify the correctness of their implementation against.

The model must be 'usable' in every domain, world-wide, including 
military/governmental and civil/non-governmental contexts, focusing on 
delivering high-assurance computer networking technology.

The specification approach is to keep the specs as simple/elegant as 
possible and to avoid higher-order arguments and complex mathematical 
structures (i.e. we use first-order logic and separation logic).

Includes an executable reference implementation, that can be used to 
check that the formal model indeed works w.r.t. current practice, but 
this reference implementation will not focus on delivering the highest 
possible performance. The specifications should be liberal enough to 
allow for such high performance implementations. We follow the 
traditional philosophy of the Internet (The design philosophy of the 
DARPA internet protocols, David D. Clark, 1988 [3]):

1. Continue despite loss of networks or gateways (survivability)
2. Support multiple communications services
3. Variety of networks (interoperability)
4. Distributed management of its resources
5. Cost effective
6. Permit host attachment with low effort (extensibility)
7. Resources used must be accountable

Fully aware that this project will be a multi-year multi-person 
endeavor. Having finally settled on a fixed academic position, I no 
longer have any reason not to start with this project, and am reasonably 
certain I will be able to lead it the coming 30 or so years. So no rush.

For additional motivation why such a 'verified Internet protocol stack' 
is urgently needed, see the recent publication:

CHAPTER 13 The Critical State of Cyberspace
Hans-Dieter Hiep
In Advances in Anti-Access and Area Denial (A2/AD): From Defensive 
Technologies to A Whole-of-Society Approach, NLARMS 2026 (Netherlands 
Annual Review of Military Studies), 2026, pp. 267-290
https://www.jstor.org/content/oa_chapter_edited/jj.40494811.19?seq=1

Do let me know if you are interested in working together on such a 
formalization effort, then we can set-up some common infrastructure and 
agree on ways of working together.

All the best, Hans-Dieter Hiep

[1] https://lean-lang.org/
[2] https://www.cslib.io/
[3] https://doi.org/10.1145/52325.52336