Binary-Level Type Inference using Datalog
Open Access
- Author:
- Huhman, Ashley Briane
- Graduate Program:
- Computer Science and Engineering
- Degree:
- Master of Science
- Document Type:
- Master Thesis
- Date of Defense:
- March 27, 2018
- Committee Members:
- Dr. Gang Tan, Thesis Advisor/Co-Advisor
Dr. Danfeng Zhang, Committee Member - Keywords:
- Datalog
Control Flow Graph construction
Type Inference analysis - Abstract:
- The Doop framework is evidence that the Datalog programming language can be used to implement entire non-trivial program analyses while maintaining high precision and scalability. This research focuses on an assembly level graphed-based type inference analysis in Datalog. Datalog provides a straightforward and easy to follow representation of the algorithm used in the analysis originally performed by D. Zeng and G. Tan in the functional programming language Objective Caml. The constraint solving algorithm performs propagation of types on a graph structure for registers and stack slots at the assembly level. The purpose of this algorithm is to help refine a control flow graph that models an entire C program. A more precise control flow graph leads to better predications of dynamic decisions within an application, thus creating a more secure environment. This research aims to allow for a more understandable implementation of the type inference analysis, in particular the constraint solving algorithm. Once the Datalog program has finished computing the results for this algorithm, given the correct input, one can simply query the current type set for any execution point within the C program. The simplicity in creating the logic for the algorithm compared to the implementation in Objective Caml is shown.