Ritsuya Ikeda, Kensuke Narita, and Shin-ya Nishizaki
DoS attacks, model checking, network simulator
Several studies have made formal analyses of denial-of-service (DoS) attacks to distributed systems. A primary factor in the attack is the imbalance between the victim server and the attackers. That is, the victim server incurs a heavy load compared to participants on the attacker side. The existing formal frameworks on DoS attacks mainly analyze and reason qualitative assertions on computational costs because generalized quantitative assertions are more difficult to formalize. The results of quantitative analysis, however, are easier to understand. Therefore, we propose a new cooperative approach to qualitative and quantitative analyses of DoS attacks. For qualitative analysis, we use Spice calculus to formulate the cost estimation in each process, which is a variation of Milner’s π-calculus. A system to be analyzed in Spice is translated into the modelling language process meta-language, to be analysed using a SPIN model checker. For quantitative analysis, the description in Spice is translated into a scenario script to be analyzed using the network simulator NS2. In the qualitative analysis, an assertion to be testified is described in linear temporal logic for SPIN model checker, whereas we can directly comprehend the result of the quantitative analysis.
Important Links:
Go Back
