ESEC/FSE 2018 (series) / JPF 2018 (series) / Java PathFinder Workshop /
Keynote: Side-Channel Analysis via Symbolic Execution and Model Counting
Mon 5 Nov 2018 09:10 - 10:00 at Spring Lake - JPF Workshop
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).
Mon 5 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Mon 5 Nov
Displayed time zone: Guadalajara, Mexico City, Monterrey change
08:30 - 17:00 | |||
09:00 10mDay opening | Opening JPF | ||
09:10 50mTalk | Keynote: Side-Channel Analysis via Symbolic Execution and Model Counting JPF Tevfik Bultan University of California, Santa Barbara | ||
10:00 30mCoffee break | Coffee break JPF | ||
10:30 30mResearch paper | Assessing the Adequacy of Synthetic Programs for Learning SPF's Configurations JPF Maria Paquin Boise State University, Elena Sherman Boise State University, Amit Jain Boise State University | ||
11:00 30mResearch paper | Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) JPF Lucas C. Cordeiro University of Manchester, UK, Daniel Kroening University of Oxford, Peter Schrammel University of Sussex | ||
11:30 30mResearch paper | Attack Synthesis for Strings using Meta-Heuristics JPF Seemanta Saha University of California Santa Barbara, Ismet Burak Kadron University of California at Santa Barbara, USA, William Eiers University of California at Santa Barbara, USA, Lucas Bang , Tevfik Bultan University of California, Santa Barbara | ||
12:00 90mLunch | Lunch @Lakeview Restaurant West JPF | ||
13:30 30mTalk | Invited talk: Test input generation using separation logic JPF Quoc-Sang Phan Fujitsu Laboratories of America | ||
14:00 30mResearch paper | Memory safety in C by abstract interpretation JPF joseph Jones Brigham Young University, James Wasson Brigham Young University, Sean Brown Brigham Young University, Seth Poulsen Brigham Young University, Peter Aldous Brigham Young University, Eric Mercer Brigham Young University | ||
14:30 30mResearch paper | Automatic Data Structure Repair using Separation Logic JPF Guolong Zheng University of Nebraska Lincoln, Quang Loc Le School of Computing, Teesside University, UK, ThanhVu Nguyen University of Nebraska-Lincoln, Quoc-Sang Phan Fujitsu Laboratories of America | ||
15:00 30mCoffee break | Coffee break JPF | ||
15:30 30mResearch paper | A Progress Bar for the JPF Search Using Program Executions JPF Kaiyuan Wang , Hayes Converse The University of Texas at Austin, Milos Gligoric University of Texas at Austin, Sasa Misailovic University of Illinois at Urbana-Champaign, Sarfraz Khurshid University of Texas at Austin | ||
16:00 50mMeeting | JPF Open Discussion JPF | ||
16:50 10mDay closing | Closing JPF | ||
