Abstract
The Internet of Things (IoT) is a broad concept comprising a wide ecosystem of interconnected services and devices connected to the Internet. The IoT concept holds fabulous promises, but security aspects tend to be significant barriers for the adoption of large-scale IoT deployments. This paper proposes an approach to assist companies or organisations in the security audit of IoT systems. This approach called Model Learning and Checking Approach (MLCA) combines model learning for automatically extracting models from event logs, and model checking for verifying whether security properties, given under the form of generic LTL formulas hold on models. The originality of MLCA lies in the fact that auditors do not have to craft models or to be expert LTL users. The LTL formula instantiation, which makes security properties concrete, is indeed semi-automatically performed by means of an expert system composed of inference rules. The latter encode some expert knowledge, which can be applied again to the same kind of systems with less efforts. We evaluated MLCA on 5 IoT systems with security measures provided by the European ENISA institute. We show that MLCA is very effective in detecting security issues and provides results within reasonable time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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.) ISoLA 2016. LNCS, vol. 9953, pp. 727–742. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_55
Beschastnikh, I., Brun, Y., Abrahamson, J., Ernst, M.D., Krishnamurthy, A.: Using declarative specification to improve the understanding, extensibility, and comparison of model-inference algorithms. IEEE Trans. Softw. Eng. 41(4), 408–428 (2015). https://doi.org/10.1109/TSE.2014.2369047
Beschastnikh, I., Brun, Y., Ernst, M.D., Krishnamurthy, A.: Inferring models of concurrent systems from logs of their behavior with Csight. In: Proceedings of the 36th International Conference on Software Engineering, pp. 468–479. ICSE 2014, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2568225.2568246, http://doi.acm.org/10.1145/2568225.2568246
van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with iOCO. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86–100. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24617-6_7
Celik, Z.B., McDaniel, P., Tan, G.: Soteria: automated iot safety and security analysis. In: 2018 USENIX Annual Technical Conference (USENIX ATC 18), pp. 147–158. USENIX Association, Boston, MA (July 2018). https://www.usenix.org/conference/atc18/presentation/celik
Chaabouni, N., Mosbah, M., Zemmari, A., Sauvignac, C., Faruki, P.: Network intrusion detection for iot security based on learning techniques. IEEE Commun. Surv. Tutor. 21(3), 2671–2701 (2019). https://doi.org/10.1109/COMST.2019.2896380
Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29
Costin, A., Zaddach, J.: Iot malware: Comprehensive survey, analysis framework and case studies (2018)
CSA: Security guidance for early adopters of the internet of things (iot), cloud security alliance, white paper (2015)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), pp. 411–420 (May 1999). https://doi.org/10.1145/302405.302672
ENISA: Baseline security recommendations for iot in the context of critical information infrastructures, Technical report (2017). https://www.enisa.europa.eu/publications/baseline-security-recommendations-for-iot
ETSI: Methods for testing & specification; risk-based security assessment and testing methodologies, Technical report (2015). https://www.etsi.org/
Falcone, Y., Jaber, M., Nguyen, T.H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011 - Proceedings of the 9th International Conference on Software Engineering and Formal Methods. Lecture Notes in Computer Science (LNCS), vol. 7041, pp. 204–220. Springer, Montevideo, Uruguay, November 2011. https://doi.org/10.1007/978-3-642-24690-6_15, https://hal.archives-ouvertes.fr/hal-00642969
Ge, M., Hong, J.B., Guttmann, W., Kim, D.S.: A framework for automating security analysis of the internet of things. J. Netw. Comput. Appl. 83, 12–27 (2017). https://doi.org/10.1016/j.jnca.2017.01.033, http://www.sciencedirect.com/science/article/pii/S1084804517300541
Gutiérrez-Madro\(\tilde{n}\)al, L., La Blunda, L., Wagner, M.F., Medina-Bulo, I.: Test event generation for a fall-detection iot system. IEEE Internet Things J. 6(4), 6642–6651 (2019). https://doi.org/10.1109/JIOT.2019.2909434
Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn., Addison-Wesley Professional, Boston (2011)
ISO: Iso/iec 27030 information technology - security techniques - guidelines for security and privacy in internet of things (iot) (2019)
Khan, M.A., Salah, K.: Iot security: review, blockchain solutions, and open challenges. Future Gener. Comput. Syst. 82, 395–411 (2018). https://doi.org/10.1016/j.future.2017.11.022, http://www.sciencedirect.com/science/article/pii/S0167739X17315765
Lally, G., Sgandurra, D.: Towards a framework for testing the security of iot devices consistently. In: Saracino, A., Mori, P. (eds.) Emerging Technologies for Authorization and Authentication, pp. 88–102. Springer International Publishing, Cham (2018)
Maksymyuk, T., Dumych, S., Brych, M., Satria, D., Jo, M.: An iot based monitoring framework for software defined 5g mobile networks. In: Proceedings of the 11th International Conference on Ubiquitous Information Management and Communication. IMCOM 2017, Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145/3022227.3022331
Mariani, L., Pastore, F.: Automated identification of failure causes in system logs. In: Software Reliability Engineering, 2008. ISSRE 2008. 19th International Symposium on Software Reliability Engineering (ISSRE), pp. 117–126, November 2008. https://doi.org/10.1109/ISSRE.2008.48
Matheu-García, S.N., Ramos, J.L.H., Gómez-Skarmeta, A.F., Baldini, G.: Risk-based automated assessment and testing for the cybersecurity certification and labelling of iot devices. Comput. Stand. Interfaces 62, 64–83 (2019)
Matheu Garcia, S.N., Hernández-Ramos, J., Skarmeta, A.: Toward a cybersecurity certification framework for the internet of things. IEEE Secur. Priv. 17, 66–76 (2019). https://doi.org/10.1109/MSEC.2019.2904475
Mohsin, M., Anwar, Z., Husari, G., Al-Shaer, E., Rahman, M.A.: Iotsat: A formal framework for security analysis of the internet of things (iot). In: 2016 IEEE Conference on Communications and Network Security (CNS), pp. 180–188, October 2016. https://doi.org/10.1109/CNS.2016.7860484
Nadir, I., et al.: An auditing framework for vulnerability analysis of iot system, pp. 39–47 (June 2019). https://doi.org/10.1109/EuroSPW.2019.00011
NIST: Framework for improving critical infrastructure cybersecurity, version 1.1, standards and technology, Technical report (2018). https://doi.org/10.6028
OWASP: Owasp testing guide v3.0 project (2020). http://www.owasp.org/index.php/Category:OWASP_Testing_Project#OWASP_Testing_Guide_v3
“Red-Hat-Software”: The business rule management system drools, March 2020. https://www.drools.org/
Salva, S., Blot, E.: Verifying the application of security measures in iot software systems with model learning. In: van Sinderen, M., Fill, H., Maciaszek, L.A. (eds.) Proceedings of the 15th International Conference on Software Technologies, pp. 350–360, ICSOFT 2020, Lieusaint, ScitePress, Paris, France, 7–9 July 2020. https://doi.org/10.5220/0009872103500360
Salva, S., Blot, E.: Cktail: model learning of communicating systems. In: Proceedings of the 15th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2020, Prague, CZECH REPUBLIC, 5–6 May 2020
Salva, S., Blot, E.: Verifying the application of security measures in iot software systems with model learning, companion site (2020). https://perso.limos.fr/~sesalva/tools/mlc/. Accessed Oct 2020
Siby, S., Maiti, R.R., Tippenhauer, N.O.: Iotscanner: Detecting and classifying privacy threats in iot neighborhoods. CoRR abs/1701.05007 (2017). http://arxiv.org/abs/1701.05007
Wilson, J., Wahby, R., Corrigan-Gibbs, H., Boneh, D., Levis, P., Winstein, K.: Trust but verify: Auditing the secure internet of things, pp. 464–474 (July 2017). https://doi.org/10.1145/3081333.3081342
Zhang, Z.K., Cho, M.C.Y., Shieh, S.: Emerging security threats and countermeasures in iot. In: Proceedings of the 10th ACM Symposium on Information, Computer and Communications Security, pp. 1–6. ASIA CCS15, Association for Computing Machinery, New York, NY, USA (2015). https://doi.org/10.1145/2714576.2737091
Acknowledgement
Research supported by the French Project VASOC (Auvergne-Rhône-Alpes Region) https://vasoc.limos.fr/.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Salva, S., Blot, E. (2021). MLCA: A Model-Learning-Checking Approach for IoT Systems. In: van Sinderen, M., Maciaszek, L.A., Fill, HG. (eds) Software Technologies. ICSOFT 2020. Communications in Computer and Information Science, vol 1447. Springer, Cham. https://doi.org/10.1007/978-3-030-83007-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-83007-6_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-83006-9
Online ISBN: 978-3-030-83007-6
eBook Packages: Computer ScienceComputer Science (R0)