HOL4P4

HOL4P4

HOL4P4 is a small-step, heapless formalisation and a type system of the P4 language implemented in HOL4. The syntax and semantics is written in the Ott metalanguage, which co-organizes export of definitions to multiple interactive theorem provers.

Content

• Semantics and type system in Ott
• Proof of determinism for the semantics
• Type preservation and progress proofs up to the frame level
• Executable semantics with soundness proof
• .p4 import tool (using Petr4 as backend)
• Symbolic execution tool
• Architecture models:
  • eBPF
  • VSS
  • V1Model

Installation

Follow the instructions in INSTALL.md. The CI scripts may also provide some guidance.

Papers

• A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, “HOL4P4: Semantics for a Verified Data Plane” (EuroP4 '22).
• A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam, “HOL4P4: Mechanized Small-Step Semantics for P4” (OOPSLA '24).
• D. Lundberg, R. Guanciale, and M. Dam, “Proof-Producing Symbolic Execution for P4” (VSTTE '24).

License

This project is distributed under the terms of the Apache License (Version 2.0), and the BSD 3-Clause License; users may pick which license to apply.

See COPYRIGHT, LICENSE-APACHE and LICENSE-BSD for details.