SaTC: CORE: Small: Regulating and Leveraging Types for Security

Data elements are defined with types during software programming. A type not only specifies the semantics and characteristics of data elements, but also constrains the program operations and behaviors against data elements. Such type information is valuable for program analysis, and type analysis does not require complicated data-flow analysis. However, the type system in the widely used system programming languages (C/C++) has two fundamental problems. First, general types are prevalent; they obscure the specific data types and result in imprecise type-based analysis results. Second, type errors and typecasting are common; directly using erroneous types for defense mechanisms would lead to runtime errors which are considered unacceptable. This project aims to address the problems and use types for various security applications. The research results will be integrated into education to improve students' awareness of type errors, and help them capture type errors and harden their code. This project aims to address fundamental problems with types in type-unsafe programming languages like C/C++ and then use the improved types for various security applications. The project has three research thrusts. First, the project will regulate types—specifizing the prevalent general types and statically detecting type-confusion errors. It will employ selective, path-based, and function-grained typecasting analysis to improve scalability and precision. The second research thrust will then develop new techniques that leverage regulated types to significantly improve the precision of several foundational analysis techniques for security. With the regulated types and precise analysis techniques, the last research thrust will build effective and practical defense mechanisms such as type-based data-/control-flow integrity. The techniques will be implemented as LLVM passes, so that they can be easily used as compiler plugins. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.