Securing P4 Programs by Information Flow Control

• URL: http://arxiv.org/abs/2505.09221v1
• Date: Wed, 14 May 2025 08:42:46 GMT
• Title: Securing P4 Programs by Information Flow Control
• Authors: Anoud Alshnakat, Amir M. Ahmadian, Musard Balliu, Roberto Guanciale, Mads Dam,
• Abstract summary: This paper presents a novel security type system for analyzing information flow in P4 programs.<n>We formalize this type system and prove it sound, guaranteeing that well-typed programs satisfy noninterference.
• Score: 4.6847954792167
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Software-Defined Networking (SDN) has transformed network architectures by decoupling the control and data-planes, enabling fine-grained control over packet processing and forwarding. P4, a language designed for programming data-plane devices, allows developers to define custom packet processing behaviors directly on programmable network devices. This provides greater control over packet forwarding, inspection, and modification. However, the increased flexibility provided by P4 also brings significant security challenges, particularly in managing sensitive data and preventing information leakage within the data-plane. This paper presents a novel security type system for analyzing information flow in P4 programs that combines security types with interval analysis. The proposed type system allows the specification of security policies in terms of input and output packet bit fields rather than program variables. We formalize this type system and prove it sound, guaranteeing that well-typed programs satisfy noninterference. Our prototype implementation, Tap4s, is evaluated on several use cases, demonstrating its effectiveness in detecting security violations and information leakages.

Related papers

• Programmable Data Planes for Network Security [5.269440215944905]
  programmable data planes have transformed network security by enabling customized, line-rate packet processing.<n>We highlight the non-obvious design techniques that make complex in-network security functions feasible despite the constraints of the hardware platform.
  arXiv  Detail & Related papers  (2025-07-29T18:55:58Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)
• Output Constraints as Attack Surface: Exploiting Structured Generation to Bypass LLM Safety Mechanisms [0.9091225937132784]
  We reveal a critical control-plane attack surface to traditional data-plane vulnerabilities.<n>We introduce Constrained Decoding Attack, a novel jailbreak class that weaponizes structured output constraints to bypass safety mechanisms.<n>Our findings identify a critical security blind spot in current LLM architectures and urge a paradigm shift in LLM safety to address control-plane vulnerabilities.
  arXiv  Detail & Related papers  (2025-03-31T15:08:06Z)
• Pareto Control Barrier Function for Inner Safe Set Maximization Under Input Constraints [50.920465513162334]
  We introduce the PCBF algorithm to maximize the inner safe set of dynamical systems under input constraints.<n>We validate its effectiveness through comparison with Hamilton-Jacobi reachability for an inverted pendulum and through simulations on a 12-dimensional quadrotor system.<n>Results show that the PCBF consistently outperforms existing methods, yielding larger safe sets and ensuring safety under input constraints.
  arXiv  Detail & Related papers  (2024-10-05T18:45:19Z)
• P4Control: Line-Rate Cross-Host Attack Prevention via In-Network Information Flow Control Enabled by Programmable Switches and eBPF [14.787290539225245]
  P4Control is a network defense system that confines end-to-end information flows in a network and prevents cross-host attacks at line rate. We conduct extensive evaluations to show that P4Control can effectively prevent cross-host attacks in real time.
  arXiv  Detail & Related papers  (2024-05-23T18:19:10Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• Secure Instruction and Data-Level Information Flow Tracking Model for RISC-V [0.0]
  Unauthorized access, fault injection, and privacy invasion are potential threats from untrusted actors. We propose an integrated Information Flow Tracking (IFT) technique to enable runtime security to protect system integrity. This study proposes a multi-level IFT model that integrates a hardware-based IFT technique with a gate-level-based IFT (GLIFT) technique.
  arXiv  Detail & Related papers  (2023-11-17T02:04:07Z)
• Towards Formal Verification of a TPM Software Stack [0.5074812070492739]
  This paper describes a case study on formal verification of tpm2-tss using the Frama-C verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool.
  arXiv  Detail & Related papers  (2023-07-31T16:35:16Z)
• Generalized Planning in PDDL Domains with Pretrained Large Language Models [82.24479434984426]
  We consider PDDL domains and use GPT-4 to synthesize Python programs. We evaluate this approach in seven PDDL domains and compare it to four ablations and four baselines.
  arXiv  Detail & Related papers  (2023-05-18T14:48:20Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  We present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications. We provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology. We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions.
  arXiv  Detail & Related papers  (2021-06-03T16:45:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.