Model checking of worm quarantine and counter-quarantine under a group defense

This is a lengthy, formal paper, but quite intriguing. So far I think the research is sound and the methodology proposed is interesting, but I don't know how well it would work in the real world. But perhaps within an enterprise ... Nonetheless, if you're feeling like reading a strong academic paper, here is one for you.

We consider what it means to perform worm quarantine across a network with an emerging self-propagating worm outbreak. It is generally understood that an effective quarantine defense can under certain conditions reduce the infection growth rate, and ideally can prevent a worm from reaching its full saturation potential. This report attempts to more precisely define the desired properties of a quarantine algorithm, and suggest different forms of quarantine properties that vary in their ability to isolate infected nodes, ensure the existence of an uninfected population, and guarantee some persistent protection, no matter how the worm behaves. We employ the SAL formal modeling language and model checker to investigate these properties on a specific group-based quarantine algorithm. In addition to answering questions regarding algorithm correctness and validating some quarantine properties, the model checker disproves other quarantine properties. The proofs and counter-examples produced during this process help in algorithm design and may be useful in informing simulation experiments or building test cases. Using a game theoretic approach, counter-examples of a win scenario for the defense yield insight into smart worm behavior that defeats a known quarantine defense.

Source: Model Checking of Worm Quarantine and Counter-Quarantine under a Group Defense,  by Linda Briesemeister, Phillip A. Porras and Ashish Tiwari.  Publication number SRI-CSL-2005-03. Computer Science Laboratory, SRI International, Menlo Park, CA. October, 2005.