AIR Integer Model
Integer overflow and wraparound are a growing and underestimated source of vulnerabilities in C and C++ programs. This continues to be an active area of research by the CERT Division's Secure Coding team.
The As-If Infinitely Ranged (AIR) Integer Model is a largely automated mechanism for eliminating integer overflow and integer truncation, and the version available here for public download was completed by the CERT Division in January of 2010 . The AIR integer model either produces a value equivalent to one that would have been obtained using infinitely ranged integers or reports a runtime constraint violation. Unlike previous integer models, AIR integers do not require precise traps and consequently do not break or inhibit most existing optimizations. Instrumented Fuzz Testing Using AIR Integers (of libraries compiled using a prototype AIR integer compiler) has been effective in discovering vulnerabilities in software, with low false positive and false negative rates.