NetQi

Paper accepted at the 4th International Conferences on Information Security and Cryptology (INSCRYPT 2008). Beijing China.

Abstract

The anticipation game framework is an extension of attack graphs based on game theory. It is used to anticipate and analyze intruder and administrator concurrent interactions with the network.

As attack graph based on model checking, the goal on an anticipation game is to prove that a safety property hold. However using this kind of goal is tedious and error prone on large networks because it assume that the analyst have a prior and complete knowledge of the network critical services.

In this paper we address this issue by introducing a new kind of goal called strategy objectives which is more usable for network security analysis purpose.

To do so we have extended the anticipation games framework with cost and reward. Additionally this extension allows to take into account the financial dimension of attack during the analysis.

We prove that finding the optimal strategy is decidable and only requires a linear memory space. Finally we show that anticipation game with strategy can be used in practice even on large networks by evaluating the performance of our prototype.

file

Using Strategy Objectives for Network Security Analysis (PDF preliminary version)

Bibtex

The paper has been accepted to  the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA’08). Held at Seoul, Korea in October 2008

Abstract

NetQi is a freely available model-checker designed to analyze network incidents such as intrusion. This tool is an implementation of the anticipation game framework, a variant of timed game tailored for network analysis. The main purpose of NetQi is to find, given a network initial state and a set of rules, the best strategy that fulfills player objectives by model-checking the anticipation game and comparing the outcome of each play that fulfills strategy constraints. For instance, it can be used to find the best patching strategy. NetQi has been successfully used to analyze service failure due to hardware, network intrusion, worms and multiple-site intrusion defense cooperation.

Bibtex

Paper accepted at FAST’08, Malaga, Spain,

Abstract

Over the last few years, attack graphs have became a well recognized tool to analyze and model complex network attack. The most advanced evolution of attack graphs, called anticipation games, is based on game theory. However even if anticipation games allow to model time, collateral effects and player interactions with the network, there is still key aspects of the network security that cannot be modeled in this framework. Theses aspects are network cooperation to fight unknown attack, the cost of attack based on its duration and the introduction of new attack over the time. In this paper we address these needs, by introducing a three-fold extension to anticipation games. We prove that this extension does not change the complexity of the framework. We illustrate the usefulness of this extension by presenting how it can be used to find a defense strategy against 0 days that use an honey net. Finally, we have implemented this extension into a prototype, to show that it can be used to analyze large networks security.

File

The paper in PDF

BibTex

Accepted paper at ASIAN 2007 at Carnegie Mellon University in Qatar.

Abstract

We present a logic-based framework to evaluate the resilience of computer networks in the face of incidents, i.e., attacks from malicious intruders as well as random faults. Our model uses a two-layered presentation of dependencies between files and services, and of timed games to represent not just incidents, but also the dynamic responses from administrators and their respective delays. We demonstrate that a variant TATL$\Diamond$ of timed alternating-time temporal logic is a convenient language to express several desirable properties of networks, including several forms of survivability. We illustrate this on a simple redundant Web service architecture, and show that checking such timed games against the so-called TATL$\Diamond$ variant of the timed alternating time temporal logic TATL is EXPTIME-complete.

Files

Paper Author version (pdf)

Bibtex