Formalizing Software Weaknesses Based On Z Specification

This thesis presents a study of the formalization of software weaknesses based on Z specifications.. Through deeply exploring the characteristics of software weaknesses, I develop a knowledge Database leveraging the concepts of Ontology engineering. With the increasing of the complexity of Software development, it is more and more important to understand the high-level impacts of weaknesses. Prototyping and describing weaknesses are two means of validation. However, neither gives full assurance that all possible situations have been checked and the system always works as expected. Furthermore, compared with increasing of design complexity, the percentage of weaknesses reported is rapidly increasing at a faster rate. It is reported that, the percentage of web-based attacks rose from 25% of the total number of entries in 2000 to 61% in 2006. And most of these security issues are caused by the design level flaws.Solving these problems needs concrete information to better understands its potential threats that help individual lay clear strategies for mitigations. Therefore, I use the CWE website as a guiding tool for such information as currently host a lot of security information and that importantly reduces cost. But notwithstanding this fact, the CWE website uses a natural language to describe weaknesses and therefore lacks adequate semantic information to be understood by a system or used by a program. I have used formal methods to describe these weaknesses and thus include: Using mathematical formulation to describe weaknesses, applying Z language to improve the formalization process and then building a Knowledge Database that will be used by programs and expert systems. My work will contribute to making programs and expert systems understand more about weaknesses. The effectiveness and the practical usefulness of the approach are exemplified by an illustrative Online banking scenario to detect weaknesses.