ATASYN

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.

Download the required software:
1. ATASYN base and expand it.
2. UPPAAL ,
3. gnuplot
4. ATASYN engine
Install gnuplot and uppaal.
Run the script engine.sh 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.

Credits:
Lead developer: V Krishna Nandivada
Faculty advisor: Jens Palsberg

Publications:

Timing analysis of TCP servers for surviving denial-of-service attacks, by V. Krishna Nandivada and Jens Palsberg. In Proceedings of RTAS'05, 11th IEEE Real-Time and Embedded Technology and Applications Symposium, San Francisco, March 2005. To appear.

Comments and/or criticisms are welcome.