[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, and information  flow security.

About:

Peter Müller has been Full Professor and  head of the Programming Methodology  Group at ETH Zurich since August 2008.  His research focuses on languages, techniques, and tools for the development of correct software. His previous appointments  include a position as Researcher at Microsoft  Research in Redmond, an Assistant Professorship at ETH Zurich, and a position as  Project Manager at Deutsche Bank in Frankfurt. Peter Müller received his PhD from the  University of Hagen