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, since 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 modeling language Promela to be analyzed 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 temporal logic LTL for SPIN model checker, whereas we can directly comprehend the result of the quantitative analysis.
各種検索
サポート
ヘルプ