Formalizing self-propagating behaviour
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.