P-Code Extension

My undergraduate thesis was working on extending the symbolic execution framework Crucible with the ability to reason about assembly directly as opposed to the source code it normally ingests. This process involved Ghidra, the reverse engineering tool, to produce a standardized assembly before feeding into Crucible itself. The majority of the work was on inferring structure from the assembly that then must be fed to Crucible. This in turn lead to learning about Dependently Typed Haskell and other rabbit holes of complexity. The code can be found here. While the code is far from finished, the logic and framework is mostly complete. The full pdf explaining and documenting my thesis can be found here.