Abstract
This paper presents a novel technique for type-guided worst-case input generation for functional programs. The technique builds on automatic amortized resource analysis (AARA), a type-based technique for deriving symbolic bounds on the resource usage of functions. Worst-case input generation is performed by an algorithm that takes as input a function, its resource-annotated type derivation in AARA, and a skeleton that describes the shape and size of the input that is to be generated. If successful, the algorithm fills in integers, booleans, and data structures to produce a value of the shape given by the skeleton. The soundness theorem states that the generated value exhibits the highest cost among all arguments of the functions that have the shape of the skeleton. This cost corresponds exactly to the worst-case bound that is established by the type derivation. In this way, a successful completion of the algorithm proves that the bound is tight for inputs of the given shape. Correspondingly, a relative completeness theorem is proved to show that the algorithm succeeds if and only if the derived worst-case bound is tight. The theorem is relative because it depends on a decision procedure for constraint solving. The technical development is presented for a simple first-order language with linear resource bounds. However, the technique scales to and has been implemented for Resource Aware ML, an implementation of AARA for a fragment of OCaml with higher-order functions, user-defined data types, and types for polynomial bounds. Experiments demonstrate that the technique works effectively and can derive worst-case inputs with hundreds of integers for sorting algorithms, operations on search trees, and insertions into hash tables.
Supplemental Material
- E. Albert, P. Arenas, S. Genaim, and G. Puebla. 2011. Closed-Form Upper Bounds in Static Cost Analysis. J. Automated Reasoning 46 (February 2011). Issue 2. Google ScholarDigital Library
- E. Albert, J. C. Fernández, and G. Román-Díez. 2015. Non-cumulative Resource Analysis. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS’15). Google ScholarDigital Library
- R. Atkey. 2010. Amortised Resource Analysis with Separation Logic. In European Symp. on Programming (ESOP’10). Google ScholarDigital Library
- M. Avanzini, U. D. Lago, and G. Moser. 2015. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Int. Conf. on Functional Programming (ICFP’15). Google ScholarDigital Library
- M. Avanzini and G. Moser. 2013. A Combination Framework for Complexity. In Int. Conf. on Rewriting Techniques and Applications (RTA’13).Google Scholar
- R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács. 2010. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning (LPAR’10). Google ScholarDigital Library
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS’14).Google Scholar
- J. Burnim, S. Juvekar, and K. Sen. 2009. WISE: Automated Test Generation for Worst-case Complexity. In Int. Conf. on Softw. Eng. (ICSE’09). Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Op. Syst. Design and Impl. (OSDI’08). Google ScholarDigital Library
- Q. Carbonneaux, J. Hoffmann, T. Reps, and Z. Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verif. (CAV’17).Google Scholar
- Q. Carbonneaux, J. Hoffmann, and Z. Shao. 2015. Compositional Certified Resource Bounds. In Prog. Lang. Design and Impl. (PLDI’15). Google ScholarDigital Library
- S. Chandra, S. J. Fink, and M. Sridharan. 2009. Snugglebug: A Powerful Approach To Weakest Preconditions. In Prog. Lang. Design and Impl. (PLDI’09). Google ScholarDigital Library
- A. Charguéraud and F. Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In Interactive Theorem Proving (ITP’15).Google Scholar
- V. Chipounov, V. Kuznetsov, and G. Candea. 2012. The S2E Platform: Design, Implementation, and Applications. Trans. on Comp. Syst. 30 (February 2012). Issue 1. Google ScholarDigital Library
- E. Çiçek, G. Barthe, M. Gaboardi, D. Garg, and J. Hoffmann. 2017. Relational Cost Analysis. In Princ. of Prog. Lang. (POPL’17). Google ScholarDigital Library
- E. Çiçek, D. Garg, and U. A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP’15).Google Scholar
- K. Claessen and J. Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In Int. Conf. on Functional Programming (ICFP’00). Google ScholarDigital Library
- K. Crary and S. Weirich. 2000. Resource Bound Certification. In Princ. of Prog. Lang. (POPL’00). Google ScholarDigital Library
- S. A. Crosby and D. S. Wallach. 2003. Denial of Service via Algorithmic Complexity Attacks. In USENIX Sec. Symp. (USENIX’03). Google ScholarDigital Library
- N. A. Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Princ. of Prog. Lang. (POPL’08). Google ScholarDigital Library
- N. Danner, D. R. Licata, and R. Ramyaa. 2015. Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP’15). Google ScholarDigital Library
- L. de Moura and N. Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS’08). Google ScholarDigital Library
- P. Dinges and G. Agha. 2014. Targeted Test Input Generation Using Symbolic–Concrete Backward Execution. In Automated Softw. Eng. (ASE’14). Google ScholarDigital Library
- A. Flores-Montoya and R. Hähnle. 2014. Resource Analysis of Complex Programs with Cost Equations. In Asian Symp. on Prog. Lang. and Systems (APLAS’14).Google Scholar
- J. E. Forrester and B. P. Miller. 2000. An Empirical Study of the Robustness of Windows NT Applications Using Random Testing. In USENIX Windows Syst. Symp. (WSS’00). Google ScholarDigital Library
- F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, and J. Giesl. 2016. Lower Runtime Bounds for Integer Programs. In Int. Joint Conf. on Automated Reasoning (IJCAR’16). Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. 2005. DART: Directed Automated Random Testing. In Prog. Lang. Design and Impl. (PLDI’05). Google ScholarDigital Library
- P. Godefroid, M. Levin, and D. Molnar. 2008. Automated Whitebox Fuzz Testing. In Network and Dist. Syst. Security (NDSS’08).Google Scholar
- S. Gulwani. 2009. SPEED: Symbolic Complexity Bound Analysis. In Computer Aided Verif. (CAV’09). Google ScholarDigital Library
- S. Gulwani, K. K. Mehra, and T. M. Chilimbi. 2009. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In Princ. of Prog. Lang. (POPL’09). Google ScholarDigital Library
- R. Harper. 2016. Practical Foundations for Programming Languages. Cambridge University Press. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. 2011. Multivariate Amortized Resource Analysis. In Princ. of Prog. Lang. (POPL’11). Google ScholarDigital Library
- J. Hoffmann, A. Das, and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Princ. of Prog. Lang. (POPL’17). Google ScholarDigital Library
- J. Hoffmann and M. Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP’10). Google ScholarDigital Library
- M. Hofmann and S. Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Princ. of Prog. Lang. (POPL’03). Google ScholarDigital Library
- M. Hofmann and G. Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA’15).Google Scholar
- S. Jost, K. Hammond, H.-W. Loidl, and M. Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In Princ. of Prog. Lang. (POPL’10). Google ScholarDigital Library
- S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. 2009. Carbon Credits for Resource-Bounded Computations using Amortised Analysis. In Symp. on Form. Meth. (FM’09). Google ScholarDigital Library
- Z. Kincaid, J. Breck, A. F. Boroujeni, and T. Reps. 2017. Compositional Recurrence Analysis Revisited. In Prog. Lang. Design and Impl. (PLDI’17). Google ScholarDigital Library
- U. D. Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS’11).Google Scholar
- U. D. Lago and B. Petit. 2013. The Geometry of Types. In Princ. of Prog. Lang. (POPL’13). Google ScholarDigital Library
- L. Lampropoulos, Z. Paraskevopoulou, and B. C. Pierce. 2018. Generating Good Generators for Inductive Relations. In Princ. of Prog. Lang. (POPL’18). Google ScholarDigital Library
- K. Luckow, R. Kersten, and C. Păsăreanu. 2017. Symbolic Complexity Analysis Using Context-Preserving Histories. In Int. Conf. on Softw. Testing, Verif. and Validation (ICST’17).Google Scholar
- K.-K. Ma, K. Y. Phang, J. S. Foster, and M. Hicks. 2011. Directed symbolic execution. In Static Analysis Symp. (SAS’11). Google ScholarDigital Library
- M. D. McIlroy. 1999. A Killer Adversary for Quicksort. J. Softw.-Practice & Experience 29 (April 1999). Issue 4. Google ScholarDigital Library
- V. C. Ngo, Mario Dehesa-Azuara, M. Fredrikson, and J. Hoffmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP’17).Google Scholar
- T. Nipkow. 2015. Amortized Complexity Verified. In Interactive Theorem Proving (ITP’15).Google Scholar
- Y. Noller, R. Kersten, and C. S. Păsăreanu. 2018. Badger: Complexity Analysis with Fuzzing and Symbolic Execution. In Int. Symp. on Softw. Testing and Analysis (ISSTA’18). Google ScholarDigital Library
- L. Noschinski, F. Emmes, and J. Giesl. 2013. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Automated Reasoning 51 (June 2013). Issue 1.Google Scholar
- T. Petsios, J. Zhao, A. D. Keromytis, and S. Jana. 2017. SlowFuzz: Automated Domain-Independent Detection of Algorithmic Complexity Vulnerabilities. In Conf. on Comp. and Comm. Sec. (CCS’17). Google ScholarDigital Library
- C. Runciman, M. Naylor, and F. Lindblad. 2008. Smallcheck and Lazy Smallcheck: Automatic Exhaustive Testing for Small Vaues. In Symp. on Haskell (Haskell’08). Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. 2005. CUTE: A Concolic Unit Testing Engine for C. In Found. of Softw. Eng. (FSE’05). Google ScholarDigital Library
- H. R. Simões, P. B. Vasconcelos, M. Florido, S. Jost, and K. Hammond. 2012. Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. In Int. Conf. on Functional Programming (ICFP’12). Google ScholarDigital Library
- M. Sinn, F. Zuleger, and H. Veith. 2014. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verif. (CAV’14). Google ScholarDigital Library
- R. E. Tarjan. 1985. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods 6 (August 1985). Issue 2.Google Scholar
- P. B. Vasconcelos. 2008. Space Cost Analysis Using Sized Types. Ph.D. Dissertation. School of Computer Science, University of St Andrews.Google Scholar
- P. B. Vasconcelos, S. Jost, M. Florido, and K. Hammond. 2015. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In European Symp. on Programming (ESOP’15).Google Scholar
- D. Walker. 2002. Substructural Type Systems. In Advanced Topics in Types and Programming Languages. MIT Press.Google Scholar
- D. Wang and J. Hoffmann. 2018. Type-Guided Worst-Case Input Generation. Available on https://www.cs.cmu.edu/~diw3/ papers/WangH18.pdf .Google Scholar
- P. Wang, D. Wang, and A. Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In Object-Oriented Prog., Syst., Lang., and Applications (OOPSLA’17). Google ScholarDigital Library
- Website. 2011. CVE - CVE-2011-4885. Available on: https://cve.mitre.org/cgi- bin/cvename.cgi?name=CVE- 2011- 4885 .Google Scholar
- Website. 2012a. PHP 5.3.8 - Hashtables Denial of Service. Available on https://www.exploit- db.com/exploits/18296/ .Google Scholar
- Website. 2012b. PHP: PHP 5 ChangeLog. Available on http://www.php.net/ChangeLog- 5.php#5.3.9 .Google Scholar
- Website. 2015. Space/Time Analysis for Cybersecurity (STAC). Available on https://www.darpa.mil/program/ space- time- analysis- for- cybersecurity .Google Scholar
- H. Xi. 2002. Dependent Types for Program Termination Verification. J. Higher-Order and Symbolic Comp. 15 (2002). Issue 1. Google ScholarDigital Library
- Y. Zhang, Z. Chen, J. Wang, W. Dong, and Z. Liu. 2015. Regular Property Guided Dynamic Symbolic Execution. In Int. Conf. on Softw. Eng. (ICSE’15). Google ScholarDigital Library
- F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. 2011. Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS’11). Google ScholarDigital Library
Index Terms
- Type-guided worst-case input generation
Recommendations
Towards automatic resource bound analysis for OCaml
POPL '17This article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and ...
Towards automatic resource bound analysis for OCaml
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesThis article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and ...
Non-polynomial Worst-Case Analysis of Recursive Programs
We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we ...
Comments