Document Open Access Logo

Lifestate: Event-Driven Protocols and Callback Control Flow

Authors Shawn Meier , Sergio Mover , Bor-Yuh Evan Chang

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2019.1.pdf
  • Filesize: 0.9 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
Keywords
  • event-driven systems
  • application-programming protocols
  • application framework interfaces
  • callbacks
  • sound framework modeling
  • predictive dynamic verification

Metrics

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

Abstract

Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid. What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order. In this paper, we tackle the problem of specifying and modeling event-driven application-programming protocols. In particular, we formalize a core meta-model that captures the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules. To evaluate the effectiveness of lifestate modeling, we provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.

Cite As Get BibTex

Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 1:1-1:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ECOOP.2019.1

Author Details

Shawn Meier
  • University of Colorado Boulder, USA
Sergio Mover
  • École Polytechnique, Institute Polytechnique de Paris, Palaiseau, France
Bor-Yuh Evan Chang
  • University of Colorado Boulder, USA

Funding

This material is based on research sponsored by DARPA under agreement number FA8750-14-2-0263.

Acknowledgements

Many thanks to Edmund S. L. Lam, Chance Roberts, and Chou Yi for help in gathering traces, as well as Alberto Griggio for a convenient tool for running tests. We also thank Aleksandar Chakarov, Maxwell Russek, the Fixr Team, and the University of Colorado Programming Languages and Verification (CUPLV) Group for insightful discussions, as well as the anonymous reviewers for their helpful comments.

Supplementary Materials

