A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices
A Master of Science thesis in Computer Engineering by Alifiya Bhanpurawala entitled, “A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices”, submitted in November 2023. Thesis advisor is Dr. Khaled El-Fakih. Soft copy is available (Thesis, Completion Certificate,...
محفوظ في:
| المؤلف الرئيسي: | |
|---|---|
| التنسيق: | doctoralThesis |
| منشور في: |
2023
|
| الموضوعات: | |
| الوصول للمادة أونلاين: | http://hdl.handle.net/11073/25489 |
| الوسوم: |
إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|
| _version_ | 1864513444162568192 |
|---|---|
| author | Bhanpurawala, Alifiya |
| author_facet | Bhanpurawala, Alifiya |
| author_role | author |
| dc.contributor.none.fl_str_mv | El Fakih, Khaled |
| dc.creator.none.fl_str_mv | Bhanpurawala, Alifiya |
| dc.date.none.fl_str_mv | 2023-11 2024-03-11T06:48:52Z 2024-03-11T06:48:52Z |
| dc.format.none.fl_str_mv | application/pdf |
| dc.identifier.none.fl_str_mv | 35.232-2023.77 http://hdl.handle.net/11073/25489 |
| dc.language.none.fl_str_mv | en_US |
| dc.subject.none.fl_str_mv | Internet of things Edge devices Security threats Mutation testing Security faults Attacks Finite state machines with timeouts |
| dc.title.none.fl_str_mv | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| dc.type.none.fl_str_mv | info:eu-repo/semantics/publishedVersion info:eu-repo/semantics/doctoralThesis |
| description | A Master of Science thesis in Computer Engineering by Alifiya Bhanpurawala entitled, “A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices”, submitted in November 2023. Thesis advisor is Dr. Khaled El-Fakih. Soft copy is available (Thesis, Completion Certificate, Approval Signatures, and AUS Archives Consent Form). |
| format | doctoralThesis |
| id | aus_529cfc4499de691e276607b1e98f4c1d |
| identifier_str_mv | 35.232-2023.77 |
| language_invalid_str_mv | en_US |
| network_acronym_str | aus |
| network_name_str | aus |
| oai_identifier_str | oai:repository.aus.edu:11073/25489 |
| publishDate | 2023 |
| repository.mail.fl_str_mv | |
| repository.name.fl_str_mv | |
| repository_id_str | |
| spelling | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge DevicesBhanpurawala, AlifiyaInternet of thingsEdge devicesSecurity threatsMutation testingSecurity faultsAttacksFinite state machines with timeoutsA Master of Science thesis in Computer Engineering by Alifiya Bhanpurawala entitled, “A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices”, submitted in November 2023. Thesis advisor is Dr. Khaled El-Fakih. Soft copy is available (Thesis, Completion Certificate, Approval Signatures, and AUS Archives Consent Form).With the rapid growth in the number of IoT devices being added to the network, a major concern that arises is the security of these systems. As these devices are resource constrained, safety measures are difficult to implement on the edge. We propose a novel approach for the detection of IoT device attacks based on the use of formal modelling and mutation testing. Namely, we model the behaviour of small IoT devices such as motion sensors and RFID card reader as state machines with timeouts. We also model basic IoT attacks; namely, battery draining, sleep deprivation, data falsification, replay, and man in the middle attacks, as special mutants of these specifications. We also consider tests for detecting actual physical device manipulation. Mutation testing is then used to derive tests that distinguish these attacks from the original specifications. The behaviour of these mutants is tested in real environment by running the tests on the data collected while the edge device is still running. Our experiments show that derived number of attack mutants and tests is small and thus these tests can be executed many times with limited overhead on the physical device. Consequently, our approach is not deterred by related high costs of traditional mutation testing. Furthermore, we demonstrate that the tests generated by our method, encompassing the considered IoT attacks, do not adequately cover mutants derived through conventional mutation code-based operators. This highlights the necessity of employing our method. A framework that implements our approach is presented along with some other relevant case studies.College of EngineeringDepartment of Computer Science and EngineeringMaster of Science in Computer Engineering (MSCoE)El Fakih, Khaled2024-03-11T06:48:52Z2024-03-11T06:48:52Z2023-11info:eu-repo/semantics/publishedVersioninfo:eu-repo/semantics/doctoralThesisapplication/pdf35.232-2023.77http://hdl.handle.net/11073/25489en_USoai:repository.aus.edu:11073/254892025-06-26T12:34:35Z |
| spellingShingle | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices Bhanpurawala, Alifiya Internet of things Edge devices Security threats Mutation testing Security faults Attacks Finite state machines with timeouts |
| status_str | publishedVersion |
| title | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| title_full | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| title_fullStr | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| title_full_unstemmed | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| title_short | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| title_sort | A Formal Assisted Approach for Modeling and Testing Security Attacks in IoT Edge Devices |
| topic | Internet of things Edge devices Security threats Mutation testing Security faults Attacks Finite state machines with timeouts |
| url | http://hdl.handle.net/11073/25489 |