Skip to main content
Erschienen in: Formal Methods in System Design 1/2018

27.11.2017

Wireless protocol validation under uncertainty

verfasst von: Jinghao Shi, Shuvendu K. Lahiri, Ranveer Chandra, Geoffrey Challen

Erschienen in: Formal Methods in System Design | Ausgabe 1/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
1
To represent the state machine succinctly, our example assumes that the DUT retries at most once.
 
2
The exact number of retransmissions is not part of the protocol, and NS-3 implementation set this to be 7.
 
Literatur
2.
Zurück zum Zitat 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–162 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–162
3.
Zurück zum Zitat 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–14 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–14
4.
Zurück zum Zitat 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–182 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–182
5.
Zurück zum Zitat 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–167 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–167
6.
Zurück zum Zitat Bonakdarpour B, Navabpour S, Fischmeister S (2011) Sampling-based runtime verification. In: FM 2011: formal methods. Springer, Berlin, pp 88–102 Bonakdarpour B, Navabpour S, Fischmeister S (2011) Sampling-based runtime verification. In: FM 2011: formal methods. Springer, Berlin, pp 88–102
7.
Zurück zum Zitat Bornholt J, Mytkowicz T, McKinley KS (2014) Uncertain\(<\)T\(>\): a first-order type for uncertain data. ACM SIGARCH Comput Archit News 42(1):51–66 Bornholt J, Mytkowicz T, McKinley KS (2014) Uncertain\(<\)T\(>\): a first-order type for uncertain data. ACM SIGARCH Comput Archit News 42(1):51–66
8.
Zurück zum Zitat 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 York 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 York
10.
Zurück zum Zitat 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–342 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–342
12.
Zurück zum Zitat 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–89 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–89
13.
Zurück zum Zitat 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–836 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–836
14.
Zurück zum Zitat 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–95 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–95
16.
Zurück zum Zitat 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–186 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–186
18.
Zurück zum Zitat 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–164 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–164
19.
Zurück zum Zitat 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–218 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–218
20.
Zurück zum Zitat 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–166 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–166
21.
Zurück zum Zitat Kamerman A, Monteban L (1997) Wavelan®-II: a high-performance wireless lan for the unlicensed band. Bell Labs Tech J 2(3):118–133CrossRef Kamerman A, Monteban L (1997) Wavelan®-II: a high-performance wireless lan for the unlicensed band. Bell Labs Tech J 2(3):118–133CrossRef
22.
Zurück zum Zitat 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–134 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–134
23.
Zurück zum Zitat Lacage M, Manshaei MH, Turletti T (2004) IEEE 802.11 rate adaptation: a practical approach. Research report RR-5208 (<inria-00070784>), p 25 Lacage M, Manshaei MH, Turletti T (2004) IEEE 802.11 rate adaptation: a practical approach. Research report RR-5208 (<inria-00070784>), p 25
24.
Zurück zum Zitat 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–122 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–122
25.
Zurück zum Zitat 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–86 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–86
26.
Zurück zum Zitat 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–143 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–143
27.
Zurück zum Zitat 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–88CrossRef 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–88CrossRef
28.
Zurück zum Zitat Mytkowicz T, Sweeney PF, Hauswirth M, Diwan A (2008) Observer effect and measurement bias in performance analysis Mytkowicz T, Sweeney PF, Hauswirth M, Diwan A (2008) Observer effect and measurement bias in performance analysis
29.
Zurück zum Zitat 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–34CrossRef 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–34CrossRef
30.
Zurück zum Zitat 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–122 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–122
32.
Zurück zum Zitat Shi J, Lahiri SK, Chandra R, Challen G (2016) Wireless protocol validation under uncertainty. Springer, Cham, pp 351–367 Shi J, Lahiri SK, Chandra R, Challen G (2016) Wireless protocol validation under uncertainty. Springer, Cham, pp 351–367
33.
Zurück zum Zitat 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–293 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–293
34.
Zurück zum Zitat 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–207 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–207
Metadaten
Titel
Wireless protocol validation under uncertainty
verfasst von
Jinghao Shi
Shuvendu K. Lahiri
Ranveer Chandra
Geoffrey Challen
Publikationsdatum
27.11.2017
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 1/2018
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0309-4

Weitere Artikel der Ausgabe 1/2018

Formal Methods in System Design 1/2018 Zur Ausgabe