Critical embedded systems deserve the highest level of assurance to guarantee that their implementation satisfies their specification. Verification techniques such as proof by deduction operate at source level but the verification effort often requires to design higher-level abstractions that facilitate the reasoning. However, this approach comes at the cost of assuming the correctness of the abstraction with respect to the source code.

We present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code outperforms a sequential evaluation of the policy rules.