Wireless network access protocols are used in numerous safety critical applications. Network availability is essential for safety critical applications,since loss of availability can cause personal or material damage. An adversary can disrupt the availability of a wireless network using denial of service (DoS) attacks. The most widely used wireless protocols are vulnerable to DoS attacks. Researchers have published DoS attacks against IEEE 802.11 local area networks (LANs), IEEE 802.16 wide area networks (WANs) and GSM andUMTS mobile networks. In this work, we analyze DoS vulnerabilities in wireless network protocols and define four categories of attacks: jamming attacks, flooding attacks, semantic attacks and implementation specific attacks. We identify semantic attacks as the most severe threat to current andfuture wireless protocols, and as the category that has received the least attention by researchers. During the first phase of the research project we discover semantic DoS vulnerabilities in the IEEE 802.11 communication protocols through manual analysis. The 802.11 standard has been subject to manual analysis of DoS vulnerabilities for more than a decade, thus our results indicate that protocol vulnerabilities can elude manual analysis. We conclude that formal methods are required in order to improve protocol robustness against semantic DoS attacks.We propose a formal method that can be used to automatically discover protocol vulnerabilities. The formal method defines a protocol model, adversary model and cost model. The protocol participants and adversary are modeled as finite state transducers, while the cost is modeled as a function of time. Our primary goal is to construct a formal method that is practical, i.e. does not require a vast amount of resources to implement, and useful, i.e. able to discover protocol vulnerabilities. We verify and validate our proposed method by modeling the 802.11w amendment to the 802.11 standard using Promela as the modeling language. We then use the SPIN model checker to verify the model properties and experiments to validate the results. The modeling and experiments result in the discovery and experimental validation of four new deadlock vulnerabilities that had eluded manual analysis. We find one deadlock vulnerability in 802.11i and three deadlock vulnerabilitiesin 802.11w. A deadlock vulnerability is the most severe form of communication protocol DoS vulnerabilities, and their discovery and removal are an essential part of robust protocol design. Thus, we conclude that our proposed formal method is both practical and useful.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:ntnu-17479 |
| Date | January 2012 |
| Creators | Eian, Martin |
| Publisher | Norges teknisk-naturvitenskapelige universitet, Institutt for telematikk, Trondheim : NTNU |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Doctoral thesis, comprehensive summary, info:eu-repo/semantics/doctoralThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | Doctoral Theses at NTNU, 1503-8181 ; 2012:230 |
Page generated in 0.0024 seconds