Skip to main content

2020 | OriginalPaper | Buchkapitel

26. Security Testing of Internet of Things for Smart City Applications: A Formal Approach

verfasst von : Moez Krichen, Mariam Lahami, Omar Cheikhrouhou, Roobaea Alroobaea, Afef Jmal Maâlej

Erschienen in: Smart Infrastructure and Applications

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

This is a work in progress in which we are interested in testing security aspects of Internet of Things for smart cities. For this purpose we follow a model-based approach which consists in: modeling the system under investigation with an appropriate formalism; deriving test suites from the obtained model; applying some coverage criteria to select suitable tests; executing the obtained tests; and finally collecting verdicts and analyzing them in order to detect errors and repair them. The adopted formalism is based on the model of extended timed automata with inputs and outputs. We propose a conformance testing relation, the so-called extended timed input–output conformance relation—etioco. For test execution, we introduce a cloud-based architecture.

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 "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!

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!

Literatur
1.
Zurück zum Zitat Ahmad, A., Bouquet, F., Fourneret, E., Le Gall, F., Legeard, B.: Model-based testing as a service for IOT platforms. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, pp. 727–742. Springer, Cham (2016)CrossRef Ahmad, A., Bouquet, F., Fourneret, E., Le Gall, F., Legeard, B.: Model-based testing as a service for IOT platforms. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, pp. 727–742. Springer, Cham (2016)CrossRef
3.
Zurück zum Zitat Behrmann, G., David, A. and Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.)International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. Revised Lectures, vol. 3185, LNCS, pp. 200–237. Springer, Berlin (2004) Behrmann, G., David, A. and Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.)International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. Revised Lectures, vol. 3185, LNCS, pp. 200–237. Springer, Berlin (2004)
4.
Zurück zum Zitat Bohli, J.-M., Skarmeta, A., Moreno, M.V., García, D., Langendörfer, P.: Smartie project: secure IoT data management for smart cities. In: 2015 International Conference on Recent Advances in Internet of Things (RIoT), vol. 00, pp. 1–6 (2015) Bohli, J.-M., Skarmeta, A., Moreno, M.V., García, D., Langendörfer, P.: Smartie project: secure IoT data management for smart cities. In: 2015 International Conference on Recent Advances in Internet of Things (RIoT), vol. 00, pp. 1–6 (2015)
5.
Zurück zum Zitat Cheikhrouhou, O.: Secure group communication in wireless sensor networks: a survey. J. Netw. Comput. Appl. 61, 115–132 (2016)CrossRef Cheikhrouhou, O.: Secure group communication in wireless sensor networks: a survey. J. Netw. Comput. Appl. 61, 115–132 (2016)CrossRef
6.
Zurück zum Zitat Felderer, M., Zech, P., Breu, R., Büchler, M., Pretschner, A.: Model-based security testing: a taxonomy and systematic classification. Softw. Test. Verif. Reliab. 26(2), 119–148 (2016)CrossRef Felderer, M., Zech, P., Breu, R., Büchler, M., Pretschner, A.: Model-based security testing: a taxonomy and systematic classification. Softw. Test. Verif. Reliab. 26(2), 119–148 (2016)CrossRef
7.
Zurück zum Zitat Gao, J., Bai, X., Tsai, W.-T.: Cloud testing- issues, challenges, needs and practice. Softw. Eng. Int. J. 1(1), 9–23 (2011) Gao, J., Bai, X., Tsai, W.-T.: Cloud testing- issues, challenges, needs and practice. Softw. Eng. Int. J. 1(1), 9–23 (2011)
8.
Zurück zum Zitat Garcia-Morchon, O., Kumar, S., Keoh, S.L., Hummen, R., Struik, R.: Security Considerations in the IP-Based Internet of Things, Internet-Draft draft-garcia-core-security-06, Internet Engineering Task Force, Fremont (2013). Work in Progress Garcia-Morchon, O., Kumar, S., Keoh, S.L., Hummen, R., Struik, R.: Security Considerations in the IP-Based Internet of Things, Internet-Draft draft-garcia-core-security-06, Internet Engineering Task Force, Fremont (2013). Work in Progress
9.
Zurück zum Zitat Granjal, J., Monteiro, E., Sá Silva, J.: On the effectiveness of end-to-end security for internet-integrated sensing applications. In: 2012 IEEE International Conference on Green Computing and Communications, pp. 87–93 (2012) Granjal, J., Monteiro, E., Sá Silva, J.: On the effectiveness of end-to-end security for internet-integrated sensing applications. In: 2012 IEEE International Conference on Green Computing and Communications, pp. 87–93 (2012)
10.
Zurück zum Zitat Heer, T., Garcia-Morchon, O., Hummen, R., Keoh, S.L., Kumar, S.S., Wehrle, K.: Security challenges in the ip-based internet of things. Wirel. Pers. Commun. 61(3), 527–542 (2011)CrossRef Heer, T., Garcia-Morchon, O., Hummen, R., Keoh, S.L., Kumar, S.S., Wehrle, K.: Security challenges in the ip-based internet of things. Wirel. Pers. Commun. 61(3), 527–542 (2011)CrossRef
11.
Zurück zum Zitat Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) Automata, Languages and Programming, pp. 545–558. Springer, Berlin (1992)CrossRef Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) Automata, Languages and Programming, pp. 545–558. Springer, Berlin (1992)CrossRef
12.
Zurück zum Zitat Hernández-Ramos, J.L., Moreno, M.V., Bernabé, J.B., Carrillo, D.G., Skarmeta, A.F.: SAFIR: secure access framework for IoT-enabled services on smart buildings. J. Comput. Syst. Sci. 81(8), 1452–1463 (2015)MathSciNetCrossRef Hernández-Ramos, J.L., Moreno, M.V., Bernabé, J.B., Carrillo, D.G., Skarmeta, A.F.: SAFIR: secure access framework for IoT-enabled services on smart buildings. J. Comput. Syst. Sci. 81(8), 1452–1463 (2015)MathSciNetCrossRef
13.
Zurück zum Zitat Hernández-Ramos, J.L., Jara, A.J., Marin, L., Gómez, A.F.S.: Dcapbac: embedding authorization logic into smart things through ECC optimizations. Int. J. Comput. Math. 93(2), 345–366 (2016)CrossRef Hernández-Ramos, J.L., Jara, A.J., Marin, L., Gómez, A.F.S.: Dcapbac: embedding authorization logic into smart things through ECC optimizations. Int. J. Comput. Math. 93(2), 345–366 (2016)CrossRef
14.
Zurück zum Zitat Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using uppaal. In: Petrenko A., Ulrich, A. (eds.) Formal Approaches to Software Testing, pp. 114–130. Springer, Berlin (2004)CrossRef Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using uppaal. In: Petrenko A., Ulrich, A. (eds.) Formal Approaches to Software Testing, pp. 114–130. Springer, Berlin (2004)CrossRef
15.
Zurück zum Zitat Keoh, S., Kumar, S., Garcia-Morchon, O., Dijk, E., Rahman, A.: DTLS-Based Multicast Security for Low-Power and Lossy Networks (LLNs). Internet-Draft Draft-keoh-dice-multicast-security-08, Internet Engineering Task Force, Fremont (2014). Work in Progress. Keoh, S., Kumar, S., Garcia-Morchon, O., Dijk, E., Rahman, A.: DTLS-Based Multicast Security for Low-Power and Lossy Networks (LLNs). Internet-Draft Draft-keoh-dice-multicast-security-08, Internet Engineering Task Force, Fremont (2014). Work in Progress.
16.
Zurück zum Zitat Krichen, M.: A formal framework for black-box conformance testing of distributed real-time systems. IJCCBS 3(1/2), 26–43 (2012)CrossRef Krichen, M.: A formal framework for black-box conformance testing of distributed real-time systems. IJCCBS 3(1/2), 26–43 (2012)CrossRef
17.
Zurück zum Zitat Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Graf, S., Mounier, L. (eds.) Model Checking Software, pp. 109–126. Springer, Berlin (2004)CrossRef Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Graf, S., Mounier, L. (eds.) Model Checking Software, pp. 109–126. Springer, Berlin (2004)CrossRef
18.
Zurück zum Zitat Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3), 238–304 (2009)CrossRef Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3), 238–304 (2009)CrossRef
19.
Zurück zum Zitat Krichen, M., Cheikhrouhou, O., Lahami, M., Alroobaea, R., Jmal Maâlej, A.: Towards a model-based testing framework for the security of internet of things for smart city applications. In: Mehmood, R., Bhaduri, B., Katib, I., Chlamtac, I. (eds.) Smart Societies, Infrastructure, Technologies and Applications, pp. 360–365. Springer, Cham (2018)CrossRef Krichen, M., Cheikhrouhou, O., Lahami, M., Alroobaea, R., Jmal Maâlej, A.: Towards a model-based testing framework for the security of internet of things for smart city applications. In: Mehmood, R., Bhaduri, B., Katib, I., Chlamtac, I. (eds.) Smart Societies, Infrastructure, Technologies and Applications, pp. 360–365. Springer, Cham (2018)CrossRef
20.
Zurück zum Zitat Lahami, M, Krichen, M., Jmaïel, M.: Safe and efficient runtime testing framework applied in dynamic and distributed systems. Sci. Comput. Program. 122(C), 1–28 (2016)CrossRef Lahami, M, Krichen, M., Jmaïel, M.: Safe and efficient runtime testing framework applied in dynamic and distributed systems. Sci. Comput. Program. 122(C), 1–28 (2016)CrossRef
21.
Zurück zum Zitat Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proceedings of the IEEE 84(8), 1090–1123 (1996)CrossRef Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proceedings of the IEEE 84(8), 1090–1123 (1996)CrossRef
22.
Zurück zum Zitat Maâlej, A.J., Krichen, M.: A model based approach to combine load and functional tests for service oriented architectures. In: Proceedings of the 10th Workshop on Verification and Evaluation of Computer and Communication System, VECoS 2016, Tunis, October 6–7, 2016, pp. 123–140 (2016) Maâlej, A.J., Krichen, M.: A model based approach to combine load and functional tests for service oriented architectures. In: Proceedings of the 10th Workshop on Verification and Evaluation of Computer and Communication System, VECoS 2016, Tunis, October 6–7, 2016, pp. 123–140 (2016)
23.
Zurück zum Zitat Mell, P., Grance, T.: The Nist Definition of Cloud Computing (2011) Mell, P., Grance, T.: The Nist Definition of Cloud Computing (2011)
24.
Zurück zum Zitat Myers, G.J., Sandler, C.: The Art of Software Testing, Wiley, Hoboken (2004) Myers, G.J., Sandler, C.: The Art of Software Testing, Wiley, Hoboken (2004)
25.
Zurück zum Zitat Nguyen, K.T., Laurent, M., Oualha, N.: Survey on secure communication protocols for the internet of things. Ad Hoc Netw. 32, 17–31 (2015)CrossRef Nguyen, K.T., Laurent, M., Oualha, N.: Survey on secure communication protocols for the internet of things. Ad Hoc Netw. 32, 17–31 (2015)CrossRef
26.
Zurück zum Zitat Park, S.D., Kim, K.-H., Haddad, W., Chakrabarti, S., Laganier, J.: IPv6 over Low Power WPAN Security Analysis. Internet-Draft draft-daniel-6lowpan-security-analysis-05, Internet Engineering Task Force, Fremont (2011). Work in Progress Park, S.D., Kim, K.-H., Haddad, W., Chakrabarti, S., Laganier, J.: IPv6 over Low Power WPAN Security Analysis. Internet-Draft draft-daniel-6lowpan-security-analysis-05, Internet Engineering Task Force, Fremont (2011). Work in Progress
27.
Zurück zum Zitat Raza, S., Wallgren, L., Voigt, T.: Svelte: real-time intrusion detection in the internet of things. Ad Hoc Netw. 11(8), 2661–2674 (2013)CrossRef Raza, S., Wallgren, L., Voigt, T.: Svelte: real-time intrusion detection in the internet of things. Ad Hoc Netw. 11(8), 2661–2674 (2013)CrossRef
28.
Zurück zum Zitat Roman, R., Zhou, J., Lopez, J.: On the features and challenges of security and privacy in distributed internet of things. Comput. Netw. 57(10), 2266–2279 (2013)CrossRef Roman, R., Zhou, J., Lopez, J.: On the features and challenges of security and privacy in distributed internet of things. Comput. Netw. 57(10), 2266–2279 (2013)CrossRef
29.
Zurück zum Zitat Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing timed automata. Theor. Comput. Sci. 254(1), 225–257 (2001)MathSciNetCrossRef Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing timed automata. Theor. Comput. Sci. 254(1), 225–257 (2001)MathSciNetCrossRef
30.
Zurück zum Zitat Tretmans, J.: Testing concurrent systems: a formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR’99 Concurrency Theory, pp. 46–65. Springer, Berlin (1999)CrossRef Tretmans, J.: Testing concurrent systems: a formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR’99 Concurrency Theory, pp. 46–65. Springer, Berlin (1999)CrossRef
31.
Zurück zum Zitat Tripakis, S.: Fault diagnosis for timed automata. In: Damm, W., Olderog, E.R. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 205–221. Springer, Berlin (2002)CrossRef Tripakis, S.: Fault diagnosis for timed automata. In: Damm, W., Olderog, E.R. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 205–221. Springer, Berlin (2002)CrossRef
32.
Zurück zum Zitat Vucinic, M., Tourancheau, B., Rousseau, F., Duda, A., Damon, L., Guizzetti, R.: OSCAR: object security architecture for the internet of things. CoRR, abs/1404.7799 (2014) Vucinic, M., Tourancheau, B., Rousseau, F., Duda, A., Damon, L., Guizzetti, R.: OSCAR: object security architecture for the internet of things. CoRR, abs/1404.7799 (2014)
33.
Zurück zum Zitat Vučinić, M., Tourancheau, B., Rousseau, F., Duda, A., Damon, L., Guizzetti, R.: Oscar. Ad Hoc Netw. 32(C), 3–16 (2015)CrossRef Vučinić, M., Tourancheau, B., Rousseau, F., Duda, A., Damon, L., Guizzetti, R.: Oscar. Ad Hoc Netw. 32(C), 3–16 (2015)CrossRef
34.
Zurück zum Zitat Walewski, J.: Internet-of-Things Architecture IOTA Project Deliverable d1.2 - Initial Architectural Reference Model for IOT (2018) Walewski, J.: Internet-of-Things Architecture IOTA Project Deliverable d1.2 - Initial Architectural Reference Model for IOT (2018)
35.
Zurück zum Zitat Wallgren, L., Raza, S., Voigt, R.: Routing attacks and countermeasures in the RPL-based internet of things. Int. J. Distrib. Sens. Netw. 9(8), 794326 (2013)CrossRef Wallgren, L., Raza, S., Voigt, R.: Routing attacks and countermeasures in the RPL-based internet of things. Int. J. Distrib. Sens. Netw. 9(8), 794326 (2013)CrossRef
36.
Zurück zum Zitat Yan, Z., Zhang, P., Vasilakos, A.V.: A survey on trust management for internet of things. J. Netw. Comput. Appl. 42, 120–134 (2014)CrossRef Yan, Z., Zhang, P., Vasilakos, A.V.: A survey on trust management for internet of things. J. Netw. Comput. Appl. 42, 120–134 (2014)CrossRef
Metadaten
Titel
Security Testing of Internet of Things for Smart City Applications: A Formal Approach
verfasst von
Moez Krichen
Mariam Lahami
Omar Cheikhrouhou
Roobaea Alroobaea
Afef Jmal Maâlej
Copyright-Jahr
2020
DOI
https://doi.org/10.1007/978-3-030-13705-2_26

Neuer Inhalt