Symbolic path cost analysis for side-channel detection

Tegan Brennan, Seemanta Saha, Tevfik Bultan, Corina S. Pǎsǎreanu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

28 Scopus citations

Abstract

Side-channels in software are an increasingly significant threat to the confidentiality of private user information, and the static detection of such vulnerabilities is a key challenge in secure software development. In this paper, we introduce a new technique for scalable detection of side-channels in software. Given a program and a cost model for a side-channel (such as time or memory usage), we decompose the control flow graph of the program into nested branch and loop components, and compositionally assign a symbolic cost expression to each component. Symbolic cost expressions provide an over-approximation of all possible observable cost values that components can generate. Queries to a satisfiability solver on the difference between possible cost values of a component allow us to detect the presence of imbalanced paths (with respect to observable cost) through the control flow graph. When combined with taint analysis that identifies conditional statements that depend on secret information, our technique answers the following question: Does there exist a pair of paths in the program's control flow graph, differing only on branch conditions influenced by the secret, that differ in observable side-channel value by more than some given threshold? Additional optimization queries allow us to identify the minimal number of loop iterations necessary for the above to hold or the maximal cost difference between paths in the graph. We perform symbolic execution based feasibility analyses to eliminate control flow paths that are infeasible.We implemented our techniques in a prototype, and we demonstrate its favourable performance against state-of-the-art tools as well as its effectiveness and scalability on a set of sizable, realistic Java server-client and peer-to-peer applications.

Original languageEnglish
Title of host publicationISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis
EditorsEric Bodden, Frank Tip
Pages27-37
Number of pages11
ISBN (Electronic)9781450356992
DOIs
StatePublished - 12 Jul 2018
Event27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018 - Amsterdam, Netherlands
Duration: 16 Jul 201821 Jul 2018

Publication series

NameISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

Conference

Conference27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018
Country/TerritoryNetherlands
CityAmsterdam
Period16/07/1821/07/18

Keywords

  • Side-channel analysis
  • Static analysis
  • Symbolic execution

Fingerprint

Dive into the research topics of 'Symbolic path cost analysis for side-channel detection'. Together they form a unique fingerprint.

Cite this