A novel flow-sensitive type and effect analysis for securing C code

In this paper, we present a novel type and effect analysis for detecting type cast errors and memory errors in C source code. Our approach involves a type system with effect, region, and cast history annotations that hold valuable information for ensuring memory safety. The cast history is a precise type decoration we define to address C type casting issues. Our flow-sensitive annotations are allowed to change from one program point to another in order to efficiently tackle temporal errors. We also define a recursive algorithm based on alias information to deal with C aliasing pitfalls and to improve the precision of our analysis. We endow our type system with static security checks that use our annotations to verify and enforce security properties. The effects generated during the type analysis provide an interface that outputs undecidable Dunno points that need runtime information for safety checking. This interface can be used to communicate with dynamic analysis approaches in order to overcome static analysis limitations.