Schadenfreude is a pet project that I've been working on for quite some time now. While starting out as a personal project, it has evolved into a project which I develop in my higher-level courses at TAMU.

Iteration one of Schadenfreude has two components:

Unfortunately, it is quite limited -- there's no form of symbolic execution or automated way to apply operations to derive values (symbolic or concrete).

Iteration two, "Schadenfreude: Resurrection", attempts to approach the failures of iteration one by applying a theorem prover to PCode operations to convert functions into theorems by combining control flow and data flow graphs into a single "mixed flow" graph. Using this, one can effectively "ask" the theorem prover to prove that a specific property is true, or if not, why it is not. This is the iteration described in a majority of this section.

Similar to iteration one, iteration two has major failures:

Here's the initial paper submitted regarding the theory and implementation of this iteration, though I warn you: it is quite cringe and may have incorrect information as I have had no formal education in program verification.

Iteration three, which is neither named nor yet exists, will attempt to resolve some failures of iteration two. Primarily:

Some theory for iteration three will be discussed, but will be marked explicitly as part of iteration three, where applicable.

Finally, iteration four will take on more implementation-specific components: syscalls and vulnerability classification. With vulnerabilities classified, the SMT solver should be able to detect vulnerabilities and generate payloads to exploit them automatically. A majority of the work of this iteration will lie in correctly representing syscall behaviour and defining vulnerabilities in the context of a binary. Without knowing how iteration three will be implemented, iteration four's implementation would be pure speculation. I'll define the "how" part later.