Write a Blog >>
Thu 21 Jan 2016 14:20 - 14:45 at Grand Bay North - Track 1: Learning and verification Chair(s): David Monniaux

Static analysis has been successfully used in many areas, from verifying mission-critical software to malware detection. Unfortunately, static analysis often produces false positives, which require significant manual effort to resolve. In this paper, we show how to overlay a probabilistic model, trained using domain knowledge, on top of static analysis results, in order to triage static analysis results. We apply this idea to analyzing mobile applications. Android application components can communicate with each other, both within single applications and between different applications. Unfortunately, techniques to statically infer Inter-Component Communication (ICC) yield many potential inter-component and inter- application links, most of which are false positives. At large scales, scrutinizing all potential links is simply not feasible. We therefore overlay a probabilistic model of ICC on top of static analysis results. Since computing the inter-component links is a prerequisite to inter-component analysis, we introduce a formalism for inferring ICC links based on set constraints. We design an efficient algorithm for performing link resolution. We compute all potential links in a corpus of 10,928 applications in 24 minutes and triage them using our probabilistic approach. We find that over 97.3% of all 489 million potential links are associated with probability values below 0.01 and are thus likely unfeasible links. Thus, it is possible to consider only a small subset of all links without significant loss of information. This work is the first significant step in making static inter-application analysis more tractable, even at large scales.

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00: Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David MonniauxCNRS, VERIMAG
14:20 - 14:45
Talk
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg
Media Attached
14:45 - 15:10
Talk
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK
Media Attached
15:10 - 15:35
Talk
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign
Media Attached
15:35 - 16:00
Talk
Symbolic Abstract Data Type Inference
Research Papers
Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot
Media Attached