CS 706 Project Presentation Schedule

Aiqing Huang, Jocelyn Chen, and Prasanna Venkatesh Ramadas

Testing is a significant and critical phase of software development that aims at assuring software quality to the end user, and static code analysis is a white box method of testing to detect potential errors without actually running the program. With an ideal goal that static analysis tools should be sound and complete, program analysis research focusses on moving strategies close to perfection. However, in the process static analysis tools may be over cautious by reporting potential errors not viable given the context or errors that aren’t errors. This reporting of false positives may annoy or intimidate a developer and may lead to potential time wasted in fixing them. Also, since the severity of bug is highly context-dependent, it is essential to learn a program with its context. We propose a bug prioritization scheme to alleviate this problem by extracting locality and bug co-occurrence information from multiple bug reports. Our proposed model is based on random forests for predicting false positive probability given the outputs of common static analysis tools. With a random sample of 304 bug instances output by FindBugs, PMD and SpotBugs, the model was found to exhibit a false positive rate of 0.0543 using random forests and 0.1087 using the baseline logistic regression while the conventional tools suffer from a false positive rate close to 0.6. The bug classifier model has an accuracy of 0.654 using random forests and 0.544 using the baseline logistic regression.

Zi Wang

In this work, we wish to synthesize test cases that lead to divergent behaviors on two or more similar programs. These behaviors could be acceptance and rejection of the programs over an input. For example, if we find an input that Microsoft Office accepts but LibreOffice rejects, then it can serve as a starting point for debugging.

Our approach is motivated by American Fuzzy Lop (AFL), the state of the art fuzzer. The guidance for AFL during fuzzing is to generate inputs with new execution trace on the program. Instead, if we have the coverage information of an input over a program, we could use this to measure the distance between the current coverage and the target basic block, which can be used as the guidance for our purpose. Combining the measures of an input on multiple programs, we wish to generate an input that will lead to the coverage we wish to achieve, for example, in some programs one of covered basic blocks containing an acceptance statement while in others one of covered basic blocks containing an rejection statement.

John Cyphert

Currently, there is great interest in automatically identifying and proving programs are free from side-channel attacks. One approach for proving the absence of side-channel attacks is through the verification of non-interference. Barthe et al. (2004) showed how non-interference could be reduced to a safety property via a self-composition construction. However, self-composition is often insufficient for verification of non-interference, because the analyzer must asynchronously summarize program behavior across multiple runs to a very high accuracy. Some have rectified this issue by building specialized analyses that consider program products. These analyses sometimes synchronously summarize behavior across multiple program runs. This synchronous comparison allows the analysis to create simpler summaries which imply non-interference. The current difficulty with these analyses is that the program products are built into the analysis, and thus are not readily available to the rich field of program assertion checkers.

In this talk I will give background into non-interference, self-composition, and product programs. I will also present a novel syntax directed algorithm that automatically constructs a new type of product program. This construction is less weighty then previous constructions and could be fed into any off-the-self assertion checker to prove non-interference.