Show simple item record

dc.contributor.authorMansour, Rihamen_US
dc.date.accessioned2014-03-14T20:08:23Z
dc.date.available2014-03-14T20:08:23Z
dc.date.issued2009-03-11en_US
dc.identifier.otheretd-03232009-182707en_US
dc.identifier.urihttp://hdl.handle.net/10919/26486
dc.description.abstractEngineering secure software remains a significant challenge for todayâ s software organizations as they struggle to understand the implications of security on their systems and develop systems that guarantee specified software security properties. The use of formal methods that are based on mathematical models has long been advocated in the development of secure systems, yet the promise of formal methods has not been realized. This is due to the additional discipline needed to formulate precisely the requirements and due complexities that often confront engineers. Further, the cost of development and the requisite learning curve of formal methods are quite high making them cost prohibitive to apply, especially for large software. The transition from requirements to design has been one of the most difficult steps in software development. Moreover, effective methods for deriving design from requirements that guarantee retention of the intended security properties remain largely unrealized on a repeatable and consistent basis. If security requirements are formalized and transformed into design using formal methods, the potential for security vulnerabilities would be diminished through better clarity, completeness, and consistency. Therefore, a requirements specification must be systematically transformable to a formal representation, and through effective formal methods the design can be derived such that the security properties are preserved and conveyed. This dissertation presents the FADES (Formal Analysis and Design for Engineering Security) approach that couples goal-oriented requirements specification with formal design specification to develop secure software in a constructive, provable and cost-effective way. To the best of our knowledge, FADES is the first security engineering approach that provides a systematic and automated bridge between semi-formal security requirements and formal design and implementation. FADES maintains the completeness and consistency of the security requirements specified with KAOS (Knowledge Acquisition for autOmated Specifications) when transformed to B formal specifications. Relaxing formality during requirements analysis enables security requirements to be better organized for producing more complete, consistent and clear requirements. The KAOS requirements model is then transformed to B, a popular formal representation used to derive and refine software systems. Security design specifications and implementation are produced using the B formal method which preserves the requisite security requirement properties. FADES treats security-specific elements in a systematic and constructive way while considering security early in the development lifecycle. Moreover, employing FADES provides better confidence for security evaluators in the evaluation of trusted software. A side effect of employing formal methods in development is the availability of sufficient traceability information at the various phases of development and maintenance allowing for more accurate impact analysis of security changes. FADES has been examined empirically both by security engineering experts and practitioners. Results obtained from the controlled experiments compare FADES to other formal methods, and show that FADES preserves security properties while maintaining better consistency, quality, and completeness. This is accomplished at a lower cost and with better results. These results have been evaluated by academic and industry experts working in the area of security and formal methods.en_US
dc.publisherVirginia Techen_US
dc.relation.haspartRihamMansour-ETD-FinalDefensDocument(new).pdfen_US
dc.relation.haspartapprovalLetter(experiment2).pdfen_US
dc.relation.haspartapprovalLetter(experiment1).pdfen_US
dc.rightsI hereby certify that, if appropriate, I have obtained and attached hereto a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to Virginia Tech or its agents the non-exclusive license to archive and make accessible, under the conditions specified below, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report.en_US
dc.subjectSecurity Engineeringen_US
dc.subjectFormal methodsen_US
dc.subjectSecurityen_US
dc.subjectFormal Analysis and Designen_US
dc.subjectGoal-Oriented Requirements Analysisen_US
dc.subjectSoftware Engineeringen_US
dc.titleFormal Analysis and Design for Engineering Securityen_US
dc.typeDissertationen_US
dc.contributor.departmentComputer Scienceen_US
dc.description.degreePh. D.en_US
thesis.degree.namePh. D.en_US
thesis.degree.leveldoctoralen_US
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen_US
thesis.degree.disciplineComputer Scienceen_US
dc.contributor.committeechairBohner, Shawn A.en_US
dc.contributor.committeememberMcCrickard, Donald Scotten_US
dc.contributor.committeememberEl-Kassas, Sherifen_US
dc.contributor.committeememberGracanin, Denisen_US
dc.contributor.committeememberEltoweissy, Mohamed Y.en_US
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-03232009-182707/en_US
dc.date.sdate2009-03-23en_US
dc.date.rdate2009-04-20
dc.date.adate2009-04-20en_US


Files in this item

Thumbnail
Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record