# Formalizing self-propagating behaviour

Since reading Ken Thompson's Reflections on Trusting Trust I am trying to formalize the idea of a program which mutates its own behaviour; specifically, a program that would be self-reproducing except that it would reproduce itself with a mutation. With this definition I wish to differentiate this kind of program from self-reproducing programs and will call them programs with self-propagating behaviour (due to the nature of propagating its own mutations). I am familiar with Hoare Logic, LTL, CTL, and CTL*, but am unsure what to use for the formulation since Hoare Logic requires a concrete implementation of a program and I am trying to represent not a program but a kind of program, and am also unsure if/how I could express this idea in LTL, CTL, or CTL*.

• Maybe look at: Simon Kramer, Julian C. Bradfield: A general definition of malware. Journal in Computer Virology 6(2): 105-114 (2010) – Dave Clarke May 14 '15 at 8:57

I don't have time for an elaborate answer right now, so here is just a quick braindump: Program logic does not restrict to concrete programs. Given e.g. a pair $(A, B)$ of pre/post-conditions, you can think of this pair as defining a set of programs

$$\{ P \ |\ P\ \text{is a programs such that}\ \models A[P]B \}$$

Here are a couple other references that might be useful.

• J. Von Neumann, Theory of Self-Reproducing Automata.
• F. Cohen, Computer Viruses - Theory and Experiments.
• S. Kramer, J. C. Bradfield, A general definition of malware.
• G. A. Kavvos, Theories of Computer Viruses: 30 Years Later.
• L. M. Adleman, An abstract theory of computer viruses.
• G. Jacob, E. Filiol, H. Debar, Formalization of viruses and malware through process algebras.
• J. L. England, Statistical physics of self-replication.

As the kind of program you envision is a form of meta-programming, I suggest also to look at this field (which is primarily implementation-driven and lacks substantial theory as of 2017). Here are some references, none of which is likely to be directly relevant, but will eventually lead to research that should be:

• M. Berger, L. Tratt, Program Logics for Homogeneous Meta-Programming
• S. N. Artemov, L. D. Beklemishev, Provability Logic.
• G. Japaridze, D. de Jongh, The logic of provability.
• S. Artemov, Explicit Provability And Constructive Semantics.
• J. Alt, S. Artemov, Reflective λ-Calculus.

My (rather tentative) answer would be that the program "changing its meaning" (being a compiler, and having been written in the language that it translates) is something that has to do no just with syntax and semantics, but with what we call pragmatics. The program has to be actually considered a compiler (by its users), i.e., at the pragmatic level.

It is an amazing thing indeed, that these pieces of software can make us dance around them, and that is possibly the reason why Ken Thompson was so impressed by what he found.

As you might expect, formal pragmatics is a discipline that has yet to be domesticated, and I am not personally familiar with the research on the subject. All I can give you is this pointer, for your own further investigation.

Perhaps the final word in self-mutation are Jugen Schmidthiber's Goedel Machines, which perform provably optimal self-modification.