JPL Technical Report Server

Using software security analysis to verify the secure socket layer (SSL) protocol

Show simple item record

dc.contributor.author Powell, John D.
dc.date.accessioned 2006-01-27T18:36:36Z
dc.date.available 2006-01-27T18:36:36Z
dc.date.issued 2004-06-14
dc.identifier.citation 13th IEEE International Workshops Enabling Technologies : Infrastructures for Collaborative Enterprises, Modena, Italy, June 14-16, 2004. en
dc.identifier.clearanceno 13th IEEE International Workshops Enabling Technologies : Infrastructures for Collaborative Enterprises, Modena, Italy, June 14-16, 2004.
dc.identifier.uri http://hdl.handle.net/2014/38396
dc.description.abstract The National Aeronautics and Space Administration (NASA) have tens of thousands of networked computer systems and applications. Software Security vulnerabilities present risks such as lost or corrupted data, information the3, and unavailability of critical systems. These risks represent potentially enormous costs to NASA. The NASA Code Q research initiative “Reducing Software Security Risk (RSSR) Trough an Integrated Approach ’’ offers, among its capabilities, formal verification of software security properties, through the use of model based verification (MBV) to address software security risks. [1,2,3,4,5,6] MBV is a formal approach to software assurance that combines analysis of software, via abstract models, with technology, such as model checkers, that provide automation of the mechanical portions of the analysis process. This paper will discuss: The need for formal analysis to assure software systems with respect to software and why testing alone cannot provide it. The means by which MBV with a Flexible Modeling Framework (FMF) accomplishes the necessary analysis task. An example of FMF style MBV in the verification of properties over the Secure Socket Layer (SSL) communication protocol as a demonstration. en
dc.description.sponsorship NASA/JP: en
dc.format.extent 871423 bytes
dc.format.mimetype application/pdf
dc.language.iso en_US en
dc.publisher Pasadena, CA : Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2004 en
dc.subject security en
dc.subject software en
dc.subject formal methods en
dc.subject model checking en
dc.title Using software security analysis to verify the secure socket layer (SSL) protocol en
dc.type Preprint en


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search


Browse

My Account