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
Bibtex
| @inproceedings{BG-asian07, | ||
| address = | {Doha, Qatar}, | |
| author = | {Bursztein, Elie and Goubault{-}Larrecq, Jean}, | |
| booktitle = | {{P}roceedings of the 12th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'07)}, | |
| DOI = | {10.1007/978-3-540-76929-3_20}, | |
| editor = | {Cervesato, Iliano}, | |
| month = | dec, | |
| pages = | {212-227}, | |
| publisher = | {Springer}, | |
| series = | {Lecture Notes in Computer Science}, | |
| title = | {A Logical Framework for Evaluating Network Resilience Against Faults and Attacks}, | |
| url = | {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf}, | |
| volume = | {4846}, | |
| y | ||
