# Presentation: 660117

## SAS ‘04

- Reducing Software Security Risk through an Integrated Approach
- David P. Gilliam and John D. Powell
- Jet Propulsion Laboratory,
- California Institute of Technology

## Acknowledgement

**NOTE:  **
**This research was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration**
**The work was sponsored by the NASA Office of Safety and Mission Assurance under the Software Assurance Research Program lead by the NASA Software IV&V Facility**
**This activity is managed locally at JPL through the Assurance and Technology Program Office**

## Current Collaborators

- David Gilliam – Principle Investigator, JPL
- John Powell – JPL Software Engineer
- Matt Bishop – Associate Professor of Computer Science, University of California at Davis
- http://rssr.jpl.nasa.gov

## Goal

- Reduce security risk to the computing environment by mitigating vulnerabilities in the software development and maintenance life cycles
- Provide an instrument and tools to help avoid vulnerabilities and exposures in software
- To aid in complying with security requirements and best practices

## Problem

- Lack of Experts: Brooks – “No Silver Bullet” is still valid (IEEE Software Engineering, 1987)
- Poor Security Requirements
- Poor System Engineering
- Leads to poor design, coding, and testing
- Cycle of Penetrate and Patch
- Piecemeal Approach to Security Assurance

## Reducing Software Security Risk Through an Integrated Approach

**Reducing Software Security Risk ****Through an Integrated Approach**

**Software Vulnerabilities Expose IT Systems and Infrastructure to Security Risks**
**Goal:   Reduce Security Risk in Software and****	**** ****	****Protect IT Systems, Data, and Infrastructure**
- Security Training for System Engineers and Developers
- Software Security Checklist for end-to-end life cycle
- Software Security Assessment Instrument (SSAI)

**Security Instrument Includes:**
- Model-Based Verification
- Property-Based Testing
- Security Checklist
- Vulnerability Matrix
- Collection of security tools

**NASA**

## Womb-to-Tomb Process

- Coincides with Organizational Polices and Requirements
- Security Risk Mitigation Process in the Software Lifecycle
- Software Lifecycle Integration
- Training
- Software Security Checklist
- Phase 1
- Provide instrument to integrate security as a formal approach to the software life cycle
- Requirements Driven
- Phase 2:
- External Release of Software
- Release Process
- Vulnerability Matrix – NASA Top 20
- Security Assurance Instruments
- Early Development – Model Checking / FMF
- Implementation  – Property Based Testing
- Security Assessment Tools (SATs)
- Description of available SATs
- Pros and Cons of each and related tools with web sites
- Notification Process when Software or Systems are De-Commissioned / Retired

## Model Checking & The Flexible Modeling Framework

**MC of FMF combinations allows partial answers to otherwise intractable system state spaces**
**MC with FMF Benefits Software in Early Lifecycle**
- Earlier Discovery of Software Errors
- Correction is easier / less expensive
- Modeling in FMF components compatible with the software development process
- Modular model design allows easy extension of existing models
- Multiple client scenarios for the server login example were quickly modeled and verified
- The various client scenarios allows extensive off-nominal verification with ease
- Rapidly changing requirements and designs
- Multiple design trade offs in login protocol were easily explored

## Model Checking: Flexible Modeling Framework (Cont.)

**Collection of Model Components **

**Model Checker **

**Component Combiner **

- Each Individual Component

- Unique Component Combinations

**If Combination State Space is too Large**

- No

- Yes

**MCCT**

**Implicit**

**Explicit**

**Heuristic Propagation of Results **

**Updated Component ******

**Combinations Containing ******

## Model Checking & The Flexible Modeling Framework – Server Login Model

- Varying levels of detail were defined for different system parts
- Multiple login failure propagation scenarios
- known but not formally defined for different systems using the login protocol
- Model extensions are readily possible for many if not all of these scenarios
**Developed quickly **
**Adapted at will**
**Cross tested against **
**Client scenarios**
**Protocol design trades**

## Server Login Model

- chan login = [0] of {short};
- chan accessed = [0] of {bit};
- short user_name = 0;
- short password = 0;
- bit accsd = 0;
- bit hash_complete = 0;
- proctype server(){
- do
**   ****::user_name == 0 && password == 0 -> login?user_name;**
**   ****::****user_name != 0 && password == 0 ->login?password;**
**   ****::user_name != 0 && password != 0 ->**
- 	do
- 	    ::user_name != password ->
- 	        if
- 	          **:: hash_complete == 0->**
**	****	****password = password * -1;**
**	****	****hash_complete = 1;**
- 	          **::hash_complete == 1->accessed!0; break;**
- 	        fi
- 	    **::user_name == password ->accessed!1; break;**
- 	od
- od }

