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.

@TechReport{briesemeister+:2005,
    author = {Linda Briesemeister and Phillip A. Porras and Ashish Tiwari},
    title = {Model Checking of Worm Quarantine and Counter-Quarantine under a Group Defense},
    institution = {SRI International, Computer Science Laboratory},
    year = {2005},
    number = {SRI-CSL-05-03},
    month = {October},
    URL = {http://www.csl.sri.com/papers/sri-csl-2005-03/}
}

• SRI-CSL-2005-03.pdf