skip to main content
research-article

Specification Inference Using Context-Free Language Reachability

Published: 14 January 2015 Publication History

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.

Supplementary Material

MPG File (p553-sidebyside.mpg)

References

[1]
A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, P. Hawkins. An overview of the Saturn project. In PASTE, 43--48, 2007.
[2]
K. Ali, O. Lhoták. Averroes: whole-program analysis without the whole program. In ECOOP, 2013.
[3]
R. Alur, P. Černy, P. Madhusudan, W. Nam. Synthesis of interface specifications for Java classes. In POPL, 2005.
[4]
G. Ammons, R. Bodík, J. Larus. Mining specifications. In POPL, 2002.
[5]
S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel, J. Klein, Y. L. Traon, D. Octeau, P. McDaniel. FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In PLDI, 2014.
[6]
T. Ball, S. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, 2002.
[7]
N. Beckman, A. Nori. Probabilistic, modular and scalable inference of typestate specifications. In PLDI, 2011.
[8]
W. Enck, P. Gilbert, B. Chun, L. Cox, J. Jung, P. McDaniel, A. Sheth. TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In OSDI, 2010.
[9]
A. P. Fuchs, A. Chaudhuri, J. S. Foster. SCanDroid: automated security certification of Android applications. In IEEE Symposium on Security and Privacy, 2010.
[10]
D. Greenfieldboyce, J. S. Foster. Type qualifier inference in Java. In OOPSLA, 2007.
[11]
J. Kodumal, A. Aiken. Banshee: a scalable constraint-based analysis toolkit. In SAS, 2005.
[12]
J. Kodumal, A. Aiken. Regularly annotated set constraints. In PLDI, 2007.
[13]
J. Kodumal, A. Aiken. The set constraint/CFL reachability connection in practice. In PLDI, 2004.
[14]
D. Knuth. A generalization of Dijkstra's algorithm. In Information Processing Letters, 6(1):1--5, 1977.
[15]
T. Kremenek, P. Twohey, G. Back, A. Ng, D. Engler. From uncertainty to belief: inferring the specification within. In OSDI, 2006.
[16]
B. Livshits, A. V. Nori, S. K. Rajamani, A. Banerjee. Merlin: specification inference for explicit information flow problems. In PLDI, 2009.
[17]
B. Livshits, M. S. Lam. Finding security vulnerabilities in Java applications with static analysis. In USENIX Security Symposium, 2005.
[18]
B. Livshits, M. S. Lam. Tracking pointers with path and context sensitivity for bug detection in C programs. In FSE, 2003.
[19]
D. Melski, T. Reps. Interconvertibility of a class of set constraints and context-free language reachability. In Theoretical Computer Science, 248(1):29--98, 2000.
[20]
M. Naik, A. Aiken, J. Whaley. Effective static race detection for Java. In PLDI, 2006.
[21]
J. W. Nimmer, M. D. Ernst. Automatic generation of program specifications. In ISSTA, 2002.
[22]
M. K. Ramanathan, A. Grama, S. Jagannathan. Static specification inference using predicate mining. In PLDI, 2007.
[23]
T. Reps. Program analysis via graph reachability. In ILPS, 1997.
[24]
T. Reps, S. Horwitz, M. Sagiv. Precise interprocedural data flow analysis via graph reachability. In POPL, 1995.
[25]
S. Shoham, E. Yahav, S. Fink, M. Pistoia. Static specification mining using automata-based abstractions. In ISSTA, 2007.
[26]
M. Sridharan, D. Gopan, L. Shan, R. Bodik. Demand-driven points-to analysis for Java. In OOPSLA, 2005.
[27]
M. Sridharan, S. Artzi, M. Pistoia, S. Guarnieri, O. Tripp, R. Berg. F4F: taint analysis of framework-based web applications. In OOPSLA, 2011.
[28]
M. Sridharan, R. Bodik. Refinement-based context-sensitive points-to analysis for Java. In PLDI, 2006.
[29]
O. Tripp, M. Pistoia, S. J. Fink, M. Sridharan, O. Weisman. TAJ: effective taint analysis of web applications. In PLDI, 2009.
[30]
R. Vallée-Rai, P. Co, E. Gagnon, L. Hendren, P. Lam, V. Sundaresan. Soot: a Java bytecode optimization framework. In CASCON, 1999.
[31]
J. Whaley, M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In OOPSLA, 2004.
[32]
Y. Xie, A. Aiken. Static detection of security vulnerabilities in scripting languages. In USENIX Security Symposium, 2006.
[33]
J. Yang, D. Evans, D. Bhardwaj, T. Bhat, M. Das. Perracotta: mining temporal API rules from imperfect traces. In ICSE, 2006.
[34]
H. Zhu, T. Dillig, I. Dillig. Automated inference of library specifications for source-sink property verification. In APLAS, 2013.

