Side channels have been increasingly demonstrated as a practical threat to the confidentiality of private user information. Being able to statically detect these kinds of vulnerabilities is a key challenge in current computer security research. We introduce a new technique, path cost analysis (PCA), for the detection of side channels. Path cost analysis assigns a symbolic cost expression to every node and every back edge of a method’s control flow graph. This cost expression gives an over-approximation for all possible observable values at that node or after traversing that cycle. Queries to a satisfiability solver on the maximum distance between specific pairs of nodes allow us to detect the presence of imbalanced paths through the control flow graph. When combined with taint analysis, we are able to answer the following question – do there exist a pair of paths in the method’s control flow graph, differing only on branch conditions influenced by the secret, which differ in observable value by more than some given threshold. In fact, we are able to specifically state what sets of secret-sensitive conditional statements introduce a side channel detectable given some noise parameter. We extend this approach to an interprocedural analysis, resulting in a sound over-approximation of the number of true side channels in the program. Greater precision can be obtained by combining our method with predicate abstraction or symbolic execution to determine whether a given path through the control flow graph is feasible. We propose evaluating our method on a set of sizeable java server-client applications.
Thu 13 Jul Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change
|10:30 - 11:00|
Jaroslav BendíkMasaryk University
|11:00 - 11:30|
|11:30 - 12:00|