Tech Reports

ULCS-08-018

Formal Models of Reproduction: from Computer Viruses to Artificial Life (PhD Thesis)

Matthew Paul Webster


Abstract

In this thesis we describe novel approaches to the formal description of systems which reproduce, and show that the resulting models have explanatory power and practical applications, particularly in the domain of computer virology. We start by generating a formal description of computer viruses based on formal methods and notations developed for software engineering. We then prove that our model can be used to detect metamorphic computer viruses, which are designed specifically to avoid well-established signature-based detection methods. Next, we move away from the specific case of reproducing programs, and consider formal models of reproducing things in general. We show that we can develop formal models of the ecology of a reproducer, based on a formalisation of Gibsons theory of affordances. These models can be classified and refined formally, and we show how refinements allow us to relate models in interesting ways. We then prove that there are restrictions and rules concerning classification based on assistance and triviality, and explore the philosophical implications of our theoretical results. We then apply our formal affordance-based reproduction models to the detection of computer viruses, showing that the different classifications of a computer virus reproduction model correspond to differences between anti-virus behaviour monitoring software. Therefore, we end the main part of the thesis in the same mode in which we started, tackling the real-life problem of computer virus detection. In the conclusion we lay out the novel contributions of this thesis, and explore directions for future research."

[Full Paper]