Nothing Special   »   [go: up one dir, main page]

Kim et al., 2020 - Google Patents

Formal verification of SDN-based firewalls by using TLA+

Kim et al., 2020

View PDF
Document ID
6206833842734630218
Author
Kim Y
Kang M
Publication year
Publication venue
IEEE Access

External Links

Snippet

Software-defined networking (SDN) has generated increased interest due to the rapid growth in the amount of data generated by the development of the Internet and communications, the commercialization of 5G, and increasingly complex networks. While …
Continue reading at ieeexplore.ieee.org (PDF) (other versions)

Classifications

    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L12/00—Data switching networks
    • H04L12/28—Data switching networks characterised by path configuration, e.g. local area networks [LAN], wide area networks [WAN]
    • H04L12/46—Interconnection of networks
    • H04L12/4604—LAN interconnection over a backbone network, e.g. Internet, Frame Relay
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/08—Configuration management of network or network elements
    • H04L41/0803—Configuration setting of network or network elements
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L12/00—Data switching networks
    • H04L12/02—Details
    • H04L12/26—Monitoring arrangements; Testing arrangements
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L12/00—Data switching networks
    • H04L12/54—Store-and-forward switching systems
    • H04L12/56—Packet switching systems
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/08—Configuration management of network or network elements
    • H04L41/0866—Checking configuration
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/14—Arrangements for maintenance or administration or management of packet switching networks involving network analysis or design, e.g. simulation, network model or planning
    • H04L41/145—Arrangements for maintenance or administration or management of packet switching networks involving network analysis or design, e.g. simulation, network model or planning involving simulating, designing, planning or modelling of a network
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L43/00—Arrangements for monitoring or testing packet switching networks
    • H04L43/50—Testing arrangements
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/50—Network service management, i.e. ensuring proper service fulfillment according to an agreement or contract between two parties, e.g. between an IT-provider and a customer
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L41/00—Arrangements for maintenance or administration or management of packet switching networks
    • H04L41/12—Arrangements for maintenance or administration or management of packet switching networks network topology discovery or management
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L63/00—Network architectures or network communication protocols for network security
    • H04L63/14—Network architectures or network communication protocols for network security for detecting or protecting against malicious traffic
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L45/00—Routing or path finding of packets in data switching networks
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F15/00—Digital computers in general; Data processing equipment in general
    • G06F15/16—Combinations of two or more digital computers each having at least an arithmetic unit, a programme unit and a register, e.g. for a simultaneous processing of several programmes
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L49/00—Packet switching elements
    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L69/00—Application independent communication protocol aspects or techniques in packet data networks

Similar Documents

Publication Publication Date Title
Kim et al. Formal verification of SDN-based firewalls by using TLA+
US10880197B2 (en) Methods, systems, and computer readable media for testing a network node using source code for programming a packet forwarding plane of the network node
US10733088B1 (en) Methods, systems, and computer readable media for testing a network node or a related application programming interface using source code metadata
US7505463B2 (en) Rule set conflict resolution
US7512071B2 (en) Distributed flow enforcement
US7760730B2 (en) Rule set verification
Farzaneh et al. A graphical modeling tool supporting automated schedule synthesis for time-sensitive networking
Miserez et al. SDNRacer: Detecting concurrency violations in software-defined networks
Velner et al. Some complexity results for stateful network verification
US20140351801A1 (en) Formal verification apparatus and method for software-defined networking
Yao et al. Formal modeling and systematic black-box testing of sdn data plane
Li et al. MSAID: Automated detection of interference in multiple SDN applications
Tu et al. Linux network programming with p4
Helm et al. Application of network calculus models on programmable device behavior
Neves et al. Dynamic property enforcement in programmable data planes
Al-Haj et al. Flowtable pipeline misconfigurations in software defined networks
WO2014168164A1 (en) Network verification device, network verification method, and program
Parizotto et al. PRIME: Programming in-network modular extensions
Hussein et al. SDN verification plane for consistency establishment
Feng et al. A reo model of software defined networks
Shukla et al. Formal modeling and verification of software‐defined networks: A survey
Zheng et al. Analysis of BPEL data dependencies
Yao et al. Testing black-box sdn applications with formal behavior models
Wang et al. Simplifying network updates in SDN and NFV networks using GUM
Leet et al. Toward the first SDN programming capacity theorem on realizing high-level programs on low-level datapaths