Speeding Up SMT-Based Quantitative Program Analysis

TL;DR

This paper introduces new techniques to efficiently perform quantitative program analysis, specifically information flow, by mitigating path explosion in SMT-based methods, enabling analysis of larger programs.

Contribution

It presents novel algorithms that leverage program structure to reduce path explosion, improving the scalability of SMT-based quantitative analysis methods.

Findings

Successfully computed channel capacities for programs with large path spaces

Mitigated path explosion using structural properties and new algorithms

Enhanced analysis capability for timing side-channels in complex programs

Abstract

Quantitative program analysis involves computing numerical quantities about individual or collections of program executions. An example of such a computation is quantitative information flow analysis, where one estimates the amount of information leaked about secret data through a program's output channels. Such information can be quantified in several ways, including channel capacity and (Shannon) entropy. In this paper, we formalize a class of quantitative analysis problems defined over a weighted control flow graph of a loop-free program. These problems can be solved using a combination of path enumeration, SMT solving, and model counting. However, existing methods can only handle very small programs, primarily because the number of execution paths can be exponential in the program size. We show how path explosion can be mitigated in some practical cases by taking advantage of special branching structure and by novel algorithm design. We demonstrate our techniques by computing the channel capacities of the timing side-channels of two programs with extremely large numbers of paths.