kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Securing P4 Programs by Information Flow Control
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-8682-6804
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0003-2198-9818
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-6005-5992
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-8069-6495
Show others and affiliations
2025 (English)In: Proceedings - 2025 IEEE 38th Computer Security Foundations Symposium, CSF 2025, Institute of Electrical and Electronics Engineers (IEEE) , 2025, p. 284-299Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2025. p. 284-299
National Category
Computer Sciences Communication Systems
Identifiers
URN: urn:nbn:se:kth:diva-370452DOI: 10.1109/CSF64896.2025.00031ISI: 001597231500019Scopus ID: 2-s2.0-105014733792OAI: oai:DiVA.org:kth-370452DiVA, id: diva2:2002181
Conference
38th IEEE Computer Security Foundations Symposium, CSF 2025, Santa Cruz, United States of America, June 16-20, 2025
Note

Part of ISBN 9798331510817

QC 20250930

Available from: 2025-09-30 Created: 2025-09-30 Last updated: 2026-05-29Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Alshnakat, AnoudAhmadian, Amir M.Balliu, MusardGuanciale, RobertoDam, Mads

Search in DiVA

By author/editor
Alshnakat, AnoudAhmadian, Amir M.Balliu, MusardGuanciale, RobertoDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer SciencesCommunication Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 79 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf