Application of lightweight formal methods to software security

Formal specification and verification of security has proven a challenging task. There is no single method that has proven feasible. Instead, an integrated approach which combines several formal techniques can increase the confidence in the verification of software security properties. Such an approach which specifies security properties in a library that can be re-used by 2 instruments and their methodologies developed for the National Aeronautics and Space Administration (NASA) at the Jet Propulsion Laboratory (JPL) are described herein The flexible modeling framework (FMF) is a model based verification instrument that uses Promela and the SPIN model checker. The property based tester (PET) uses TASPEC and a test execution monitor (TEM). They are used to reduce vulnerabilities and unwanted exposures in software during the development and maintenance life cycles. These instruments are currently being piloted with a COTS server-agent application.