An arms-race exists between malware authors and system defenders in which defenders develop new detection approaches only to have the malware authors develop new techniques to bypass them. This motivates the need for a formal framework to jointly reason about malware and its detection. This dissertation presents such a formal framework termed the extended Maurer model} (EMM) and then applies this framework to develop a game-theoretic model of the malware authors versus system defenders confrontation. To be inclusive of modern computers and networks, the EMM has been developed by extending to the existing Maurer computer model, a Turing-reducible model of computer operations. The basic components of the Maurer model have been extended to incorporate the necessary structures to enable the modeling of programs, concurrency, multiple processors, and networks. In particular, we show that the proposed EMM remains a Turing equivalent model which is able to model modern computers, computer networks, as well as complex programs such as modern virtual machines and web browsers. Through the proposed EMM, we provide formalizations for the violations of the standard security policies. Specifically, we provide the definitions of the violations of confidentiality policies, integrity policies, availability policies, and resource usage policies. Additionally, we also propose formal definitions of a number of common malware classes, including viruses, Trojan horses, spyware, bots, and computer worms. We also show that the proposed EMM is complete in terms of its ability to model all implementable that could exist malware within the context of a given defended environment. We then use the EMM to evaluate and analyze the resilience of a number of common malware detection approaches. We show that static anti-malware signature scanners can be easily evaded by obfuscation, which is consistent with the results of prior experimental work. Additionally, we also use the EMM to formally show that malware authors can avoid detection by dynamic system call sequence detection approaches, which also agrees with recent experimental work. A measure-theoretic model of the EMM is then developed by which the completeness of the EMM with respect to its ability to model all implementable malware detection approaches is shown. Finally, using the developed EMM, we provide a game-theoretic model of the confrontation of malware authors and system defenders. Using this game model, under game theory's strict dominance solution concept, we show that rational attackers are always required to develop malware that is able to evade the deployed malware detection solutions. Moreover, we show that the attacker and defender adaptations can be modeled as a sequence of iterative games. Hence, the question can be asked as to the conditions required if such a sequence (or arms-race) is to converge towards a defender advantageous end-game. It is shown via the EMM that, in the general context, this desired situation requires that the next attacker adaptation exists as, at least, a computationally hard problem. If this is not the case, then we show via the EMM's measure theory perspective, that the defender is left needing to track statistically non-stationary attack behaviors. Hence, by standard information theory constructs, past attack histories can be shown to be uninformative with respect to the development of the next to be required adaptation of the deployed defenses. To our knowledge, this is the first work to: (i) provide a joint model of malware and its detection, (ii) provide a model that is complete with respect to all implementable malware and detection approaches, (iii) provide a formal bridge between Turing-reducibility and measure theory, and (iv) thereby, allow game theory's strict dominance solution concept to be applied to formally reason about the requirements if the malware versus anti-malware arms-race is to converge to a defender advantageous end-game. / Graduate / melgamal@uvic.ca