Project Description
Quantitative program analysis is an emerging area with applications to software reliability, quantitative information flow[1], side-channel detection and attack synthesis[2]. Recently, quantitative program analysis techniques based on symbolic execution and model counting constraint solvers[3] have been applied to quantifying information leakage due to side-channels[4]. Most of the recent quantitative program analysis techniques use Symbolic Path Finder (SPF) [5] as a symbolic execution engine and apply the quantitative program analysis techniques to Java code. These techniques currently cannot support large programs due to scalability issues with SPF. We believe that there is an opportunity to apply these techniques to programs written in C and show their effectiveness for analyzing security sensitive C code. KLEE [6] is a popular symbolic execution tool for C and it has been applied to large real world programs. But, so far there is no support for quantitative analysis in KLEE. In this project, the goal is to integrate existing model counting tools [7,8] with KLEE to support quantitative program analysis for C programs.
Team Members
- Kunal Handa (kunalhanda@umail.ucsb.edu)
- Olivia Gillam (oliviagillam@ucsb.edu)
- Surendra Ghentiyala (surendra@umail.ucsb.edu)
- Victoria Reed (victoriareed@ucsb.edu)
Professor and Mentors
- Professor: Prof. Tevfik Bultan (bultan@ucsb.edu)
- Mentor: Seemanta Saha (seemantasaha@ucsb.edu)
Meeting Time
- Meeting with Advisor:
- Location: Zoom
- Time: Wed, 11am-noon
- Meeting with Team:
- Location: Zoom
- Time: Mon- 5:50 to 6:50pm, Wed- 6 to 7pm
- Meeting with Prof. Mirza and Prof. Eiers:
- Location: Zoom
- Time: Th - 2-2:30pm
Links to Proposals and Presentation
- Proposal link
- Final presentation: