Report ID
2016-03
Report Authors
Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina Pasareanu, Tevfik Bultan
Report Date
Abstract

A crucial problem in software security is the detection of side channels. Information gained by observing non-functional properties of program executions (such as execution time or memory usage) can enable attackers to infer secret information (such as a password). We present an automated approach based on symbolic execution, string analysis, and model counting, for detecting and quantifying side-channels in Java programs. In addition to computing information leakage for a single run of a program, we also compute information leakage for multiple runs for a type of side channels called segmented oracles. In segmented oracles, the attacker is able to explore each segment of a secret (for example each character of a password) independently. We present an efficient technique for segmented oracles that computes information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. Our implementation uses the symbolic execution tool Symbolic Path Finder (SPF), SMT solver Z3, and two model counting constraint solvers LattE and ABC. Although LattE has been used before for analyzing numeric constraints, in this paper, we present an approach for using LattE for analyzing string constraints. We also extend the string constraint solver ABC for analysis of both numeric and string constraints, and we integrate ABC in SPF, enabling quantitative symbolic string analysis.

Document
paper_2.pdf402.17 KB