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 non­functional 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).

Conference Day
Mon 5 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:30 - 17:00
JPF WorkshopJPF at Spring Lake
09:00
10m
Day opening
Opening
JPF

09:10
50m
Talk
Keynote: Side-Channel Analysis via Symbolic Execution and Model Counting
JPF
Tevfik BultanUniversity of California, Santa Barbara
10:00
30m
Coffee break
Coffee break
JPF

10:30
30m
Research paper
Assessing the Adequacy of Synthetic Programs for Learning SPF's Configurations
JPF
Maria PaquinBoise State University, Elena ShermanBoise State University, Amit JainBoise State University
11:00
30m
Research paper
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)
JPF
Lucas C. CordeiroUniversity of Manchester, UK, Daniel KroeningUniversity of Oxford, Peter SchrammelUniversity of Sussex
11:30
30m
Research paper
Attack Synthesis for Strings using Meta-Heuristics
JPF
Seemanta SahaUniversity of California Santa Barbara, Ismet Burak KadronUniversity of California at Santa Barbara, USA, William EiersUniversity of California at Santa Barbara, USA, Lucas Bang, Tevfik BultanUniversity of California, Santa Barbara
12:00
90m
Lunch
Lunch @Lakeview Restaurant West
JPF

13:30
30m
Talk
Invited talk: Test input generation using separation logic
JPF
Quoc-Sang PhanFujitsu Laboratories of America
14:00
30m
Research paper
Memory safety in C by abstract interpretation
JPF
joseph JonesBrigham Young University, James WassonBrigham Young University, Sean BrownBrigham Young University, Seth PoulsenBrigham Young University, Peter AldousBrigham Young University, Eric MercerBrigham Young University
14:30
30m
Research paper
Automatic Data Structure Repair using Separation Logic
JPF
Guolong ZhengUniversity of Nebraska Lincoln, Quang Loc LeSchool of Computing, Teesside University, UK, ThanhVu NguyenUniversity of Nebraska-Lincoln, Quoc-Sang PhanFujitsu Laboratories of America
15:00
30m
Coffee break
Coffee break
JPF

15:30
30m
Research paper
A Progress Bar for the JPF Search Using Program Executions
JPF
Kaiyuan Wang, Hayes ConverseThe University of Texas at Austin, Milos GligoricUniversity of Texas at Austin, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Sarfraz KhurshidUniversity of Texas at Austin
16:00
50m
Meeting
JPF Open Discussion
JPF

16:50
10m
Day closing
Closing
JPF