Quantitative information-flow (QIF) analysis provides a measure of the amount of information revealed when a program runs. For instance, if a program operates on secret (private, confidential, etc.) data, QIF measures in bits of the amount of information about that secret that can be inferred from the program's outputs or other observable behaviors. One class of powerful techniques for this analysis starts by symbolically executing software to characterize its input-output relation as a formula, and then uses model counting applied to such a formula to provide an information-flow estimate. Model counting is the problem of counting the number of solutions to a logical formula. Even approximate model counting can be quite expensive; I'll describe a technique we've developed to speed up hashing-based approximate model counting by using a statistical model to choose queries (TACAS 2018). Then I'll put this in a broader context using binary symbolic execution to perform QIF analysis of complete programs. To improve the scalability of this measurement to larger programs, I'll describe our ongoing work on a hybrid approach that uses precise-but-expensive model counting to improve the precision of a scalable-but-conservative approach based on network flow capacity (PLDI 2008).
(research joint with Seonmo Kim and Navid Emamdoost, UMN)
Stephen McCamant has been an Assistant Professor of Computer Science and Engineering at the University of Minnesota since the fall of 2012, where his main research area is program analysis for software security and correctness. He is especially interested in binary code analysis and transformation, hybrid dynamic/static techniques and symbolic execution, information flow/taint analysis, and applications of decision procedures. His research on software-based fault isolation was a key foundation for the Google Native Client system, and he is the primary author of the FuzzBALL binary symbolic execution system which participated in the DARPA Cyber Grand Challenge and is available open-source. He received his Ph.D from MIT in 2008, and from 2008-2012 he was a postdoc at UC Berkeley.