CISPA
Browse

Model Checking Data Flows in Concurrent Network Updates

Download (436.5 kB)
conference contribution
posted on 2023-11-29, 18:12 authored by Bernd FinkbeinerBernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog, Jesko Hecking-Harbusch
We present a model checking approach for the verification of data flow correctness in networks during concurrent updates of the network configuration. This verification problem is of great importance for software-defined networking (SDN), where errors can lead to packet loss, black holes, and security violations. Our approach is based on a specification of temporal properties of individual data flows, such as the requirement that the flow is free of cycles. We check whether these properties are simultaneously satisfied for all active data flows while the network configuration is updated. To represent the behavior of the concurrent network controllers and the resulting evolutions of the configurations, we introduce an extension of Petri nets with a transit relation, which characterizes the data flow caused by each transition of the Petri net. For safe Petri nets with transits, we reduce the verification of temporal flow properties to a circuit model checking problem that can be solved with effective verification techniques like IC3, interpolation, and bounded model checking. We report on encouraging experiments with a prototype implementation based on the hardware model checker ABC.

History

Preferred Citation

Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog and Jesko Hecking-Harbusch. Model Checking Data Flows in Concurrent Network Updates. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2020-05-25

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3083, title = "Model Checking Data Flows in Concurrent Network Updates", author = "Finkbeiner, Bernd and Gieseking, Manuel and Olderog, Ernst-Rüdiger and Hecking-Harbusch, Jesko", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC