Next: Bugs Found Up: Model Checking Large Network Previous: Checking Implementation Robustness

Results

**Figure 1:** The Linux TCP implementation (version ) does not honor the RST flag in the SYN_RECV state unless the ACK bit is set. The bug was inadvertently introduced while fixing a ``harmless and rare'' case. The code prematurely returns when the ACK field is not set on an incoming packet.
$\begin{figure}\small { \begin{verbatim}// net/ipv4/tcp_minisocks.c // Process ... ...ST\vert TCP_FLAG_SYN)) goto embryonic_reset; ... }\end{verbatim}} \end{figure}$

The effectiveness of CMC can be measured using two metrics. One is the number of bugs CMC is able to find. The second measure is how well the given system is tested. This section describes our results of model checking the Linux TCP implementation using these two metrics.

Table 4: Coverage achieved during model refinement. The branching factor is a measure of the state space size.

		Line	Protocol	Branching	Additional
	Model Description	Coverage	Coverage	Factor	Bugs
1	Standard server and client	47.4 %	64.7 %	2.91	2
2	Model 1 + simultaneous connect	51.0 %	66.7 %	3.67	0
3	Model 2 + partial close	52.7 %	79.5 %	3.89	2
4	Model 3 + message corruption	50.6 %	84.3 %	7.01	0
	Combined Coverage	55.4 %	92.1 %

Subsections

Next: Bugs Found Up: Model Checking Large Network Previous: Checking Implementation Robustness

Madanlal Musuvathi 2004-03-03