Back to matrix

E02-SC: Pending

Rationale

Protocols to Code (Pereira et al., arXiv:2405.06074v1, 2024; later CCS 2025 publication) supplies concrete SCION forwarding verification using Isabelle/HOL and Go-code verification. Its scope includes path authorization and implementation safety. The authors describe the router implementation team as independent of the verification effort. However, the author list also includes SCION architect Adrian Perrig; separate implementation and verification teams do not alone establish the third-party independence required by E02.

Assessment method

Formal-study scope and independence review; no proof execution

Source context

Pereira et al., Protocols to Code, arXiv:2405.06074v1; authors, abstract and verification approach

Outstanding qualification

Identify review governance, author roles and relevant conflicts before classifying this collaboration as independent third-party analysis; shared affiliation alone is not an automatic exclusion. Alternatively locate a qualifying external audit or formal analysis. Preserve the substantive verification evidence rather than treating Pending as absence of security work. The inspected retained artifact is the 2024 v1 preprint; later publication is a separate version. No proof rerun, complete control-plane coverage or current deployed-build certification.

Public sources

• https://arxiv.org/abs/2405.06074v1
• https://doi.org/10.1145/3719027.3765104

Editorial evidence references

The following identifiers refer to research records not included in this public package; they are not public links.

• round293-sources.json