BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Secure Routing - Peter Müller (ETH Zürich)
DTSTART:20220706T100000Z
DTEND:20220706T110000Z
UID:TALK175763@talks.cam.ac.uk
DESCRIPTION:SCION is a new Internet architecture that addresses many of th
 e security vulnerabilities of today&rsquo\;s Internet. Its clean-slate des
 ign 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 t
 o its concrete implementation. The project uses stepwise refinement to pro
 ve that the protocol withstands increasingly strong attackers. The refinem
 ent proofs assume that all network components such as routers satisfy thei
 r specifications. This property is then verified separately using deductiv
 e program verification in separation logic. This talk will give an overvie
 w of the verifiedSCION project and explain\, in particular\, how we verify
  code-level properties such as memory safety\, I/O behavior\, and informat
 ion flow security.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR