Huginn-TCP Huginn-TCP Huginn-TCP is a formal model in HOL4 of TCP/IP which is validated against several TCP/IP stacks. The aim is to provide TCP/IP implementors with a turnkey system to find anomalies in their stack. Huginn-TCP includes a trace checker that validates a given trace, which consists of captured network frames, UNIX socket API calls, and changes to the TCP control block. The model encodes non-deterministic choices which are taken by existing TCP/IP implementations. The model is accompanied by an extensive test suite. Huginn-TCP is based on the 2000-2009 Netsem Network Semantics research project, which was validated against the FreeBSD-4.6, the Linux 2.4.20, and the Windows XP TCP/IP implementation. Huginn-TCP takes advantage of the current HOL4 proof system, which uses PolyML (instead of Moscow ML), and is already 20 times faster on average. The tracing subsystem is being replaced by DTrace (on FreeBSD-11), instead of a sockets wrapper, libpcap slurper, and a kernel ringbuffer. The testing subsystem is being rewritten to accommodate this change. Support for newer TCP features such as delayed ACK, selective ACK, LRO, TSO, are planned. People Hannes Mehnert Michael Norrish Peter Sewell Funding This work is funded by REMS: Rigorous Engineering of Mainstream Systems, EPSRC Programme Grant EP/K008528/1.