**Obtain User Name**
**Obtain User Password**
**After User Name and Password Obtained**
**Use hash to transform password for verification**
**If verification fails then deny access**
**If verification succeeds then grant access**

## Client Login Models and Their Verification

- chan login = [0] of {**short**};
**...**
- active proctype good_client(){
- 	**short **usr_nm = 1;
- 	**short **pswd = -1;
- 	run server();
- 	login!usr_nm;
- 	login!pswd;
**	****accessed?accsd;**}

**Property of Interest**
**No access until hash verification is complete**
**accsd==0 ******** hash_complete==1 **
**Good Client **
**Correct Login**
- Hash verification correlates user and password before access
**Bad Client**
**Circumvents Login**
- Buffer handles data  range of –215 to 215-1 (short data type)
- -65535 overflows buffer
**Access granted before password  hash execution**
**Hash function ignored**

- chan login = [0] of {**short**};
**...**
- active proctype bad_client(){
- 	**short** usr_nm = 1;
- 	**short **pswd = -1;
- 	run server();
- 	login!usr_nm;
- 	login!**-65535**;
- 	accessed?accsd;}

## Property-Based Testing

- Property-based testing tool – Tester’s Assistant (Matt Bishop, UC Davis)
- Perform code slicing on applications for properties for a known set of vulnerabilities
- Test for vulnerabilities in code on the system or whenever the computing environment changes
- Initially, checks software developed in JAVA and C
- The goal is to have the tool check other programming and scripting languages as well (C++, Perl, ActiveX, etc.)

## Property-Based Testing (Cont.):  How It Works

**Notes:**
This slide shows how property-based testing fits into the derivation of assurance. The figure on the left captures what assurance is about: given a knowledge of security and an accurate specification of the security model (which says what you are, and are not, allowed to do), you analyze the software to determine the level of assurance, or belief that the program does what it is supposed to do. The arrow going from the left to the right  shows that security properties, written in TASPEC, capture the idea of the security model The arrow goes to the “properties” box on the right, to emphasize the properties we test for are directly taken from the security properties of the model. We expect the code to honor these.
We next slice the program, or derive the smallest program equivalent to the original with respect to the stated properties. We then instrument and test this program, as described earlier. The testing either validates the properties or shows the do not hold. This helps us determine the level of assurance of the program, as captured by the arrow going from the right to the left.

## Tester’s Assistant Specifications

- No access until hash verified
- Obtain user’s name
- Obtain user’s password
- Is password correct? {
- 	Generate user’s password hash
- 	Compare user's password hash to hash stored for that user name
- 	If match, set UID to user's uid (granting access)
- 	If no match, set UID to ERROR (denying access)
- }
- If access granted {
- 	compare UID to the uid for which access is granted
- 	if match, all is well
- 	if no match, specification violated
- }

## Fed to Test Execution Monitor

**Good login**
- user_password(“me”, “xyz”, 917)
*In state 1*
- password_entered(“xyz”)
*In state 2*
- equals(“xyz”, “xyz”)
*In state 3*
- authenticated(917)
*In state 3A*
- access_acquired(917)
*In state 4*
***Invariant holds***

**Bad login, but access granted due to programming error**
- user_password(“me”, “xyz”, 917)
*In state 1*
- password_entered(“abc”)
*In state 2*
- equals(“abd”, “xyz”)
*Fails, so do not enter state 3*
- access_acquired(917)
*In state 4*
***Invariant fails as state 3A never entered, as invariant require***

## Software Security Checklist (SSC)

- Two Phases
- Phase 1:
- Provide instrument to integrate security as a formal approach to the software life cycle
- Requirements Driven
- Pre-Requirements
- Understand the Problem and Scope
- Requirements Gathering and Elicitation
- Be Aware of Applicable Requirements Documents
- Provide Trace to External Requirements Docs

## SSC (Cont.)

- Phase 2:
- External Release
- Release Process
- Areas for Protection:
- Protect People
- Protect ITAR and EAR
- Protect Trade Secrets – Patents
- Protect Organizational Resources
- Considerations
- Insecure Subsystem Calls
- Embedded IP Addresses or Phone Numbers
- Web Site for Questions and Tools for Code Checking

- Release Process

## Current Work

- Model-Based Verification of SSL Protocol
- Report Submitted to IV&V Center
- Integration of Security into Software Quality Improvement (SQI) at JPL
- Inclusion of Security in Life Cycle Process
- Security Risk Assessment – Potential Use of Defect Detection and Prevention Tool
- Formal Verification of Patchlink Patch Management Software Agent
- Used in All NASA Centers

## Note on Future Work

- Training Course for SSC and Use of Security Assessment Tools
- Experts and Expert Center Available to Assist with the Instrument and Tools
- Integrate with Deep Space Mission Systems (DSMS)
- Verifying SSL and use in DSMS
- Potential to Verify Space Link Extension (SLE) Protocol
- Potential to Verify Space Communication Protocol Standard (SCPS) implementations
- Integrate Project Life Cycle Security Risk Management at JPL with Instrument Support

## David Gilliam, JPL

- 400 Oak Grove Dr., MS 144-210
- Pasadena, CA 91109
- Phone:  (818) 354-0900
- Email:  _[david.p.gilliam@jpl.nasa.gov](mailto:david.p.gilliam@jpl.nasa.gov)_
- John Powell, JPL
- MS 125-233
- Phone:  (818) 393-1377
- Email:	_[john.d.powell@jpl.nasa.gov](mailto:john.d.powell@jpl.nasa.gov)_
- Matt Bishop, UC Davis
- Department of Computer Science
- 3059 Engineering Unit II
- phone: +1 (530) 752-8060
- fax: +1 (530) 752-4767
- email: bishop@cs.ucdavis.edu

***FOR MORE INFO...******	******Web Site:  http://rssr.jpl.nasa.gov/***

## QUESTIONS?

**? ? ?**

## BACKUP SLIDES

## Example C Code

- /* *get user name* */
- if (fgets(stdin, uname, sizeof(uname)–1) == NULL)
- 	return(FAILED);
- /* *get user password* */
- typedpwd = getpass(“Password: “);
- /* *now get information about user with that name* */
- if ((pw = getpwnam(uname)) != NULL){
- 	/* *generate user’s password hash* */
- 	hashtp = crypt(pw->pw_passwd, typedpwd);
- 	/* *compare this to stored hash; if match, grant access* */
- 	if (strcmp(pw->pw_passwd, hashtp) == 0){
- 		/* *match -- grant access* */
- 		setuid(pw->pw_uid);
- 		return(SUCCESS);
- 	}
- 	/* *didn’t match -- fall through to deny access* */
- }
- return(FAILED);

## TASPEC

- View process as sequence of states
- Care only about those related to properties
- State 1: name, hash, uid for user with login name obtained
- State 2: add in hash of password supplied by user
- State 3: add in equality of hash of password supplied by user *and* hash of user with login name
- State 3A (alternate expression of state 3): user has authenticated him/herself
- State 4: add in granting of access

## TASPEC Specification

- /* if assert, enter state 1 */
**location** **func** *getpwnam*(*name*) **result** *pwent*
- 	{ **assert** *user_password*(*name*, *pwent*->*pw_passwd*, *pwent*->*pw_uid*); }
- /* if assert, transition from state 1 to state 2 */
**location** **func** *crypt*(*password*,*salt*) **result** *encryptpwd*
- 	{ **assert** *password_entered*(*encryptpwd*); }
- /* if assert, transition from state 2 to state 3 */
**location** **func** *strcmp*(*s1*, *s2*) **result** 0
- 	{ **assert** *equals*(*s1*, *s2*); }
- /* if in state 3, transition to state 3A */
*password_entered*(*pwd1*) **and ***user_password*(*name*, *pwd2*, *uid*) **and** *equal*(*pwd1*, *pwd2*)
- 	{ **assert** *authenticated*(*uid*) ; }
- /* if assert, transition from state 3A to state 4 */
**location func** *setuid*(*uid*) **result **1
- 	{ **assert** *access_acquired*(*uid*); }
- /* invariant; must always hold */
*authenticated*(*uid*) **before** *access_acquired*(*uid*)

## C Code and States

- if (fgets(stdin, uname, sizeof(uname)–1) == NULL)
- 	return(FAILED);
- typedpwd = getpass(“Password: “);
- if ((pw = getpwnam(uname)) != NULL){
- 	/* *if here, enter state 1* */
- 	hashtp = crypt(pw->pw_passwd, typedpwd);
- 	/* *enter state 2* */
- 	if (strcmp(pw->pw_passwd, hashtp) == 0){
- 		/* *if here, enter state 3 and then 3A* */
- 		setuid(pw->pw_uid);
- 		/* *enter state 4* */
- 		return(SUCCESS);
- 	}
- }
- return(FAILED);