Keynote: Side-Channel Analysis via Symbolic Execution and Model Counting
An important problem in computer security is the detection of side-channel vulnerabilities. Information gained by observing nonfunctional properties of program executions (i.e., side-channels such as execution time or memory usage) can enable attackers to infer secrets that the program accesses (such as a password). In this talk, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for quantifying side-channel leakage in Java programs. I will also discuss automata-based model counting techniques. We have implemented these techniques by integrating our model-counting constraint solver, called Automata-Based model Counter (ABC), with the symbolic execution tool Symbolic Path Finder (SPF).