# Weird Machines, Exploitability and Provable Unexploitability **Author**: Thomas Dullien (Halvar Flake) [[Computer Science]] [[Computer Security]] [[Software Exploits]] [[Reverse Engineering]] [IEEE Xplore Full-Text PDF:](http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8226852) ## Reading Notes The paper is about formalizing the concept of a [[Software Exploits]]. Lots of folk knowledge, no formal publishing. [[ZK - Eschewing formalization and publication leads to the creation of folk knowledge]] [[Weird Machine]]: - [[Complexity]] of program works for the attacker - Non-exploitability is the exception - Boundary where [[Complexity]] causes exploitability is low I'm personally learning about a lot of topics in the Related Work section: - [[Proof-Carrying Code]] - [[Lambda Calculus]] in the presence of faults (hardware faults) - Something called "stuttering bisimulation" (there is something called the "bisimulation" community), which I think refers to two automatons that simulate each other at different levels of abstraction (something the [[Model Checking]] community apparently studies).