A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
When you program in C, it is easy to make programming mistakes that directly compromise spatial memory safety, such as null pointer dereferences, type confusion, or buffer overflows. These direct memory corruption errors are a subclass of undefined behaviors in C, i.e., programming mistakes that you should not make, such as division by zero, signed integer overflow, or breaking the C strict aliasing rules. The compiler assumes that you do not make these mistakes, which are not checked, meaning that if you do make them, your program may crash, corrupt memory, or exhibit other unpredictable behaviors. Moreover, these mistakes can be exploited by an attacker to take control of your program, and this represents both the most common and the most severe kind of security vulnerabilities.
Thus, it is important to ensure that your program is free from these undefined behaviors. Providing tools that do this practically is one of the main purposes behind the development of Codex, a sound static analyzer based on abstract interpretation. The paper focuses on particular method that can ensure spatial memory safety of C or binary programs almost automatically, requiring only a small amount of type annotations.
