Idle Port Scanning and Non-interference Analysis of Network Protocol Stacks Using Model Checking

Roya Ensafi, Jong Chun Park, Deepak Kapur, Jedidiah R. Crandall

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Scopus citations


Idle port scanning uses side-channel attacks to bounce scans off of a "zombie" host to stealthily scan a victim IP address or infer IP-based trust relationships between the zombie and victim. 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. Two new methods of idle scans resulted from our modeling effort, based on TCP RST rate limiting and SYN caches, respectively. Through experimental verification of these attacks, we show that it is possible to scan victims which the attacker is not able to route packets to, meaning that protected networks or ports closed by firewall rules can be scanned. This is not possible with the one currently known method of idle scan in the literature that is based on non-random IPIDs. For the future design of network protocols, a notion of trusted vs. untrusted networks and hosts (based on existing IP-based trust relationships) will enable shared, limited resources to be divided. For a model complex enough to capture the details of each attack and where a distinction between trusted and untrusted hosts can be made, we modeled RST rate limitations and a split SYN cache structure. Non-interference for these two resources was verified with symbolic model checking and bounded model checking to depth 1000, respectively. Because each transition is roughly a packet, this demonstrates that the two respective idle scans are ameliorated by separating these resources.

Original languageEnglish (US)
Title of host publicationProceedings of the 19th USENIX Security Symposium
PublisherUSENIX Association
Number of pages16
ISBN (Electronic)9781931971775
StatePublished - 2010
Externally publishedYes
Event19th USENIX Security Symposium - Washington, United States
Duration: Aug 11 2010Aug 13 2010

Publication series

NameProceedings of the 19th USENIX Security Symposium


Conference19th USENIX Security Symposium
Country/TerritoryUnited States

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Information Systems
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Idle Port Scanning and Non-interference Analysis of Network Protocol Stacks Using Model Checking'. Together they form a unique fingerprint.

Cite this