Abstract: Detecting serious security vulnerabilities in protocols and products is extremely difficult. Current vulnerability test methods themselves are limited and it may be that vulnerabilities are in the product and/or are inherent in the protocol itself. Many detected vulnerabilities often relate only to values out-of-range for message parameters, and thus correspond mainly to syntactic problems. Decisions are often based on observing if the product being tested has crashed or if its service has been impaired during the test in order to decide whether the product is vulnerable, without knowing the semantics and real cause of the crash or impairment. Thus, the problem under study is to develop a cost-effective vulnerability test methodology based on the semantics of vulnerability for VoIP protocols and products.
The basis of the methodology is the use of formal methods and heuristic search for vulnerabilities. Principles based on security boundaries provide a basis for applying heuristic rules for automated state-space searching for vulnerabilities in protocol and system models. The Session Initiation Protocol (SIP) is used to illustrate and validate the approach. Through Formal Modeling, validation by heuristic state-space searching, simulation and testing, our formal heuristic method uses good engineering practice and automation for vulnerability analysis of communication protocols.
We have applied formal methods, heuristics, and risk estimation principles to the vulnerability testing of SIP. We show how to augment a formal model of SIP by adding heuristics based on risk parameters. By using risk thresholds, we show how to guide the development of high-risk vulnerability tests for SIP using automated analysis of the model.