Protocols to Code: Formal Verification of a Next-Generation Internet Router
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929339001470976 |
|---|---|
| author | Pereira, João C. Klenze, Tobias Giampietro, Sofia Limbeck, Markus Spiliopoulos, Dionysios Wolf, Felix A. Eilers, Marco Sprenger, Christoph Basin, David Müller, Peter Perrig, Adrian |
| author_facet | Pereira, João C. Klenze, Tobias Giampietro, Sofia Limbeck, Markus Spiliopoulos, Dionysios Wolf, Felix A. Eilers, Marco Sprenger, Christoph Basin, David Müller, Peter Perrig, Adrian |
| contents | We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_06074 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Protocols to Code: Formal Verification of a Next-Generation Internet Router Pereira, João C. Klenze, Tobias Giampietro, Sofia Limbeck, Markus Spiliopoulos, Dionysios Wolf, Felix A. Eilers, Marco Sprenger, Christoph Basin, David Müller, Peter Perrig, Adrian Cryptography and Security Networking and Internet Architecture Programming Languages We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed. |
| title | Protocols to Code: Formal Verification of a Next-Generation Internet Router |
| topic | Cryptography and Security Networking and Internet Architecture Programming Languages |
| url | https://arxiv.org/abs/2405.06074 |