Utilizing type systems for static vulnerability analysis

Abstract

Programming languages use type systems to reduce number of bugs. Type systems of most languages are not powerful enough to express basic exception safety. Extension of type system in a way that allows representing exception guaranties can provide valuable information to analysis tools. Such tools could even be implemented in type system. We describe a way to extend type system of a given language allowing security invariants to be expressed and vulnerable code to be located.

Keywords

• static code analysis
• type systems
• vulnerability analysis
• dependent types
• memory safety
• pointer aliasing