µTCP
TCP/IP implementation derived from HOL4 formal specification
In this project, we will bring µTCP to an initial stable release. It originates from the research project NetSem (by Peter Sewell et al), which developed an executable specification of TCP/IP in HOL4. This specification is tested against Linux, FreeBSD, and Windows. It is a precise model of what to expect and allow out in the wild - different from the hundreds of pages of RFCs.
µTCP has been manually translated to OCaml, and several design decisions have been taken. Some features are not in scope of µTCP. In this project, we will work on a stable release of µTCP, and focus on features (SACK, pluggable congestion control, path MTU discovery, ..), and do a lot of performance engineering.
- The project's own website: https://robur.coop
Run by robur
This project was funded through the NGI0 Commons Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101135429. Additional funding is made available by the Swiss State Secretariat for Education, Research and Innovation (SERI).
