Lightweight formal models of software weaknesses

Many vulnerabilities in today´s software products are rehashes of past vulnerabilities. Such rehashes could be a result of software complexity that masks inadvertent loopholes in design and implementation, developer ignorance/disregard for security issues, or use of software in contexts not anticipated for the original specification. While weaknesses and exposures in code are vendor, language, or environment specific, to understand them we need better descriptions that identify their precise characteristics in an unambiguous representation. In this paper, we present a methodology to develop precise and accurate descriptions of common software weaknesses through lightweight formal modeling using Alloy. Natural language descriptions of software weaknesses used for formalization are based on the community developed Common Weakness Enumerations (CWE).