TY - CONF JO - Enabling Technologies: Infrastructure for Collaborative Enterprises, 2006. WETICE '06. 15th IEEE International Workshops on TI - Security Verification Techniques Applied to PatchLink COTS Software T2 - Enabling Technologies: Infrastructure for Collaborative Enterprises, 2006. WETICE '06. 15th IEEE International Workshops on IS - SN - 1524-4547 VO - SP - 319 EP - 325 AU - David P. Gilliam AU - John D. Powell AU - Matt Bishop AU - Chris Andrew AU - Sameer Jog Y1 - June 2006 PY - 2006 KW - Unix KW - formal specification KW - program verification KW - security of data KW - software packages KW - Jet Propulsion Laboratory KW - PatchLink COTS software KW - UNIX agent KW - University of California KW - commercial-off-the-shelf software product KW - flexible modeling framework KW - formal specification KW - model-based verification instrument KW - property-based tester KW - security verification techniques KW - software artifacts VL - JA - Enabling Technologies: Infrastructure for Collaborative Enterprises, 2006. WETICE '06. 15th IEEE International Workshops on DOI - 10.1109/WETICE.2006.59 AB - Verification of the security of software artifacts is a challenging task. An integrated approach that combines verification techniques can increase the confidence in the security of software artifacts. Such an approach has been developed by the Jet Propulsion Laboratory (JPL) and the University of California at Davis (UC Davis). Two security verification instruments were developed and then piloted on PatchLink's UNIX agent, a commercial-off-the-shelf (COTS) software product, to assess the value of the instruments and the approach. The two instruments are the flexible modeling framework (FMF) - a model-based verification instrument (JPL), and a property-based tester (UC Davis). Security properties were formally specified for the COTS artifact and then verified using these instruments. The results were then reviewed to determine the effectiveness of the approach and the security of the COTS product ER -