|
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 project, 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
are based on the community developed Common Weakness Enumerations (CWE).
Gandhi, R.A., Siy, H., Yan, Wu,
"Lightweight formalisation of security weaknesses" Workshop on Formal
Methods in Software Engineering (FormaliSE): 25 May 2013, San Francisco
(USA), in conjunction with International Conference on Software Engineering.
2013. Preprint
Buffer overflow:
Constraints over a single
operation:
Alloy Specification for CWE
119
Alloy Specification for CWE
787
Alloy Specification
for CWE 121
Constraints over a series
of operations:
Alloy Specification for CWE
119
Alloy Specification for CWE
787
Alloy Specification
for CWE 121
Authentication
atttempts:
Constraints over a series
of operations:
Alloy Specification for CWE
799
Alloy Specification for CWE
307
OS command injection:
Constraints over a single
operation:
Alloy Specification for CWE
20
Alloy Specification for CWE
707
Alloy Specification for CWE
74
Alloy Specification for CWE
77
Alloy Specification for CWE 78
Alloy Analyzer download:
http://alloy.mit.edu/alloy/download.html
|
