[SCS]: CSI Talk - Verified Secure Routing

Important this is an event organized by the School of Computer Science. It is not affiliated with the ACM Student Chapter!

CION is a new Internet architecture that addresses many of the security vulnerabilities of  today’s Internet. Its clean-slate design provides,  among other properties, route control, failure  isolation, and multi-path communication. The  verifiedSCION project is an effort to formally  verify the correctness and security of SCION. It  aims to provide strong guarantees for the entire  architecture, from the protocol design to its  concrete implementation. The project uses  stepwise refinement to prove that the protocol  withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately  using deductive program verification in separation logic. This talk will give an overview of the  verifiedSCION project and explain, in particular,  how we verify code-level properties such as  memory safety, I/O behavior,…