# Presentation: 099893

## Reducing Software Security Risk Through an Integrated Approach 

**David Gilliam, John Powell, & John Kelly**
**Jet Propulsion Laboratory**
**Matt Bishop **
**University of California at Davis**

- California Institute of Technology, Jet Propulsion Lab

## NASA RTOP: 

- Reducing Software Security Risk

**NOTE:  **
**	****This work is sponsored by NASA's Office of Safety and Mission Assurance under the NASA Software Program lead by the NASA Software IV&V Facility**
**	**
**	****This activity is managed locally at JPL through the Assurance and Technology Program Office (502)**

## Research Goal

**Growth of internet, network aware applications and collaborative work **
**NASA’s computing environment at risk—viruses, worms, trojan programs, and intrusions**
**Potential damage to NASA tasks and projects**
**Reduce security risk to the computing environment by mitigating vulnerabilities in the software development and maintenance life cycles**
**Vulnerability Matrix (VM) **
**Security Assessment Tools List (SATs)**
**Property-based Testing (PBT) tool—Tester’s Assistant**
**Model-Based security specification and verification tool (MBV)**

**Notes:**
Reduce vulnerabilities with network/internet aware applications
Inter-planetary Network (IPN)

## Research Goal (Cont.)

**Provide software security assessment instrument**
**Software Engineers, Programmers, System Administrators**
**Instrument used collectively or as individual tools**

## Real Project Application

**JPL/NASA Class A Flight Project**
**Will test toolset on Flight Mission internet-aware communication software**
**Other NASA & JPL Projects**
**Potential for use with the Inter-Planetary Network (IPN)**
**JPL/NASA Project WebSite:  http://security.jpl.nasa.gov/rssr**

## Vulnerability Matrix

**Vulnerability matrix to assist security experts and programmers where best to expend their efforts**
**VM:  DOVES database (maintained by UC Davis):  **_**[http://seclab.cs.ucdavis.edu/projects/ ](http://seclab.cs.ucdavis.edu/projects/vulnerabilities/)**_
**Uses the Common Vulnerabilities and Exposures (CVE) Listing (MITRE)**
**	**_**[http://cve.mitre.org/cve/](http://cve.mitre.org/cve/)**_
**Contains signatures used to exploit the vulnerability – signature properties can be used with the Tester’s Assistant (TA) and the Modeling SPIN Tool (MBV)**
**Will include properties for each vulnerability or exposure for use with the TA and the MBV instruments**

## Security Assessment Tools

**Software Security Assessment Instrument**
**Security assessment tools**
**Description of each tool and its purpose**
**Pros and Cons of each tool**
**Alternate and related tools**
**Maintained by UC Davis (for future additional tools)**

## 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 **
**The goal is to have the tool check other programming and scripting languages as well (C, C++, Perl, ActiveX, etc.)**

## Property-Based Testing (Cont.)

**Compare program actions with specifications**
**Create low-level specifications**
**Instrument program to check that these hold**
**Run program under run-time monitor**
**Report violations of specifications**

**Notes:**
Overview

Property-based testing is a testing technique that models very mathematical techniques for proving software correct. The problem is that the mathematical techniques are impractical. So property-based testing uses the same principles, but applies them in an informal way: by testing that the program matches its requirements.
The requirements are specified using a little language called TASPEC that is very low-level. It expresses specifications at the level of the program. Basically, TASPEC creates a small state machine based upon assertions, which are statements of properties, and invariants, which are specifications that must hold.
The tester is given the TASPEC properties. The program is then reduced to the smallest program that will compile and is equivalent to the original program; that is, the original program and the new one always have the same assertions made. The new program is instrumented to emit the assertions as required.
The program is then executed under a run-time monitor. This monitor reads the assertions, and whenever an invariant should hold, checks that it does. This may occur when a particular set of assertions is made, or throughout the execution of the program.

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

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

- *Backup Slides provide an example on how this works with the TASPEC

**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.

## Model-Based Security Specification

**Model-based security specification and verification involves applying formal modeling to the IT security arena**
**Verification systems that perform logical verification of temporal properties over models are referred to as **_**model checkers**_
**Exhaustive search of a model’s corresponding state space**** **
**Can be used on suitably restricted “partial specifications”**

## Model Based Verification (MBV) within an Integrated Approach

- VMatrix

- PBT

- MBV

**Attacks not found **
**in the Wild**

**Flexible Modeling Framework (FMF)**
**Compositional Approach**
**Makes use of SPIN**
**Infers Results from a partial model**

**Property Interaction with**

-  **Vulnerability Matrix (VM)**

-   **Property Based Testing (PBT)**

**Potentially discovers new vulnerabilities**

## Summary

**Growth of NASA’s network aware software applications and collaborative work increase risk to NASA environment**
**Risk will continue to increase as collaboration increases**
**Software Security Assessment Instrument for use in the software development and maintenance lifecycle**

## Summary (Cont.)

**Assessment Instrument composed of three tools and reports:**
**Vulnerability Matrix**
**Tester’s Assistant**
**Model-Based Verification**
**Tools can be used collectively or individually**
**There is a potential for wider application of the instrument beyond assessment of security of software**

## Collaborators

**David Gilliam – Principle Investigator **
**	****	****Network and Computer Security, JPL**
**John Powell – Research Engineer **
**	****	****Quality Assurance, JPL**
**John Kelly – RTOP Manager**
**	****	****Quality Assurance, JPL**
**Matt Bishop – Associate Professor of Computer Science **
**	****	****University of California at Davis**

## David Gilliam

**JPL**
**400 Oak Grove Dr., MS 144-210**
**Pasadena, CA 91109**
**Phone:  (818) 354-0900****	****	****FAX: (818) 393-1377**
**Email:  david.p.gilliam@jpl.nasa.gov**
**Website:  http://security.jpl.nasa.gov/rssr/**
**John Powell**
**MS 125-233**
**Phone:  (818) 393-1377****	**
**Email:****	****john.d.powell@jpl.nasa.gov**

***FOR MORE INFO...***

## Backup Slides

## Model – Based Specification & Verification

## Model Checking: A Case Study Simplified State Machine for Prime

**Model Checking: A Case Study ****Simplified State Machine for Prime**

- PRIME

- BACKUP

- Prime init

- suspend

- PRIME NOMINAL

- SEQUENCE IDLE

- Power-up
- Idle

- Fault
- Idle

- SFP
- ACTIVE

- SEQUENCE CRITICAL

**System fault protection (SFP)**
**  ****Response Active**

**SFP Response**
**Done**

**Done**

**Activate**

**Resume**
**from**
**mark point**

- “Validating Requirements for Fault Tolerant Systems Using Model Checking”, Schneider, Callahan & Easterbrook,  1998
*This Case Study was funded by the NASA Software Program  at the NASA IV&V Facility and JPL under a separate task  *

## State Charts

**State Charts are specification notations to define systems **
**Defines the collection of (abstract) variable value pairs at a given point in the system (execution) – referred to as a state**
**Defines the relationships with which the system transitions from one state to the another**

## The Flexible Modeling Framework (FMF) Approach to MBV

**A Component (c) is some logical unit of  process or application behavior**
**A single application often will need to broken into multiple model components**
**Combining two components C1 and C2**
**Model Checking (MC)**
**Non-trivial combination of C1 and C2**
**Searches the Cartesian Product of the sizes of C1 and C2**
**FMF **
**MC of C1 and C2 individually**
**Combines the State Charts (SC) of C1 and C2**
**Integrates assumptions that follow from 1 above**
**SC traversal or *****localized *****MC of appropriate sub-model**

## Domain Specifics and FMF

**C1**
**C2**
**MC reports p holds for C1 and C2 **
**Assumptions can be made about transitions (T) in C1/C2 SC**
**P holds on T from C1 ^ C2**
**P holds on T from C1 ^ (Unknown in C2)**
**P holds on T from (Unknown in C1) ^ C**
**Unify consistent states in the SCs of C1 and C2**
**Condition:  All variables that are known in C1 and C2 agree**
**Any path from “O” that does not reach “~O” produces an unknown security result when the combined C1/C2**

**O @ t(x)**

**~O @ t(x+n)**

**Property p must hold**

**O @ t(y)**

**~O @ t(y+m)**

**Property p must hold**

## Combinatorial Network Aware Cases being Addressed

**C1**
**C2**
**Network Aware (NA) Cases:**
**t(x) = t(y) – C1 and C2 are NA simultaneously**
**t(x+n) = t(y) – C1 ends NA sequence and C2 starts NA sequence simultaneously**
**t(x) = t(y+m) – C2 ends NA sequence and C1 starts NA sequence simultaneously**
**Sub cases where (n = m) and (n != m) – not currently known if this distinction is significant with an abstract model in this domain**

**O @ t(x)**

**~O @ t(x+n)**

**Property p must hold**

**O @ t(y)**

**~O @ t(y+m)**

**Property p must hold**

## Combinatorial Network Aware Cases being Addressed (Cont.)

**The same timing cases seen on the previous slide must be considered in the context of one NA component (C1) and one non-NA component (C2)**
**C1 occurring in a time relation case previously discussed while sharing resources in common may potentially create vulnerabilities.**
**E.g.  A NA control application and a printer**
**Non NA components (application pieces) may have been justifiably engineered with little or no consideration of network security issues**
**A non-NA component may represent a piece of a NA application that does not interact with a network.**
**I.E.  t(X+n) < t(y), t(x) > t(y+m)**

## Property – Based Testing

## Property-Based Tester

**Notes:**
Finally, this slide shows the “Tester’s Assistant” used to test programs. It takes as input the program and program-specific specifications. It has libraries of useful security specifications, specifications of system calls (such as for setuid), for library functions (such as for getpwnam and strcmp), and applies standard testing techniques to the slice, or transformed, program.
The results are test data that was used to test the program, a measure of completeness (how complete was the test coverage; were all paths exercised, were only some, etc.), and what problems were uncovered.

## Property-Based Tester

**TASPEC language definitions**
**Handle ambiguous specifications and facts**
**Resetting, non-resetting temporal operators**
**Existential, universal logical operators**
**Design Decisions**
**Instrumenter does most work**

**Notes:**
Example of an ambiguous specification and fact: the following facts are defined
	authenticated(Alice), password(Alice), password(Bob)
The invariant is
	authenticated(X) before password(X)
Is this true or false? Both: true for X = Alice, false for X = Bob. Which to report? We chose true (I.e., if it’s true for any X).

Example of problem with temporal operators: suppose we have “X before Y”. Does this mean “Every time Y becomes false, X will become true before Y becomes true again” (resetting) or “X will become true before Y next becomes true” (non-resetting)? We use the latter, although either is equally valid.

Example of problem with logical operators: suppose we have “A and B implies A < B”. If interpreted existentially, then if any A is less than any B, the expression is true but if interpreted universally, all A must be less than all B. Both counter-intuitive. Approach: and, or are existential, implies is universal. Not (negation) is interpreted universally, i.e., not A means “There is not any instantiation of variables that will make X true”. These provide the most intuitive results, with some caution: De Morgan’s laws, for example, are not true any more.

Rather than have the execution monitor read in and process the specification file and handle location specifiers, the code is instrumented to emit the processed specifications and handle location specifiers. This makes the execution monitor faster, which makes it more amenable to real-time analysis.

## Tester’s Assistant Specifications

**Example: “a user must authenticate himself or herself before acquiring privileges”**
**is password correct? {**
**	****Compare user's password hash to hash stored for that user name**
**	****If match, set UID to user's uid**
**	****If no match, set UID to ERROR **
**}**
**if privileges granted {**
**	****compare UID to the uid for which privileges are granted**
**	****if match, all is well**
**	****if no match, specification violated**
**}**

**Notes:**
Let’s go through this process slowly, so you get a feel for how it works. First, specification. We need to map these into a very low level. So here is one for a login program on a UNIX-like system. At the highest level, the login completes when the user acquires privileges of the user being logged in.
Now, what does this mean at the code level? A user authenticates himself or herself by supplying a login name and the corresponding password. So, first we require the password to be right. We do this by comparing a hash from the user’s password as typed to the hash stored in a file. On success, we obtain the user’s number (UID) for later use. On failure, we set the UID to something bogus.
Next comes the acquiring of privileges. If privileges are granted, one particular system call is used, and it takes as its argument a UID. 
So we have two parts: “authentication” and “acquiring privileges”. We have to put them together. So, we require the authentication to come first (hence the ordering) and then that the UID for which privileges are acquired match that of the authenticated user. If the two UIDs match, and authentication preceded the acquisition of privileges, we’re fine. Otherwise the program violated its specification.

## Example C Code

**if (fgets(stdin, uname, sizeof(uname)–1) == NULL)**
**	****return(FAILED);**
**typedpwd = getpass(“Password: “);**
**if ((pw = getpwnam(uname)) != NULL){**
**	****hashtp = crypt(pw->pw_passwd, typedpwd);**
**	****if (strcmp(pw->pw_passwd, hashtp) == 0){**
**	****	****setuid(pw->pw_uid);**
**	****	****return(SUCCESS);**
**	****}**
**}**
**return(FAILED);**

**Notes:**
This is a segment of C code that performs the login. The first “if” statement gets the login name.  The call to the function getpass gets the typed password.
The next “if” statement sees if there is a user of the given name. If so, the function getpwnam returns information about the user, the key pieces being the hashed password (in the pw->pw_passwd field) and the user’s UID (in the pw->pw_uid field). The typed password is then hashed using the appropriate hash function (which is encoded in the stored hash). The resulting hash, hashtp, is compared to the stored hash. If they match, the user has entered the correct password, is authenticated, and the function setuid is called with that user’s UID. This causes the process to acquire that user’s privileges.
In this function, if SUCCESS is returned, the program has successfully acquired privileges. If FAILURE is returned, the program has not.

## In TASPEC

- location func** *****setuid*****(*****uid*****) **result **1**
**	****{ **assert** *****privileges_acquired*****(*****uid*****); }**
- location** **func** *****crypt*****(*****password*****,*****salt*****) **result** *****encryptpwd***
**	****{ **assert** *****password_entered*****(*****encryptpwd*****); }**
- location** **func** *****getpwnam*****(*****name*****) **result** *****pwent***
**	****{ **assert** *****user_password*****(*****name*****, *****pwent*****->*****pw_passwd*****, *****pwent*****->*****pw_uid*****); }**
- location** **func** *****strcmp*****(*****s1*****, *****s2*****) **result** 0**
**	****{ **assert** *****equals*****(*****s1*****, *****s2*****); }**
***password_entered*****(*****pwd1*****) **and
- 			***user_password*****(*****name*****, *****pwd2*****, *****uid*****) **and** *****equal*****(*****pwd1*****, *****pwd2*****)**
**	****{ **assert** *****authenticated*****(*****uid*****) ; }**
***authenticated*****(*****uid*****) **before** *****privileges_acquired*****(*****uid*****)**

**Notes:**
Now here’s what this looks like in TASPEC. The “location func” keywords bind assertions and actions to invocation of functions. So when setuid is called, the predicate “privileges_acquired(UID)” is placed into the representation of the state, where UID is the same UID as given to setuid.
The next three keywords trigger when the appropriate functions are called.
The next-to-last statement is invoked when the three assertions hold. It asserts that “authenticated(UID)” holds.
The last line is an invariant that says whenever “privileges_acquired(UID)”  is asserted, “authenticated(UID)” must hold. Otherwise there is an error.
So, merging this with the previous program ...

## Merging

**if (fgets(stdin, uname, sizeof(uname)–1) == NULL)**
**	****return(FAILED);**
**typedpwd = getpass(“Password: “);**
**if ((pw = getpwnam(uname)) != NULL){**
**	****hashtp = crypt(pw->pw_passwd, typedpwd);**
**	****if (strcmp(pw->pw_passwd, hashtp) == 0){**
**	****	****setuid(pw->pw_uid);**
**	****	****return(SUCCESS);**
**	****}**
**}**
**return(FAILED);**

**user_password(uname, pw->pw_passwd, pw->pw_uid)**

**user_password(uname, pw->pw_passwd, pw->pw_uid)**
**password_entered(hashtp)**

**user_password(uname, pw->pw_passwd, pw->pw_uid)**
**password_entered(hashtp)**
**equals(pw->pw_passwd, hashtp)**
**authenticated(pw_>pw_uid)**

**Notes:**
This combines the previous two slides. The arrows show the assertions at each step. These are actually emitted into another process, the run-time monitor, that checks to ensure no invariants are violated.
Notice that each call of a function in the specification adds to the state. In the last call (to strcmp), the three assertions cause the fourth to be added.
The use of these invariants also allows us to build a library of invariants that cover vulnerabilities ranging from race conditions to buffer overflows to other things.

## Potential Follow-On Work

**Training in use of security assessment tools in the software development and maintenance life-cycle**
**Development of re-composable model sub-components**
**Develop capability for easy storage and access of a library of common network security model components and past verification results**
**Develop a programmer interface to assist users with generating properties for input into the tools**

## Potential Follow-On Work (cont.)

**Enhancing and augmenting the toolset**
**Port the code to run on different operating systems**
**Include additional programming and scripting languages that the Tester’s Assistant tool can slice for vulnerabilities**
**Augment the toolset by incorporating or developing additional tools**
**Develop a graphical user interface front-end checklist and decision tree to assist in building the Model to be verified**