Cited By

View all
  • (2023)Recursive State Machine Guided Graph Folding for Context-Free Language ReachabilityProceedings of the ACM on Programming Languages10.1145/35912337:PLDI(318-342)Online publication date: 6-Jun-2023
  • (2021)Systemizing Interprocedural Static Analysis of Large-scale Systems Code with GraspanACM Transactions on Computer Systems10.1145/346682038:1-2(1-39)Online publication date: 29-Jul-2021
  • (2020)C2S: translating natural language comments to formal program specificationsProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409716(25-37)Online publication date: 8-Nov-2020
  • Show More Cited By

Index Terms

  1. Specification Inference Using Context-Free Language Reachability

        Recommendations

        Comments

        Information & Contributors

        Information

        Published In

        cover image ACM SIGPLAN Notices
        ACM SIGPLAN Notices  Volume 50, Issue 1
        POPL '15
        January 2015
        682 pages
        ISSN:0362-1340
        EISSN:1558-1160
        DOI:10.1145/2775051
        • Editor:
        • Andy Gill
        Issue’s Table of Contents
        • cover image ACM Conferences
          POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
          January 2015
          716 pages
          ISBN:9781450333009
          DOI:10.1145/2676726
        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        Published: 14 January 2015
        Published in SIGPLAN Volume 50, Issue 1

        Check for updates

        Author Tags

        1. program analysis
        2. specification inference
        3. verification

        Qualifiers

        • Research-article

        Funding Sources

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • Downloads (Last 12 months)11
        • Downloads (Last 6 weeks)0
        Reflects downloads up to 19 Feb 2025

        Other Metrics

        Citations

        Cited By

        View all
        • (2023)Recursive State Machine Guided Graph Folding for Context-Free Language ReachabilityProceedings of the ACM on Programming Languages10.1145/35912337:PLDI(318-342)Online publication date: 6-Jun-2023
        • (2021)Systemizing Interprocedural Static Analysis of Large-scale Systems Code with GraspanACM Transactions on Computer Systems10.1145/346682038:1-2(1-39)Online publication date: 29-Jul-2021
        • (2020)C2S: translating natural language comments to formal program specificationsProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409716(25-37)Online publication date: 8-Nov-2020
        • (2019)Path Querying with Conjunctive Grammars by Matrix MultiplicationProgramming and Computing Software10.1134/S036176881907004145:7(357-364)Online publication date: 1-Dec-2019
        • (2019)Inferring Patterns for Taint-Style Vulnerabilities With Security PatchesIEEE Access10.1109/ACCESS.2019.29115927(52339-52349)Online publication date: 2019
        • (2018)Calling-to-reference context translation via constraint-guided CFL-reachabilityACM SIGPLAN Notices10.1145/3296979.319237853:4(196-210)Online publication date: 11-Jun-2018
        • (2018)Parser combinators for context-free path queryingProceedings of the 9th ACM SIGPLAN International Symposium on Scala10.1145/3241653.3241655(13-23)Online publication date: 17-Sep-2018
        • (2018)Calling-to-reference context translation via constraint-guided CFL-reachabilityProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192378(196-210)Online publication date: 11-Jun-2018
        • (2015)Towards a Scalable Framework for Context-Free Language ReachabilityCompiler Construction10.1007/978-3-662-46663-6_10(193-211)Online publication date: 2015
        • (2024)LibAlchemy: A Two-Layer Persistent Summary Design for Taming Third-Party Libraries in Static Bug-Finding SystemsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639132(1-13)Online publication date: 20-May-2024
        • Show More Cited By

        View Options

        Login options

        View options

        PDF

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        Figures

        Tables

        Media

        Share

        Share

        Share this Publication link

        Share on social media