Formal Analysis and Design for Engineering Security

Simple item page
dc.contributor.authorMansour, Rihamen
dc.contributor.committeechairBohner, Shawn A.en
dc.contributor.committeememberMcCrickard, D. Scotten
dc.contributor.committeememberEl-Kassas, Sherifen
dc.contributor.committeememberGracanin, Denisen
dc.contributor.committeememberEltoweissy, Mohamed Y.en
dc.contributor.departmentComputer Scienceen
dc.date.accessioned2014-03-14T20:08:23Zen
dc.date.adate2009-04-20en
dc.date.available2014-03-14T20:08:23Zen
dc.date.issued2009-03-11en
dc.date.rdate2009-04-20en
dc.date.sdate2009-03-23en
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
dc.description.degreePh. D.en
dc.identifier.otheretd-03232009-182707en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-03232009-182707/en
dc.identifier.urihttp://hdl.handle.net/10919/26486en
dc.publisherVirginia Techen
dc.relation.haspartRihamMansour-ETD-FinalDefensDocument(new).pdfen
dc.relation.haspartapprovalLetter(experiment2).pdfen
dc.relation.haspartapprovalLetter(experiment1).pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectSecurity Engineeringen
dc.subjectFormal methodsen
dc.subjectSecurityen
dc.subjectFormal Analysis and Designen
dc.subjectGoal-Oriented Requirements Analysisen
dc.subjectSoftware Engineeringen
dc.titleFormal Analysis and Design for Engineering Securityen
dc.typeDissertationen
thesis.degree.disciplineComputer Scienceen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.leveldoctoralen
thesis.degree.namePh. D.en

Files

Original bundle
Now showing 1 - 3 of 3
Thumbnail Image
Name:
RihamMansour-ETD-FinalDefensDocument(new).pdf
Size:
3.85 MB
Format:
Adobe Portable Document Format
Download
Thumbnail Image
Name:
approvalLetter(experiment2).pdf
Size:
212.46 KB
Format:
Adobe Portable Document Format
Download
Thumbnail Image
Name:
approvalLetter(experiment1).pdf
Size:
247.67 KB
Format:
Adobe Portable Document Format
Download

Collections

Doctoral Dissertations