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.
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.
Download the required software:
- ATASYN base and expand it.
- ATASYN engine
Install gnuplot and uppaal.
Run the script engine.sh and follow the instructions.
Lead developer: V Krishna Nandivada
Faculty advisor: Jens Palsberg
Comments and/or criticisms are welcome.