Preventive Model-based Verification and Repairing for SDN Requests
Burdonov I., Kossachev A., Nina Yevtushenko, L´opez J., Kushik N., Zeghlache D.
Software Defined Networking (SDN) is a novel network management technology, which currently attracts a lot of attention due to the provided capabilities. Recently, different works have been devoted to testing / verifying the (correct) configurations of SDN data planes. In general, SDN forwarding devices (e.g., switches) route (steer) traffic according to the configured flow rules; the latter identifies the set of virtual paths implemented in the data plane. In this paper, we propose a novel preventive approach for verifying that no misconfigurations (e.g., infinite loops), can occur given the requested set of paths. We discuss why such verification is essential, namely, how, when synthesizing a set of data paths, other not requested and undesired data paths (including loops) may be unintentionally configured. Furthermore, we show that for some cases the requested set of paths cannot be implemented without adding such undesired behavior, i.e., only a superset of the requested set can be implemented. Correspondingly, we present a verification technique for detecting such issues of potential misconfigurations and estimate the complexity of the proposed method; its polynomial complexity highlights the applicability of the obtained results. Finally, we propose a technique for debugging and repairing a set of paths in such a way that the corrected set does not induce undesired paths into the data plane, if the latter is possible.
, , in : Symposium on Logical Foundations of Computer Science (LFCS 2016). Vol. 9537: Logical Foundations of Computer Science.: Springer, 2016. P. 317-330.
Added: November 25, 2016
, , in : Logic, Rationality and Interaction. Proceedings of The Fifth International Conference on Logic, Rationality and Interaction. Lecture Notes in Computer Science 9394. Vol. 9394: Lecture Notes in Computer Science.: Springer, 2016. P. 295-307.
Added: November 25, 2016
Added: July 18, 2018
Austin : IEEE Computer Society, 2018
Added: July 3, 2019
, , , Journal of Parallel and Distributed Computing 2021 Vol. 155 P. 14-23
This paper provides a true-concurrency approach for the specification and verification of systems of concurrent communicating agents with durable actions. We present high-level Petri nets with durable actions (DaHL) to cope with various details in such complex systems. We define a DaHL module as an open variant of time-dependent colored Petri nets. A DaHL system ...
Added: May 13, 2021
, , et al., Proceedings of the ACM on Programming Languages 2021 Vol. 5 No. OOPSLA Article 98
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose ...
Added: February 2, 2022
, В кн. : Модель доходной стратификации российского общества: динамика, факторы, межстрановые сравнения. : Издательство Нестор-История, 2018. Гл. 1.4. С. 93-116.
The chapter covers the issue of monetary relative poverty line location in modern Russia. As it follows from international studies on income stratification it should be placed between 0.5 to 0.75 of median per capita income. Based on the poverty risk data, it is shown that the 0.5 line can be applied as a deep poverty line, and the ...
Added: April 16, 2019
The paper is devoted to testing critical Software Defined Networking (SDN) components and in particular, SDN-enabled switches. A switch can be seen as a forwarding device with a set of configured rules and thus, can be modelled and analyzed as a ‘stateless’ system. Correspondingly, in this paper we propose to use appropriate logic circuits or networks ...
Added: November 1, 2018
, , et al., , in : Proceedings of the 14th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management - (Volume 2) KEOD. Vol. 2: KEOD.: SciTePress, 2022. P. 237-244.
Added: October 24, 2022
Proceedings of the 16th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2021)
, , et al., SCITEPRESS – Science and Technology Publications, 2021
Software Defined Networking (SDN) devices (e.g., switches) route traffic according to the configured flow rules, and thus a set of virtual paths gets implemented in the data plane. We propose a novel preventive approach for verifying that no misconfigurations (e.g., infinite loops), can occur given the requested set of paths. Such verification is essential since when configuring a ...
Added: October 25, 2021
Added: July 18, 2018