FORMAL VERIFICATION OF TCP/IP TRANSPORT LEVEL PROTOCOLS

                              Mark Smith
                              Bell Labs

TCP is the most widely used protocol for reliable data delivery across
the internet.  To provide reliable data delivery, TCP goes through
three phases: *open*, *data transfer*, and *close*. In the open phase,
a connection is established by synchronizing the states at both
end-points. Data is sent in the data transfer phase, and in the close
phase the state associated with the connection is deleted.  Depending
on the application, the open phase of TCP may be inefficient, and
there have been several protocols proposed to correct this
inefficiency.  In the data transfer phase, TCP uses a cumulative
acknowledgment (ACK) mechanism to recover from lost packets.  This
mechanism may also be inefficient and proposals have been made to
rectify this inefficiency.  In this talk we present work in the formal
verification of a protocol proposed to improve the efficiency of the
open phase of TCP, and of a mechanism proposed to improve the rate at
which TCP recovers from losses.

The first protocol we examine is T/TCP.  While TCP works well for
sending large amounts of data, it is inefficient for small
transactions because of the overhead due to the open phase.  A
transaction is typically just a request and a response.  Unlike other
protocols proposed to provide efficient transactions, the goal of
T/TCP is not to perform efficient transactions all the time, but only
under certain conditions. However, in examining T/TCP we observed that
in certain situations the protocol may deliver the same message twice,
even when efficient transactions are not required. This observation
led us to consider whether any protocol can deliver streams of data
reliablely and still have fast transactions under the same conditions
required by T/TCP. We present a formal definition of what it means to
provide fast transactions and reliable message delivery under the
conditions proposed by the designers of T/TCP, and prove that without
"accurate" clocks, it is impossible for any protocol to solve this
problem.

The selective acknowledgment (SACK) mechanism is supposed to improve
the performance of TCP when multiple packets are lost from one window
of data.  SACK is being proposed as a new standard option for TCP.
With selective acknowledgment, non-contiguous blocks of data can be
acknowledged, and the sender only has to retransmit data that is
actually lost.  The proposed mechanism for implementing the SACK
option for TCP is sufficiently complicated that it is not obvious that
it is safe. We present a formal proof that SACK does not violate the
safety properties of the ACK mechanism currently used with TCP.  We
also show that SACK can improve the time it takes for the sender to
recover from multiple packet losses by using the additional
information at the sender.  Additionally, we show that SACK can
improve performance even with window sizes as small as four packets
and in situations where acknowledgment packets are lost.


-- 
Rance Cleaveland (rance@cs.sunysb.edu)
Tel:   (516) 632-8448 (voice), (516) 632-8334 (fax)
WWW:   http://www.cs.sunysb.edu/~rance
Post:  Dept. of Comp. Sci., SUNY at Stony Brook, Stony Brook, NY 11794-4400