Project Description

Vulnerabilities are software bugs that can be used by attackers to alter the execution of programs to achieve harmful consequences. For example, the recent data breach of the private information of hundreds of millions of  Facebook users,  the LockFile ransomware attack, and the series of attacks on U.S. Federal government computer systems all took advantage of vulnerabilities.

Discovering and mitigating software vulnerabilities is a  classic yet challenging security problem due to its variability in nature, priority, and complexity. Software teams often skip low-priority, seemingly innocuous vulnerabilities to ensure effective use of their budget. However, an attacker may exploit a seemingly innocuous vulnerability to gain access to other critical vulnerabilities, resulting in a successful attack. For a given program with a vulnerability, an exploit is an input to the program that triggers the vulnerability. One approach to protecting a program from being exploited by attackers is to generate signatures that will recognize the exploits of the vulnerability. Preconditions and postconditions of a vulnerable program can provide a concise signature that recognizes the specific patterns or inputs associated with that particular vulnerability. Preconditions define the expected state of a program before a specific function or code segment is executed, while postconditions describe the intended state after the execution. 

In this project, we are aiming to use symbolic execution to capture preconditions and postconditions of a detected vulnerability. The system's input can be a tuple <Program, Vulnerability point, Vulnerability condition> that describes exactly one vulnerability, and the output will be the pre and post-condition of that vulnerability. By combining preconditions and postconditions analysis, we can proactively identify vulnerability signatures, understand the conditions that lead to their exploitation, and develop effective countermeasures.

 

Prerequisite Information

None

Knowledge/Skills to Acquire (with guidance from mentors)

Learning prior work and tools on 1) Symbolic Execution 2) Static Analysis 3) Constraint Solvers

Team Members

  • Rick T. Zhang
  • Kaitlyn Tom
  • Shelly Zhu
  • Suhrit Padakanti

Professor and Mentors

  • Prof. Tevfik Bultan
  • Grad mentors: Md Shafiuzzaman, Achintya Desai

Meeting Times

  • Mentor Meetings
    • Thursdays, 5-5:30 p.m.
  • ERSP Team Meetings
    • Thursdays, 8:45-10:45 a.m.

Research Logs