In this project we seek to identify ways in which the systems development life cycle (SDLC) can be augmented to address security concerns that have arisen in recent years relating to security vulnerability defects in software. Our approach consists of developing an extended contract model to capture and enforce software security properties. Contracts can provide a useful mechanism for the identification, tracking, and validation of security vulnerabilities. In this work, we propose a new contract-based security assertion monitoring framework (CB_SAMF) that is intended to reduce the number of security vulnerabilities that are exploitable across multiple software layers, and to be used in an enhanced SDLC. We develop formal syntax and semantics for our new security contract model using Linear Temporal Logic (LTL). This provides ground for rigorous definition of security assertions characterizing desired properties. Through security activities integrated into the SDLC we can identify potential security vulnerabilities in software systems, which in turn are used for the creation of contracts defining security assertions. Our contract model can then be applied, as runtime probes, against the security vulnerabilities.

We show how contract-based security assertion monitoring can be achieved in a live environment by developing an execution environment based on the Linux operating system.


  • Dr. Issa Traore, Coordinator
  • Mr. Alexander Hoole, Investigator