[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3377811.3380346acmconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
research-article

Conquering the extensional scalability problem for value-flow analysis frameworks

Published: 01 October 2020 Publication History

Abstract

Modern static analyzers often need to simultaneously check a few dozen or even hundreds of value-flow properties, causing serious scalability issues when high precision is required. A major factor to this deficiency, as we observe, is that the core static analysis engine is oblivious of the mutual synergy among the properties being checked, thus inevitably losing many optimization opportunities. Our work is to leverage the inter-property awareness and to capture redundancies and inconsistencies when many properties are considered at the same time. We have evaluated our approach by checking twenty value-flow properties in standard benchmark programs and ten real-world software systems. The results demonstrate that our approach is more than 8× faster than existing ones but consumes only 1/7 of the memory. Such substantial improvement in analysis efficiency is not achieved by sacrificing the effectiveness: at the time of writing, thirty-nine bugs found by our approach have been fixed by developers and four of them have been assigned CVE IDs due to their security impact.

References

[1]
Sven Apel, Dirk Beyer, Vitaly Mordan, Vadim Mutilin, and Andreas Stahlbauer. 2016. On-the-fly decomposition of specifications in software model checking. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, 349--361.
[2]
Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. 2014. Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14). ACM, 259--269.
[3]
Pavel Avgustinov, Oege de Moor, Michael Peyton Jones, and Max Schäfer. 2016. QL: Object-oriented Queries on Relational Data. In 30th European Conference on Object-Oriented Programming (ECOOP '16). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2:1--2:25.
[4]
Domagoj Babic and Alan J. Hu. 2008. Calysto: Scalable and precise extended static checking. In Proceedings of the 30th International Conference on Software Engineering (ICSE '08). IEEE, 211--220.
[5]
Thomas Ball and Sriram K. Rajamani. 2002. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '02). ACM, 1--3.
[6]
Paul Beanie, Henry Kautz, and Ashish Sabharwal. 2003. Understanding the power of clause learning. In Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI '03). Morgan Kaufmann Publishers Inc., 1194--1201.
[7]
Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. 2010. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 2 (2010), 66--75.
[8]
Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly declarative specification of sophisticated points-to analyses. In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA '09). ACM, 243--262.
[9]
Gianpiero Cabodi and Sergio Nocco. 2011. Optimized model checking of multiple properties. In 2011 Design, Automation, and Test in Europe Conference (DATE '11). IEEE, 1--4.
[10]
P Camurati, C Loiacono, P Pasini, D Patti, and S Quer. 2014. To split or to group: from divide-and-conquer to sub-task sharing in verifying multiple properties. In International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), Lausanne, Switzerland. Springer, 313--325.
[11]
Sagar Chaki, Edmund M Clarke, Alex Groce, Somesh Jha, and Helmut Veith. 2004. Modular verification of software components in C. IEEE Transactions on Software Engineering 30, 6 (2004), 388--402.
[12]
Sigmund Cherem, Lonnie Princehouse, and Radu Rugina. 2007. Practical memory leak detection using guarded value-flow analysis. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '07). ACM, 480--491.
[13]
Chia Yuan Cho, Vijay D'Silva, and Dawn Song. 2013. BLITZ: Compositional bounded model checking for real-world programs. In Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE '13). IEEE, 136--146.
[14]
Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. 2010. Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Transactions on Computational Logic (TOCL) 12, 1 (2010), 7.
[15]
Edmund Clarke, Daniel Kroening, and Karen Yorav. 2003. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of the 40th annual Design Automation Conference. ACM, 368--371.
[16]
Patrick Cousot and Radhia Cousot. 2002. Modular static program analysis. In International Conference on Compiler Construction (CC '02). Springer, 159--179.
[17]
Ron Cytron, Jeanne Ferrante, Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1991. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems (TOPLAS) 13, 4 (1991), 451--490.
[18]
Manuvir Das, Sorin Lerner, and Mark Seigle. 2002. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI '02). ACM, 57--68.
[19]
Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337--340.
[20]
Jeffrey Dean, David Grove, and Craig Chambers. 1995. Optimization of object-oriented programs using static class hierarchy analysis. In European Conference on Object-Oriented Programming. Springer, 77--101.
[21]
Dorothy E. Denning. 1976. A lattice model of secure information flow. Commun. ACM 19, 5 (1976), 236--243.
[22]
Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. 2006. A scalable algorithm for minimal unsatisfiable core extraction. In Theory and Applications of Satisfiability Testing (SAT '06). Springer, 36--41.
[23]
Isil Dillig, Thomas Dillig, and Alex Aiken. 2008. Sound, complete and scalable path-sensitive analysis. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '08). ACM, 270--280.
[24]
Isil Dillig, Thomas Dillig, Alex Aiken, and Mooly Sagiv. 2011. Precise and compact modular procedure summaries for heap manipulating programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11). ACM, 567--577.
[25]
Gang Fan, Rongxin Wu, Qingkai Shi, Xiao Xiao, Jinguo Zhou, and Charles Zhang. 2019. Smoke: scalable path-sensitive memory leak detection for millions of lines of code. In Proceedings of the 41st ACM/IEEE International Conference on Software Engineering (ICSE '19). IEEE, 72--82.
[26]
Eugene Goldberg, Matthias Güdemann, Daniel Kroening, and Rajdeep Mukherjee. 2018. Efficient verification of multi-property designs (The benefit of wrong assumptions). In 2018 Design, Automation, and Test in Europe Conference (DATE '18). IEEE, 43--48.
[27]
James C King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385--394.
[28]
Wei Le and Mary Lou Soffa. 2008. Marple: a demand-driven path-sensitive buffer overflow detector. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering. ACM, 272--282.
[29]
Lian Li, Cristina Cifuentes, and Nathan Keynes. 2011. Boosting the Performance of Flow-sensitive Points-to Analysis Using Value Flow. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (ESEC/FSE '11). ACM, 343--353.
[30]
Benjamin Livshits and Monica S Lam. 2003. Tracking pointers with path and context sensitivity for bug detection in C programs. In Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE '11). ACM, 317--326.
[31]
Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z Guyer, Uday P Khedker, Anders Møller, and Dimitrios Vardoulakis. 2015. In defense of soundiness: a manifesto. Commun. ACM 58, 2 (2015), 44--46.
[32]
Scott McPeak, Charles-Henri Gros, and Murali Krishna Ramanathan. 2013. Scalable and incremental software bug detection. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE '13). ACM, 554--564.
[33]
Vitaly O Mordan and Vadim S Mutilin. 2016. Checking several requirements at once by CEGAR. Programming and Computer Software 42, 4 (2016), 225--238.
[34]
Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '95). ACM, 49--61.
[35]
Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, and Ciera Jaspan. 2018. Lessons from building static analysis tools at Google. Commun. ACM 61, 4 (2018), 58--66.
[36]
Caitlin Sadowski, Jeffrey Van Gogh, Ciera Jaspan, Emma Söderberg, and Collin Winter. 2015. Tricorder: Building a program analysis ecosystem. In Proceedings of the 37th International Conference on Software Engineering (ICSE '15). IEEE, 598--608.
[37]
Qingkai Shi, Rongxin Wu, Gang Fan, and Charles Zhang. 2019. Conquering the Extensional Scalability Problem for Value-Flow Analysis Frameworks. arXiv preprint arXiv:1912.06878 (2019).
[38]
Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. 2018. Pinpoint: Fast and precise sparse value flow analysis for million lines of code. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '18). ACM, 693--706.
[39]
Robert E. Strom. 1983. Mechanisms for Compile-time Enforcement of Security. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '83). ACM, 276--284.
[40]
Robert E Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering SE-12, 1 (1986), 157--171.
[41]
Yulei Sui and Jingling Xue. 2016. SVF: Interprocedural static value-flow analysis in LLVM. In International Conference on Compiler Construction (CC '16). ACM, 265--266.
[42]
Yulei Sui, Ding Ye, and Jingling Xue. 2014. Detecting memory leaks statically with full-sparse value-flow analysis. IEEE Transactions on Software Engineering 40, 2 (2014), 107--122.
[43]
Omer Tripp, Marco Pistoia, Patrick Cousot, Radhia Cousot, and Salvatore Guarnieri. 2013. Andromeda: Accurate and scalable security analysis of web applications. In International Conference on Fundamental Approaches to Software Engineering. Springer, 210--225.
[44]
Yichen Xie and Alex Aiken. 2005. Context- and path-sensitive memory leak detection. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE '05). ACM, 115--125.
[45]
Yichen Xie and Alex Aiken. 2005. Scalable error detection using Boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05). ACM, 351--363.
[46]
Hua Yan, Yulei Sui, Shiping Chen, and Jingling Xue. 2018. Spatio-temporal context reduction: a pointer-analysis-based static approach for detecting use-after-free vulnerabilities. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE '18). IEEE, 327--337.

Cited By

View all
  • (2024)SPATA: Effective OS Bug Detection with Summary-Based, Alias-Aware, and Path-Sensitive Typestate AnalysisACM Transactions on Computer Systems10.1145/369525042:3-4(1-40)Online publication date: 6-Sep-2024
  • (2024)Automatically Inspecting Thousands of Static Bug Warnings with Large Language Model: How Far Are We?ACM Transactions on Knowledge Discovery from Data10.1145/365371818:7(1-34)Online publication date: 19-Jun-2024
  • (2024)Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingProceedings of the ACM on Software Engineering10.1145/36437491:FSE(494-516)Online publication date: 12-Jul-2024
  • Show More Cited By

Index Terms

  1. Conquering the extensional scalability problem for value-flow analysis frameworks

    Recommendations

    Comments

    Please enable JavaScript to view thecomments powered by Disqus.

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    ICSE '20: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering
    June 2020
    1640 pages
    ISBN:9781450371216
    DOI:10.1145/3377811
    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]

    Sponsors

    In-Cooperation

    • KIISE: Korean Institute of Information Scientists and Engineers
    • IEEE CS

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 01 October 2020

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. compositional program analysis
    2. demand-driven analysis
    3. static bug finding
    4. value-flow analysis

    Qualifiers

    • Research-article

    Funding Sources

    • Hong Kong
    • MSRA

    Conference

    ICSE '20
    Sponsor:

    Acceptance Rates

    Overall Acceptance Rate 276 of 1,856 submissions, 15%

    Upcoming Conference

    ICSE 2025

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)26
    • Downloads (Last 6 weeks)2
    Reflects downloads up to 13 Dec 2024

    Other Metrics

    Citations

    Cited By

    View all
    • (2024)SPATA: Effective OS Bug Detection with Summary-Based, Alias-Aware, and Path-Sensitive Typestate AnalysisACM Transactions on Computer Systems10.1145/369525042:3-4(1-40)Online publication date: 6-Sep-2024
    • (2024)Automatically Inspecting Thousands of Static Bug Warnings with Large Language Model: How Far Are We?ACM Transactions on Knowledge Discovery from Data10.1145/365371818:7(1-34)Online publication date: 19-Jun-2024
    • (2024)Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingProceedings of the ACM on Software Engineering10.1145/36437491:FSE(494-516)Online publication date: 12-Jul-2024
    • (2024) Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path ConditionsACM Transactions on Software Engineering and Methodology10.1145/363274333:3(1-33)Online publication date: 24-Jan-2024
    • (2023)Place your locks wellProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620446(3727-3744)Online publication date: 9-Aug-2023
    • (2023) Anchor: Fast and Precise Value-flow Analysis for Containers via Memory OrientationACM Transactions on Software Engineering and Methodology10.1145/356580032:3(1-39)Online publication date: 26-Apr-2023
    • (2023)Optimize value-flow analysis based static vulnerability detection by solver ratingInternational Conference on Computer Network Security and Software Engineering (CNSSE 2023)10.1117/12.2683173(15)Online publication date: 26-Jun-2023
    • (2023)VALAR: Streamlining Alarm Ranking in Static Analysis with Value-Flow Assisted Active Learning2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00098(1940-1951)Online publication date: 11-Sep-2023
    • (2022)Fast and precise application code analysis using a partial libraryProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510046(934-945)Online publication date: 21-May-2022
    • (2022)Path-sensitive and alias-aware typestate analysis for detecting OS bugsProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507770(859-872)Online publication date: 28-Feb-2022
    • 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

    Media

    Figures

    Other

    Tables

    Share

    Share

    Share this Publication link

    Share on social media