Formal Methods in System Design

, Volume 53, Issue 1, pp 33–53 | Cite as

Wireless protocol validation under uncertainty

  • Jinghao ShiEmail author
  • Shuvendu K. Lahiri
  • Ranveer Chandra
  • Geoffrey Challen


Runtime validation of wireless protocol implementations cannot always employ direct instrumentation of the device under test (DUT). The DUT may not implement the required instrumentation, or the instrumentation may alter the DUT’s behavior when enabled. Wireless sniffers can monitor the DUT’s behavior without instrumentation, but they introduce new validation challenges. Losses caused by wireless propagation prevent sniffers from perfectly reconstructing the actual DUT packet trace. As a result, accurate validation requires distinguishing between specification deviations that represent implementation errors and those caused by sniffer uncertainty. We present a new approach enabling sniffer-based validation of wireless protocol implementations. Beginning with the original protocol monitor state machine, we automatically and completely encode sniffer uncertainty by selectively adding non-deterministic transitions. We characterize the NP-completeness of the resulting decision problem and provide an exhaustive algorithm for searching over all mutated traces. We also present practical protocol-oblivious heuristics for searching over the most likely mutated traces. We have implemented our framework and show that it can accurately identify implementation errors in the face of uncertainty.


Runtime verification Wireless protocol Sniffer Uncertainty 


  1. 1.
    Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Arnold M, Vechev M, Yahav E (2008) QVM: an efficient runtime for detecting defects in deployed systems. In: ACM SIGPLAN notices, vol 43. ACM, New York, pp 143–162Google Scholar
  3. 3.
    Bahl P, Chandra R, Padhye J, Ravindranath L, Singh M, Wolman A, Zill B (2006) Enhancing the security of corporate Wi-Fi networks using DAIR. In: Proceedings of the 4th international conference on mobile systems, applications and services. ACM, New York, pp 1–14Google Scholar
  4. 4.
    Bartocci E, Grosu R, Karmarkar A, Smolka SA, Stoller SD, Zadok E, Seyster J (2012) Adaptive runtime verification. In: International conference on runtime verification. Springer, Berlin, pp 168–182Google Scholar
  5. 5.
    Basin D, Klaedtke F, Marinovic S, Zălinescu E (2012) Monitoring compliance policies over incomplete and disagreeing logs. In: International conference on runtime verification. Springer, Berlin, pp 151–167Google Scholar
  6. 6.
    Bonakdarpour B, Navabpour S, Fischmeister S (2011) Sampling-based runtime verification. In: FM 2011: formal methods. Springer, Berlin, pp 88–102Google Scholar
  7. 7.
    Bornholt J, Mytkowicz T, McKinley KS (2014) Uncertain\(<\)T\(>\): a first-order type for uncertain data. ACM SIGARCH Comput Archit News 42(1):51–66Google Scholar
  8. 8.
    Cheng Y-C, Bellardo J, Benkö P, Snoeren AC, Voelker GM, Savage S (2006) Jigsaw: solving the puzzle of enterprise 802.11 analysis, vol 36. ACM, New YorkGoogle Scholar
  9. 9.
    Ciabarra M. WiFried: iOS 8 WiFi issue.
  10. 10.
    Das A, Lahiri SK, Lal A, Li Y (2015) Angelic verification: precise verification modulo unknowns. In: Computer aided verification—27th international conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, proceedings, part I, pp 324–342Google Scholar
  11. 11.
    digitalmediaphile. Windows 10 wifi issues with surface pro 3 and surface 3.
  12. 12.
    Edelkamp S, Schuppan V, Bošnački D, Wijs A, Fehnker A, Aljazzar H (2008) Survey on directed model checking. In: International workshop on model checking and artificial intelligence. Springer, Berlin, pp 65–89Google Scholar
  13. 13.
    Elbaum S, Rosenblum DS (2014) Known unknowns: testing in the presence of uncertainty. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, FSE 2014, New York, NY, USA. ACM, pp 833–836Google Scholar
  14. 14.
    Fei L, Midkiff SP (2006) Artemis: practical runtime monitoring of applications for execution anomalies. In: ACM SIGPLAN notices, vol 41. ACM, New York, pp 84–95Google Scholar
  15. 15.
    Gizmodo. The worst bugs in android 5.0 lollipop and how to fix them.
  16. 16.
    Godefroid P (1997) Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, pp 174–186Google Scholar
  17. 17.
  18. 18.
    Hauswirth M, Chilimbi TM (2004) Low-overhead memory leak detection using adaptive statistical profiling. In: Acm SIGPLAN notices, vol 39. ACM, New York, pp 156–164Google Scholar
  19. 19.
    Jakšić S, Bartocci E, Grosu R, Ničković D (2016) Quantitative monitoring of STL with edit distance. In: International conference on runtime verification. Springer, Berlin, pp 201–218Google Scholar
  20. 20.
    Kalajdzic K, Bartocci E, Smolka SA, Stoller SD, Grosu R (2013) Runtime verification with particle filtering. In: International conference on runtime verification. Springer, Berlin, pp 149–166Google Scholar
  21. 21.
    Kamerman A, Monteban L (1997) Wavelan®-II: a high-performance wireless lan for the unlicensed band. Bell Labs Tech J 2(3):118–133CrossRefGoogle Scholar
  22. 22.
    Lacage M, Manshaei MH, Turletti T (2004) IEEE 802.11 rate adaptation: a practical approach. In: Proceedings of the 7th ACM international symposium on modeling, analysis and simulation of wireless and mobile systems. ACM, New York, pp 126–134Google Scholar
  23. 23.
    Lacage M, Manshaei MH, Turletti T (2004) IEEE 802.11 rate adaptation: a practical approach. Research report RR-5208 (<inria-00070784>), p 25Google Scholar
  24. 24.
    Lee D, Netravali AN, Sabnani KK, Sugla B, John A (1997) Passive testing and applications to network management. In: Proceedings, 1997 international conference on network protocols, 1997. IEEE, pp 113–122Google Scholar
  25. 25.
    Mahajan R, Rodrig M, Wetherall D, Zahorjan J (2006) Analyzing the MAC-level behavior of wireless networks in the wild. In: ACM SIGCOMM computer communication review, vol 36. ACM, New York, pp 75–86Google Scholar
  26. 26.
    Marino D, Musuvathi M, Narayanasamy S (2009) Literace: effective sampling for lightweight data-race detection. In: ACM Sigplan notices, vol 44. ACM, New York, pp 134–143Google Scholar
  27. 27.
    Musuvathi M, Park DY, Chou A, Engler DR, Dill DL (2002) CMC: a pragmatic approach to model checking real code. ACM SIGOPS Oper Syst Rev 36(SI):75–88CrossRefGoogle Scholar
  28. 28.
    Mytkowicz T, Sweeney PF, Hauswirth M, Diwan A (2008) Observer effect and measurement bias in performance analysisGoogle Scholar
  29. 29.
    Riley GF, Henderson TR (2010) The ns-3 network simulator. In: Wehrle K, Günes M, Gross J (eds) Modeling and tools for network simulation. Springer, Berlin, pp 15–34CrossRefGoogle Scholar
  30. 30.
    Sampson A, Panchekha P, Mytkowicz T, McKinley KS, Grossman D, Ceze L (2014) Expressing and verifying probabilistic assertions. In: ACM SIGPLAN notices, vol 49. ACM, New York, pp 112–122Google Scholar
  31. 31.
    Savvius Inc. Savvius Wi-Fi adapters.
  32. 32.
    Shi J, Lahiri SK, Chandra R, Challen G (2016) Wireless protocol validation under uncertainty. Springer, Cham, pp 351–367Google Scholar
  33. 33.
    Sistla AP, Žefran M, Feng Y (2011) Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: International conference on runtime verification. Springer, Berlin, pp 276–293Google Scholar
  34. 34.
    Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2011) Runtime verification with state estimation. In: Khurshid S, Sen K (eds) Runtime verification. Springer, Berlin, pp 193–207Google Scholar
  35. 35.
  36. 36.
    Wikipedia. Xbox one controller.

Copyright information

© pringer Science+Business Media, LLC, part of Springer Nature 2017

Authors and Affiliations

  1. 1.University at BuffaloBuffaloUSA
  2. 2.Microsoft ResearchRedmondUSA

Personalised recommendations