Symbolic Quantitative Analysis for Software Testing and Security

Quantitative program analysis is an emerging area with applications to software testing and security. In recent years, symbolic quantitative program analysis techniques based on symbolic execution and model counting constraint solvers have been applied to reliability analysis, performance evaluation, information flow analysis, side-channel detection and attack synthesis.In this thesis, I focus on two significant problems in software testing and security: 1) assessment and guidance for testing techniques, and 2) assessment of information leakage. First, I present symbolic quantitative analysis techniques for assessment and guidance of testing techniques by identifying hard-to-reach statements and rare paths in programs, and guiding testing techniques using these information. Then, I present symbolic quantitative analysis techniques for quantifying the amount of information a program can leak, and synthesizing attacks to quantify the maximum amount of information that can be obtained by an attacker.Towards assessing testing difficulty, I develop an efficient and scalable heuristic for probabilistic reachability analysis using branch model counting, dependency analysis, abstract interpretation and probabilistic model checking. The technique I develop can identify hard-to-reach program statements with high precision and accuracy compared to existing techniques based on symbolic execution and statistical sampling.I also develop heuristics to identify rare program paths (program paths that a testing technique is unlikely to explore by generating random inputs) using control flow analysis, dependency analysis and branch model counting. Guiding concolic execution using the rare paths in the program, I can generate inputs that existing coverage-guided mutation-based fuzzing tools cannot. Providing these inputs as the initial seed set to existing fuzzers increases code coverage.Towards quantifying information leakage, I extend the existing symbolic quantitative analysis techniques by providing a framework to compute information leakage bound in presence of approximate model counting. I also generalize the existing side-channel attack synthesis techniques by providing support for unbounded strings using meta-heuristic search and improve efficiency of attack synthesis by exploiting the incremental nature of attack synthesis techniques