2 papers
cs.CR2024
Protocols to Code: Formal Verification of a Next-Generation Internet Router
João C. Pereira, Tobias Klenze, Sofia Giampietro +8
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…
cs.LO2023
Refinement Proofs in Rust Using Ghost Locks
Aurea Bílá, João C. Pereira, Jan Schär +1
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementatio…