Idle port scanning and non-interference analysis of network protocol stacks using model checking
Roya Ensafi, Jong-Chun Park, Deepak Kapur, Jedidiah R. Crandall · 2010
Idle port scanning uses side-channel attacks to bounce scans off of a “zombie” host to stealthily scan a victim IP address and determine if a port is open or closed, or infer IP-based trust relationships between the zombie and victim. In this paper, we present results from building a transition system model of a network protocol stack for an attacker, victim, and zombie, and testing this model for non-interference properties using model checking. We present two new methods of idle scans in this paper that resulted from our modeling effort, both of which have been verified through implementation. One is based on TCP RST rate limiting and the other on SYN caches. The latter does not require the attacker to send any packets to the victim on the port to be scanned, not even forged packets. This gives the attacker additional capabilities beyond known idle scan techniques, such as the ability to scan ports that are blocked by a firewall or locate hosts on trusted networks, to which the attacker is not able to route packets, and infer their operating system. This is in contrast to the one currently known method of idle scan in the literature, which is based on non-random IPIDs. For the future design of network protocols, we suggest that a notion of trusted vs. untrusted networks and hosts be made explicit in the protocol stack all the way down to the IP layer. This will enable shared, limited resources to be divided in a way that achieves non-interference and makes idle scans impossible. Using symbolic model checking, we verify that separate RST rate limitations for trusted vs. untrusted hosts achieves non-interference (without the SYN cache). Using bounded model checking we model a split SYN cache structure with separate buffers for trusted and untrusted hosts and prove non-interference to a depth of 1000 transitions. Because each transition is roughly a packet, this means that idle scans are eliminated by the split SYN cache for all practical purposes.