From owner-freebsd-net@FreeBSD.ORG Mon Mar 28 19:38:32 2005 Return-Path: Delivered-To: freebsd-net@freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id 052D416A4CE for ; Mon, 28 Mar 2005 19:38:32 +0000 (GMT) Received: from mta1.cl.cam.ac.uk (mta1.cl.cam.ac.uk [128.232.0.15]) by mx1.FreeBSD.org (Postfix) with ESMTP id 224AA43D46 for ; Mon, 28 Mar 2005 19:38:31 +0000 (GMT) (envelope-from peter.sewell@cl.cam.ac.uk) Received: from stem.cl.cam.ac.uk ([128.232.9.62] helo=cl.cam.ac.uk) by mta1.cl.cam.ac.uk with esmtp (Exim 3.092 #1) id 1DG04E-0001F2-00 for freebsd-net@freebsd.org; Mon, 28 Mar 2005 20:38:30 +0100 To: freebsd-net@freebsd.org Date: Mon, 28 Mar 2005 20:38:29 +0100 From: Peter Sewell Message-Id: Subject: Rigorous specification for TCP, UDP, and Sockets X-BeenThere: freebsd-net@freebsd.org X-Mailman-Version: 2.1.1 Precedence: list List-Id: Networking and TCP/IP with FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 28 Mar 2005 19:38:32 -0000 [apologies to anyone who has seen this on the end-to-end list] Our recent technical reports may be of interest to BSD TCP/IP developers: TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview UCAM-CL-TR-624 Volume 2: The Specification UCAM-CL-TR-625 They are available from together with the summary paper: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. These give a detailed and precise specification of the behaviour of three common TCP/IP stacks - versions of FreeBSD, Linux, and Windows XP - as seen from socket calls and the wire interface. The specification has been validated through extensive testing (primarily against FreeBSD for the TCP aspects). It models the actual observed behaviour, bugs and all, rather than an idealisation of the RFCs. The specification is annotated for the non-specialist reader, and we hope that it will be useful as an informal reference for stack implementors and for sockets users (supplementing the existing RFCs and books), as well as supporting automated conformance testing. Our techniques may be useful in the development of new protocols and extensions. We would greatly appreciate feedback, on both content and usability. Peter, for the Netsem team: Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough