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.