Many existing methods of forensic malware analysis rely on the investigators’ practical experience rather than hard science. This paper presents a formal (i.e. based on mathematics) approach to reconstructing activities of a malicious executable found in a victim’s system during a post-mortem analysis. The behavior of the suspect executable is modeled as a finite state automaton where each state represents behavior that results in an observable modification to the victim’s system. The derived model of the malicious code allows for accurate reasoning and deduction of the occurrence of malicious activities even when anti-forensic methods are employed to disrupt the investigation process.