[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Freire et al., 2018 - Google Patents

Uncovering bugs in p4 programs with assertion-based verification

Freire et al., 2018

View PDF
Document ID
884156152872753761
Author
Freire L
Neves M
Leal L
Levchenko K
Schaeffer-Filho A
Barcellos M
Publication year
Publication venue
Proceedings of the Symposium on SDN Research

External Links

Snippet

Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data …
Continue reading at dl.acm.org (PDF) (other versions)

Classifications

    • 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
    • G06F11/362—Software debugging
    • G06F11/3636—Software debugging by tracing the execution of the program
    • 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
    • G06F11/3668—Software testing
    • G06F11/3672—Test management
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/57—Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities
    • G06F21/577—Assessing vulnerabilities and evaluating computer system security
    • 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
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • 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/44—Arrangements for executing specific programmes
    • G06F9/455—Emulation; Software simulation, i.e. virtualisation or emulation of application or operating system execution engines
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/30—Monitoring
    • G06F11/34—Recording or statistical evaluation of computer activity, e.g. of down time, of input/output operation; Recording or statistical evaluation of user activity, e.g. usability assessment
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/07—Error detection; Error correction; Monitoring responding to the occurence of a fault, e.g. fault tolerance
    • G06F11/0703—Error or fault processing not based on redundancy, i.e. by taking additional measures to deal with the error or fault not making use of redundancy in operation, in hardware, or in data representation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • 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
    • 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
    • H04L43/00—Arrangements for monitoring or testing packet switching networks
    • H04L43/50—Testing arrangements

Similar Documents

Publication Publication Date Title
Freire et al. Uncovering bugs in p4 programs with assertion-based verification
Liu et al. P4v: Practical verification for programmable data planes
Stoenescu et al. Debugging P4 programs with Vera
Neves et al. Verification of p4 programs in feasible time using assertions
Zaostrovnykh et al. Verifying software network functions with no verification expertise
Ball et al. Vericon: towards verifying controller programs in software-defined networks
Yuan et al. {NetSMC}: A Custom Symbolic Model Checker for Stateful Network Verification
Tian et al. Aquila: a practically usable verification system for production-scale programmable data planes
El-Hassany et al. SDNRacer: concurrency analysis for software-defined networks
Wu et al. Automatic synthesis of nf models by program analysis
Skowyra et al. A verification platform for SDN-enabled applications
Shukla et al. Runtime verification of P4 switches with reinforcement learning
Miserez et al. SDNRacer: Detecting concurrency violations in software-defined networks
Panda et al. Verifying isolation properties in the presence of middleboxes
Dumitru et al. Can we exploit buggy P4 programs?
Kheradmand et al. P4K: A formal semantics of P4 and applications
Yaseen et al. Aragog: Scalable runtime verification of shardable networked systems
Marchetto et al. A framework for verification-oriented user-friendly network function modeling
Kohler et al. Programming language optimizations for modular router configurations
Li et al. MSAID: Automated detection of interference in multiple SDN applications
Bressana et al. Finding hard-to-find data plane bugs with a PTA
Neves et al. Dynamic property enforcement in programmable data planes
Tu et al. Linux network programming with p4
Pirelli et al. Automated verification of network function binaries
Birnfeld et al. P4 switch code data flow analysis: Towards stronger verification of forwarding plane software