Specification Inference Using Context-Free Language Reachability

Abstract

We present a framework for computing context-free language reachability properties when parts of the program are missing. Our framework infers candidate specifications for missing program pieces that are needed for verifying a property of interest, and presents these specifications to a human auditor for validation. We have implemented this framework for a taint analysis of Android apps that relies on specifications for Android library methods. In an extensive experimental study on 179 apps, our tool performs verification with only a small number of queries to a human auditor.

Document Details

Document Type
Pub Defense Publication
Publication Date
Jan 14, 2015
Source ID
10.1145/2775051.2676977

Entities

People

  • Alex Aiken
  • Osbert Bastani
  • Saswat Anand

Organizations

  • Air Force Research Laboratory
  • Stanford University

Tags

Fields of Study

  • Computer science

Readers

  • Agent-Based Social Robotics and Mobile-Assisted Learning in Virtual Environments.
  • Computational Linguistics

Technology Areas

  • AI & ML
  • AI & ML - Bayesian Inference
  • AI & ML - Machine Translation