References

  1. Android Developers. The Activity Lifecycle. https://developer.android.com/guide/components/activities/activity-lifecycle.html, 2018.
  2. Android Developers. UI/Application exerciser monkey. https://developer.android.com/studio/test/monkey.html, 2018.
  3. Android Topeka. Crash if rotate device right after press floating action button #4 Topeka for Android. https://github.com/googlesamples/android-topeka/issues/4, 2015.
  4. Yauhen Leanidavich Arnatovich, Minh Ngoc Ngo, Hee Beng Kuan Tan, and Charlie Soh. Achieving High Code Coverage in Android UI Testing via Automated Widget Exercising. In Asia-Pacific Software Engineering Conference (APSEC), 2016. URL: http://dx.doi.org/10.1109/APSEC.2016.036.
  5. Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. FlowDroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In Programming Language Design and Implementation (PLDI), 2014. URL: http://dx.doi.org/10.1145/2594291.2594299.
  6. Osbert Bastani, Saswat Anand, and Alex Aiken. Specification Inference Using Context-Free Language Reachability. In Principles of Programming Languages (POPL), 2015. URL: http://dx.doi.org/10.1145/2676726.2676977.
  7. Pavol Bielik, Veselin Raychev, and Martin T. Vechev. Scalable race detection for Android applications. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2015. URL: http://dx.doi.org/10.1145/2814270.2814303.
  8. Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. Selective control-flow abstraction via jumping. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2015. URL: http://dx.doi.org/10.1145/2814270.2814293.
  9. Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang. Droidel: A general approach to Android framework modeling. In State of the Art in Program Analysis (SOAP), 2015. URL: http://dx.doi.org/10.1145/2771284.2771288.
  10. Chris Boyle. Simon Tatham’s Puzzles. https://github.com/chrisboyle/sgtpuzzles/blob/658f00f19172bdbceb5329bc77376b40fe550fcb/app/src/main/java/name/boyle/chris/sgtpuzzles/GamePlay.java#L183, 2014.
  11. Yinzhi Cao, Yanick Fratantonio, Antonio Bianchi, Manuel Egele, Christopher Kruegel, Giovanni Vigna, and Yan Chen. EdgeMiner: Automatically detecting implicit control flow transitions through the Android framework. In Network and Distributed System Security (NDSS), 2015. URL: https://www.ndss-symposium.org/ndss2015/edgeminer-automatically-detecting-implicit-control-flow-transitions-through-android-framework.
  12. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv Symbolic Model Checker. In Computer-Aided Verification (CAV), 2014. URL: http://dx.doi.org/10.1007/978-3-319-08867-9_22.
  13. Adrian Chifor. Swiftnotes. https://f-droid.org/en/packages/com.moonpi.swiftnotes/, 2015.
  14. D120. Kistenstapeln. https://github.com/d120/Kistenstapeln-Android, 2015.
  15. Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram K. Rajamani, and Damien Zufferey. P: safe asynchronous event-driven programming. In Programming Language Design and Implementation (PLDI), 2013. URL: http://dx.doi.org/10.1145/2491956.2462184.
  16. Martin Fietz. FeedRemover: already running - issue #1304 - AntennaPod/AntennaPod. https://github.com/AntennaPod/AntennaPod/issues/1304, 2015.
  17. Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol., 17(2), 2008. URL: http://dx.doi.org/10.1145/1348250.1348255.
  18. Jeffrey Fischer, Rupak Majumdar, and Todd D. Millstein. Tasks: language support for event-driven programming. In Partial Evaluation and Program Manipulation (PEPM), 2007. URL: http://dx.doi.org/10.1145/1244381.1244403.
  19. Adam P. Fuchs, Avik Chaudhuri, and Jeffrey S. Foster. SCanDroid: Automated security certification of Android applications. Technical Report CS-TR-4991, University of Maryland, College Park, 2009. Google Scholar
  20. Marko Gargenta. Yamba. https://github.com/learning-android/Yamba/blob/429e37365f35ac4e5419884ef88b6fa378c023f8/src/com/marakana/android/yamba/StatusFragment.java, 2014.
  21. Marko Gargenta and Masumi Nakamura. Learning Android. O'Reilly Media, 2014. Google Scholar
  22. Nicolas Guillaumin. OSMTracker for Android. https://github.com/nguillaumin/osmtracker-android/blob/d80dea16e456defe5ab62ed8b5bc35ede363415e/app/src/main/java/me/guillaumin/android/osmtracker/gpx/ExportTrackTask.java, 2015.
  23. Chun-Hung Hsiao, Cristiano Pereira, Jie Yu, Gilles Pokam, Satish Narayanasamy, Peter M. Chen, Ziyun Kong, and Jason Flinn. Race detection for event-driven mobile applications. In Programming Language Design and Implementation (PLDI), 2014. URL: http://dx.doi.org/10.1145/2594291.2594330.
  24. Jinseong Jeon, Kristopher K. Micinski, and Jeffrey S. Foster. SymDroid: Symbolic execution for Dalvik bytecode. Technical report, Department of Computer Science, University of Maryland, College Park, 2012. Google Scholar
  25. Jinseong Jeon, Xiaokang Qiu, Jonathan Fetter-Degges, Jeffrey S. Foster, and Armando Solar-Lezama. Synthesizing framework models for symbolic execution. In International Conference on Software Engineering (ICSE), 2016. URL: http://dx.doi.org/10.1145/2884781.2884856.
  26. Pallavi Joshi and Koushik Sen. Predictive Typestate Checking of Multithreaded Java Programs. In Automated Software Engineering (ASE), 2008. URL: http://dx.doi.org/10.1109/ASE.2008.39.
  27. Vladislav Kaplun. Update RequestAsyncTask.java by kaplad - Pull Request #315 - facebook/facebook-android-sdk. https://github.com/facebook/facebook-android-sdk/pull/315, 2014.
  28. Maria Kechagia and Diomidis Spinellis. Undocumented and unchecked: exceptions that spell trouble. In Mining Software Repositories, (MSR), 2014. URL: http://dx.doi.org/10.1145/2597073.2597089.
  29. Jinyung Kim, Yongho Yoon, Kwangkeun Yi, and Junbum Shin. SCANDAL: Static analyzer for detecting privacy leaks in Android applications. IEEE Mobile Security Technologies (MoST)., 2017. Google Scholar
  30. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4), 2006. URL: http://dx.doi.org/10.1007/s10990-006-0480-6.
  31. Pallavi Maiya, Rahul Gupta, Aditya Kanade, and Rupak Majumdar. Partial Order Reduction for Event-Driven Multi-threaded Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016. URL: http://dx.doi.org/10.1007/978-3-662-49674-9_44.
  32. Pallavi Maiya, Aditya Kanade, and Rupak Majumdar. Race detection for Android applications. In Programming Language Design and Implementation (PLDI), 2014. URL: http://dx.doi.org/10.1145/2594291.2594311.
  33. Shawn Meier, Sergio Mover, and Bor-Yuh Evan Chang. Lifestate: Event-Driven Protocols and Callback Control Flow (Extended Version). CoRR, abs/, 2019. URL: http://arxiv.org/abs/1906.04924.
  34. Nomair A. Naeem and Ondrej Lhoták. Typestate-like analysis of multiple interacting objects. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). ACM, 2008. URL: http://dx.doi.org/10.1145/1449764.1449792.
  35. NextGis. NextGisLogger. https://github.com/nextgis/nextgislogger, 2017.
  36. OneBusAway. IllegalStateException: Fragment BaseMapFragment not attached to Activity #570 OneBusAway. https://github.com/OneBusAway/onebusaway-android/issues/570, 2016.
  37. Danilo Dominguez Perez and Wei Le. Predicate callback summaries. In International Conference on Software Engineering (ICSE), 2017. URL: http://dx.doi.org/10.1109/ICSE-C.2017.95.
  38. PingPlusPlus. Ping Plus Plus. https://github.com/PingPlusPlus/pingpp-android, 2017.
  39. Steve Pomeroy. The Complete Android Activity/Fragment Lifecycle v0.9.0. https://github.com/xxv/android-lifecycle, 2014.
  40. Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripada, Damien Zufferey, Bor-Yuh Evan Chang, and Pavol Cerný. DroidStar: callback typestates for Android classes. In International Conference on Software Engineering (ICSE), 2018. URL: http://dx.doi.org/10.1145/3180155.3180232.
  41. Red Reader. Crash during commenting #467 RedReader. https://github.com/QuantumBadger/RedReader/issues/467, 2017.
  42. A. Rountev, D. Yan, S. Yang, H. Wu, Y. Wang, and H. Zhang. GATOR: Program analysis toolkit for Android. http://web.cse.ohio-state.edu/presto/software/, 2017.
  43. Atanas Rountev and Dacong Yan. Static Reference Analysis for GUI Objects in Android Software. In Code Generation and Optimization (CGO), 2014. URL: http://dx.doi.org/10.1145/2544137.2544159.
  44. sh1ro. NovelDroid. https://github.com/sh1r0/NovelDroid/blob/f3245055d7a8bcc69a9bca278fbe890081dac58a/app/src/main/java/com/sh1r0/noveldroid/SettingsFragment.java, 2016.
  45. Eric Smith and Alessandro Coglio. Android platform modeling and Android app verification in the ACL2 theorem prover. In Verified Software: Theories, Tools, and Experiments (VSTTE), 2015. URL: http://dx.doi.org/10.1007/978-3-319-29613-5_11.
  46. StackOverflow Post. Got exception: fragment already active. https://stackoverflow.com/questions/10364478/got-exception-fragment-already-active, 2012.
  47. StackOverflow Post. Alertdialog creating exception in android. https://stackoverflow.com/questions/15104677/alertdialog-creating-exception-in-android, 2013.
  48. StackOverflow Post. OnClickListener fired after onPause? https://stackoverflow.com/questions/31432014/onclicklistener-fired-after-onpause, 2015.
  49. StackOverflow Post. Android: click event after Activity.onPause(). https://stackoverflow.com/questions/38368391/android-click-event-after-activity-onpause, 2016.
  50. Robert E. Strom and Shaula Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Trans. Software Eng., 12(1), 1986. Google Scholar
  51. Matthias Urhahn. AudioBug. https://github.com/d4rken/audiobug, 2017.
  52. Yan Wang, Hailong Zhang, and Atanas Rountev. On the unsoundness of static analysis for Android GUIs. In State of the Art in Program Analysis (SOAP), 2016. URL: http://dx.doi.org/10.1145/2931021.2931026.
  53. Shengqian Yang, Dacong Yan, Haowei Wu, Yan Wang, and Atanas Rountev. Static Control-Flow Analysis of User-Driven Callbacks in Android Applications. In International Conference on Software Engineering (ICSE), 2015. URL: http://dx.doi.org/10.1109/ICSE.2015.31.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact