Document Open Access Logo

Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates

Authors John Toman, Dan Grossman

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.24.pdf
  • Filesize: 0.83 MB
  • 32 pages

Document Identifiers

Author Details

John Toman
  • Paul G. Allen School of Computer Science & Engineering, University of Washington, USA
Dan Grossman
  • Paul G. Allen School of Computer Science & Engineering, University of Washington, USA

Funding

This paper is based upon work sponsored in part by DARPA under agreement number FA8750-16-2-0032.

Cite As Get BibTex

John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 24:1-24:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ECOOP.2018.24

Abstract

Modern software increasingly relies on external resources whose location or content can change during program execution. Examples of such resources include remote network hosts, database entries, dynamically updated configuration options, etc. Long running, adaptable programs must handle these changes gracefully and correctly. Dealing with all possible resource update scenarios is difficult to get right, especially if, as is common, external resources can be modified without prior warning by code and/or users outside of the application's direct control. If a resource unexpectedly changes during a computation, an application may observe multiple, inconsistent states of the resource, leading to incorrect program behavior.
This paper presents a sound and precise static analysis, Legato, that verifies programs correctly handle changes in external resources. Our analysis ensures that every value computed by an application reflects a single, consistent version of every external resource's state. Although consistent computation in the presence of concurrent resource updates is fundamentally a concurrency issue, our analysis relies on the novel at-most-once condition to avoid explicitly reasoning about concurrency. The at-most-once condition requires that all values depend on at most one access of each resource. Our analysis is flow-, field-, and context-sensitive. It scales to real-world Java programs while producing a moderate number of false positives. We applied Legato to 10 applications with dynamically updated configurations, and found several non-trivial consistency bugs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automated static analysis
Keywords
  • Static Analysis
  • Dynamic Configuration Updates

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Peter Bailis, Alan Fekete, Michael J Franklin, Ali Ghodsi, Joseph M Hellerstein, and Ion Stoica. Coordination avoidance in database systems. Proceedings of the VLDB Endowment, 8(3), 2014. Google Scholar
  2. Paulo Barros, Suzanne Just, Renéand Millstein, Paul Vines, Werner Dietl, and Michael D Ernst. Static analysis of implicit control flow: Resolving java reflection and android intents. In ASE, 2015. Google Scholar
  3. Tom Bergan, Dan Grossman, and Luis Ceze. Symbolic execution of multithreaded programs from arbitrary program contexts. In OOPSLA, 2014. Google Scholar
  4. Arthur J Bernstein, Philip M Lewis, and Shiyong Lu. Semantic conditions for correctness at different isolation levels. In Data Engineering, 2000. Google Scholar
  5. Philip A Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency control and recovery in database systems. Addison-Wesley Pub. Co. Inc., Reading, MA, 1987. Google Scholar
  6. Matt Bishop and Michael Dilger. Checking for race conditions in file accesses. Computing systems, 2(2), 1996. Google Scholar
  7. Eric Bodden. Inter-procedural data-flow analysis with ifds/ide and soot. In State of the Art in Java Program analysis, 2012. Google Scholar
  8. Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira. Ownership types for object encapsulation. In POPL, 2003. Google Scholar
  9. Xiang Cai, Rucha Lale, Xincheng Zhang, and Robert Johnson. Fixing races for good: Portable and reliable unix file-system race detection. In Information, Computer and Communications Security, 2015. Google Scholar
  10. Sagar Chaki, Edmund Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, and Karen Yorav. Efficient verification of sequential and concurrent c programs. Formal Methods in System Design, 25(2-3):129-166, 2004. Google Scholar
  11. Sagar Chaki, Edmund Clarke, Nicholas Kidd, Thomas Reps, and Tayssir Touili. Verifying concurrent message-passing c programs with recursive calls. In TACAS, 2006. Google Scholar
  12. Manuvir Das, Sorin Lerner, and Mark Seigle. Esp: Path-sensitive program verification in polynomial time. In PLDI, 2002. Google Scholar
  13. Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In PLDI, 2001. Google Scholar
  14. Robert DeLine and Manuel Fähndrich. Typestates for objects. In ECOOP, 2004. Google Scholar
  15. Alain Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In PLDI, 1994. Google Scholar
  16. William Enck, Peter Gilbert, Seungyeop Han, Vasant Tendulkar, Byung-Gon Chun, Landon P Cox, Jaeyeon Jung, Patrick McDaniel, and Anmol N Sheth. Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. TOCS, 32(2), 2014. Google Scholar
  17. Stephen J Fink, Eran Yahav, Nurit Dor, G Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. TOSEM, 17(2), 2008. Google Scholar
  18. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1), 1987. Google Scholar
  19. Neil D. Jones and Steven S. Muchnick. Flow analysis and optimization of lisp-like structures. In POPL, 1979. Google Scholar
  20. Matthias L. Jugel. Personal Communication, 2017. Google Scholar
  21. Uday P Khedker, Amitabha Sanyal, and Amey Karkare. Heap reference analysis using access graphs. TOPLAS, 30(1), 2007. Google Scholar
  22. Dave King, Boniface Hicks, Michael Hicks, and Trent Jaeger. Implicit flows: Can’t live with ‘em, can’t live without ‘em. In Information Systems Security, 2008. Google Scholar
  23. Johannes Lerch, Johannes Späth, Eric Bodden, and Mira Mezini. Access-path abstraction: Scaling field-sensitive data-flow analysis with unbounded access paths. In ASE, 2015. Google Scholar
  24. Max Lillack, Christian Kästner, and Eric Bodden. Tracking load-time configuration options. In ASE, 2014. Google Scholar
  25. Yu Lin. Automated refactoring for Java concurrency. PhD thesis, University of Illinois at Urbana-Champaign, 2015. Google Scholar
  26. Mario Linares-Vásquez, Boyang Li, Christopher Vendome, and Denys Poshyvanyk. Documenting database usages and schema constraints in database-centric applications. In ISSTA, 2016. Google Scholar
  27. Peng Liu, Omer Tripp, and Xiangyu Zhang. Flint: fixing linearizability violations. In OOPLSA, 2014. Google Scholar
  28. Ben Livshits. Standford securibench suite. http://suif.stanford.edu/~livshits/securibench/, 2017.
  29. Benjamin Livshits. Improving software security with precise static and runtime analysis. PhD thesis, Stanford University, 2006. Google Scholar
  30. Andy Maule, Wolfgang Emmerich, and David S Rosenblum. Impact analysis of database schema changes. In ICSE, 2008. Google Scholar
  31. William S. McPhee. Operating system integrity in os/vs2. IBM Systems Journal, 13(3), 1974. Google Scholar
  32. Rajiv Mordani and Shing Wai Chan. Java servlet specification, 2009. Google Scholar
  33. Sarah Nadi, Thorsten Berger, Christian Kästner, and Krzysztof Czarnecki. Mining configuration constraints: Static analyses and empirical results. In ICSE, 2014. Google Scholar
  34. Nomair A. Naeem and Ondrej Lhotak. Typestate-like analysis of multiple interacting objects. In OOPSLA, 2008. Google Scholar
  35. Mayur Hiru Naik. Effective Static Race Detection For Java. PhD thesis, Stanford, 2008. Google Scholar
  36. Mathias Payer and Thomas R. Gross. Protecting applications against tocttou races by user-space caching of file metadata. In VEE, 2012. Google Scholar
  37. Dong Qiu, Bixin Li, and Zhendong Su. An empirical analysis of the co-evolution of schema and code in database applications. In FSE, 2013. Google Scholar
  38. Ariel Rabkin and Randy Katz. Static extraction of program configuration options. In ICSE, 2011. Google Scholar
  39. Elnatan Reisner, Charles Song, Kin-Keung Ma, Jeffrey S Foster, and Adam Porter. Using symbolic evaluation to understand behavior in configurable software systems. In ICSE, 2010. Google Scholar
  40. Mooly Sagiv, Thomas Reps, and Susan Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci., 167(1-2), 1996. Google Scholar
  41. Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. Boomerang: Demand-driven flow-and context-sensitive pointer analysis for java. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming (ECOOP 2016), volume 56 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:26, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2016/6116, URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.22.
  42. Robert E Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12, 1986. Google Scholar
  43. John Toman and Dan Grossman. Staccato: A Bug Finder for Dynamic Configuration Updates. In ECOOP, 2016. Google Scholar
  44. Emina Torlak and Satish Chandra. Effective interprocedural resource leak detection. In ICSE, 2010. Google Scholar
  45. Jesse A. Tov and Riccardo Pucella. Practical affine types. In POPL, 2011. Google Scholar
  46. Omer Tripp, Marco Pistoia, Stephen J. Fink, Manu Sridharan, and Omri Weisman. Taj: Effective taint analysis of web applications. In PLDI, 2009. Google Scholar
  47. Raja Vallée-Rai, Etienne Gagnon, Laurie Hendren, Patrick Lam, Patrice Pominville, and Vijay Sundaresan. Optimizing java bytecode using the soot framework: Is it feasible? In Compiler Construction, 2000. Google Scholar
  48. David Van Horn and Matthew Might. Abstracting abstract machines. In ICFP, 2010. Google Scholar
  49. Philip Wadler. Linear types can change the world. In IFIP TC, 1990. Google Scholar
  50. Daniel M Yellin and Robert E Strom. Protocol specifications and component adaptors. TOPLAS, 19(2), 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact