COOPERATION OF MODEL CHECKING AND NETWORK SIMULATION FOR COST ANALYSES OF DISTRIBUTED SYSTEMS
Ritsuya Ikeda, Kensuke Narita, Shin-ya Nishizaki · International Journal of Computers and Applications · 2011
AbstractSeveral 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 i...