— Denial-of-service attacks are becoming more frequent and sophisticated. Researchers have proposed a variety of defenses, including better system configurations, infrastructures, protocols, firewalls, and monitoring tools. Can we validate a server implementation in a systematic manner? In this paper we focus on a particular attack, SYN flooding, where an attacker sends many TCP-connection requests to a victim’s machine. We study the issue of whether a TCP server can keep up with the packets from an attacker, or whether the server will exhaust its buffer space. We present a tool for statically validating a TCP server’s ability to survive SYN flooding attacks. Our tool automatically transforms a TCP-server implementation into a timed automaton, and it transforms an attacker model, given by the output of a packet generator, into another timed automaton. Together the two timed automata form a system for which the model checker UPPAAL can decide whether a bad state, in which the ...
V. Krishna Nandivada, Jens Palsberg