Citation
Osbert Bastani. "Interactive Information Flow Analysis of Android Apps". Talk or presentation, October, 2015.

Abstract
Static information flow analysis has the potential to greatly aid human auditors in finding privacy violations and malicious software. However, challenges in scaling sound, precise static analyses mean that an auditor must settle for either imprecise results (generating many false positives, which can be time-consuming to discharge) or unsound results (which makes it easy for adversaries to hide malicious behaviors). We propose a verification approach that relies on interaction with a human auditor to eliminate false positives. In our approach, the static analysis queries the auditor about program properties, and uses abductive inference to minimize the number of queries needed. We apply this approach to solve two problems we have encountered in practice: (i) synthesizing models for relevant library functions, and (ii) removing dead code that causes imprecision in the analysis.

Electronic downloads

• seminar.2015-10-19.Osbert_Bastani.pdf · application/pdf · 2963 kbytes

• HTML

  Osbert Bastani. <a
  href="http://chess.eecs.berkeley.edu/pubs/1147.html"
  ><i>Interactive Information Flow Analysis of
  Android Apps</i></a>, Talk or presentation, 
  October, 2015.

• Plain text

  Osbert Bastani. "Interactive Information Flow Analysis
  of Android Apps". Talk or presentation,  October, 2015.

• BibTeX

  @presentation{Bastani15_InteractiveInformationFlowAnalysisOfAndroidApps,
      author = {Osbert Bastani},
      title = {Interactive Information Flow Analysis of Android
                Apps},
      month = {October},
      year = {2015},
      abstract = {Static information flow analysis has the potential
                to greatly aid human auditors in finding privacy
                violations and malicious software. However,
                challenges in scaling sound, precise static
                analyses mean that an auditor must settle for
                either imprecise results (generating many false
                positives, which can be time-consuming to
                discharge) or unsound results (which makes it easy
                for adversaries to hide malicious behaviors). We
                propose a verification approach that relies on
                interaction with a human auditor to eliminate
                false positives. In our approach, the static
                analysis queries the auditor about program
                properties, and uses abductive inference to
                minimize the number of queries needed. We apply
                this approach to solve two problems we have
                encountered in practice: (i) synthesizing models
                for relevant library functions, and (ii) removing
                dead code that causes imprecision in the analysis.},
      URL = {http://chess.eecs.berkeley.edu/pubs/1147.html}
  }
  

Posted by Sadigh Dorsa on 26 Oct 2015.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.