An Economic Incentive-Based Risk Transfer Approach for Defending Against DDoS Attacks

Volumetric DDoS attacks are continued to be an immense threat to e-commerce and other online businesses from the last decade as attackers have much resources to amplify scale and frequency day by day. Despite significant efforts by research community and security professionals, we are lacking a robust solution against DDoS attacks. Generally, the attacker's investment in sending large amount of traffic to paralyze a system is negligible as compared to the loss they caused to an organization. Therefore, in this article, a risk transfer approach, a combination of techno-economic aspects is proposed where the risk of being attacked is transferred to some cooperating ISPs in return for economic incentives. In the proposed approach, user's attention, cash, other network and computational resources are contemplated as valuable resources. User must have consent from server in the form of “Sending Rights” which can be obtained by solving cryptographic puzzle (computational work) or by purchasing through micropayment or combination of both according to traffic load level. Our proposed solution is implemented on PN2sim simulator and then verified on SPIN model checker. Implementation results show the supremacy of our proposed approach.

Model Checking of WebRTC Peer to Peer System

The establishment of the multimedia session is crucial in the WebRTC architecture before media and data transmission. The preliminary bi-directional flow provides the network with all the information needed in order to control and manage the communication between end-users. This control includes the setup, management, and teardown of a session and the definition, and the modification of multiple features that will be enabled in the ongoing session. This is performed by a mechanism named Signaling. In this work, we will use the formal verification to increase confidence in our SDL model by checking the consistency and reliability of the WebRTC Peer to Peer system. The verification and validation are proved the most efficient tools to avoid errors and defects in the concurrent system designs. Indeed, by using model-checking techniques we will verify if the WebRTC system adheres to standards if it performs the selected functions in the correct manner. To achieve that, we will first translate the SDL model to an intermediate format IF that will be retranslated to a Promela Model. Second, using the SPIN model checker, we will verify the general correctness of the model before checking if the desired properties are satisfied using the Linear Temporal Logic (LTL).

A Method to Analyze Predicate Transition Nets Using SPIN Model Checker

High-level Petri nets (HLPNs) are a formal method for studying concurrent and distributed systems and have been widely used in many application domains. However, their strong expressive power hinders their analyzability. In this paper, we present a new transformational analysis method for analyzing a special class of HLPNs — predicate transition (PrT) nets. This method extends and improves our prior results by covering more PrT net features including full first-order logic formulas and exploring additional alternative translation schemes. This new analysis method is supported by a tool chain — front-end PIPE[Formula: see text] for creating and simulating PrT nets and back-end SPIN for model checking safety and liveness properties. We have applied this method to two benchmark systems used in annual Petri net model checking contest 2015. We discuss several properties and show the detailed model checking results in one system.

An Approach to UML Consistency Checking Based on Compositional Semantics

One of the ways to specify dynamic behavior in UML is to model interactions between objects with sequence diagrams, and model the behavior of each object with state machines. In this context, the problem of ensuring consistency between the sequence diagrams and state machines may arise. To verify consistency, the authors propose an approach based on compositions of Büchi automata which allow us to capture the evolution of each object among the lifeline. This paper focuses on UML modeling and verification methods and bridges the gap between theoretical studies on formal semantics and practical studies to implement languages through model transformations. The transformations include basic interactions, state invariants, strict and weak sequencing, and alternative interaction fragments. Ultimately, the results of the transformations are integrated into the Spin model checker as a never claim property. The authors use the Automatic Gate Controller Railway (AGCR) as an example to illustrate their approach.