Threat modeling using formal methods: A new approach to develop secure web applications

Software security problems exist since the early days of computer systems. Operating system level approaches, network level approaches and machine level approaches are not sufficient for the security of software systems. Software security has gained attention in the recent years as an internal security issue of software systems as compared to external protective measures. Threat modeling is a technique being used to model threats into software systems. By applying threat modeling at the early stages of software development life cycle, all possible threats to software systems can be identified and mitigated and hence in this way, a more secure software application can be developed. Various threat modeling approaches such as CLASP, SDL, STRIDE, DREAD, TAM and Touch Points are being used by many organizations for threat modeling into software systems. But all of the approaches being used for threat modeling are based on informal and semi formal techniques. Formal methods are based on mathematics and provide state of the art techniques for secure software development. Formal methods had been used successfully in many critical systems such as CICS, Paris Railway System and British Air Traffic Control System etc. In the proposed approach VDM++, will be used for specification of core components: STRIDE, DREAD and Security Mechanisms. VDM++Tools will be used for type checking and proof obligations.