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 tool 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 ATASYN 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 buffer overruns, can be reached. Our tool has two advantages over simply testing the server implementation with a packet generator. First, our tool is an order of magnitude faster because of aggressive abstraction of the server code. Second, our tool can be applied to a variety of server software without having to install each one in the kernel of an operating system. Thus, a programmer of defensive measures against SYN flooding attacks can get rapid feedback during development.

Getting the tool ATASYN to work is a 3 phase work.

  1. Download the required software:
    1. ATASYN base and expand it.
    2. UPPAAL ,
    3. gnuplot
    4. ATASYN engine
  2. Install gnuplot and uppaal.
  3. Run the script and follow the instructions.
Voila! You can now run ATASYN to test your TCP stack for a pentium machine. If you have get any errors while running it then follow the error and go back to the step 1/2/3 whichever is appropriate. Currently ATASYN is supported for linux running on pentium architecture only. ATASYN uses D-ITG to generate packets sequences.

Lead developer: V Krishna Nandivada
Faculty advisor: Jens Palsberg


Comments and/or criticisms are welcome.