Logic For Exploit Detection: Utilizing Proof Search for Exploitability Detection in Compact Software Systems

Eskandari Miandoab, Kaveh

Etd

Logic For Exploit Detection: Utilizing Proof Search for Exploitability Detection in Compact Software Systems

Public Deposited

Compact, yet complex systems and software are widely utilized, both on administrative, organizational, and personal levels, for the processing of large amounts of data. These software make imperative decisions and are used as a main tool in everyday workings such as voting software and automatic moderation systems. However, these systems inherently carry the danger of being exploitable either due to their design or owing to the data that they are based on, which can adversely affect the individuals impacted by their usage. In this work, we aim to identify and mitigate this behavior in compact software systems by catching possible exploitability bugs prior to the implementation of the system. Our workflow consists of two main steps, we first model the system as the steps the program takes to reach a conclusion using linear logic programming, and then apply proof search for the early identification of design exploits in the system. We wish to provide a complete and sound framework for the detection of exploits in a software's design, and we believe that our framework can reduce the required workload for the removal of these design mistakes in later stages of development. Our main focus in this project is the detection of exploits that can be generated by following set a number of steps in accordance with the program logic, thus we refrain from focusing on security exploits, and those with external intervention, such as code injection. More concretely, our framework is best used to catch bugs that arise due to the program logic. Additionally, the proposed framework can be used for education to showcase how a bug propagates through a given software, and how a small change in a program can lead to vastly different results.

Creator