Keynotes
Dawn Song: Formal Verification for Computer Security: Lessons Learned and Future Directions
October 4, 9:00am
Abstract: Formal verification techniques have been fruitful for a broad spectrum of different security applications and domains. However, many important questions and considerations influence the success of applying formal verification techniques to security applications and domains. In this talk, I will share lessons learned from experience of over a decade in applying formal verification techniques to security. I will also discuss new exciting application domains such as blockchain and smart contracts for formal verification. I will pose important, open challenges and discuss future directions for verifying next-generation systems such as learning systems.
Bio: Dawn Song is Professor of Computer Science at UC Berkeley. Prior to joining UC Berkeley, she was an Assistant Professor at Carnegie Mellon University from 2002 to 2007. Her research interest lies in security and privacy issues in computer systems and networks, including areas ranging from software security, networking security, database security, distributed systems security, to applied cryptography. She is the recipient of various awards including the MacArthur Fellowship, the Guggenheim Fellowship, the NSF CAREER Award, the Alfred P. Sloan Research Fellowship, the MIT Technology Review TR-35 Award, the IBM Faculty Award, the George Tallman Ladd Research Award, the Okawa Foundation Research Award, the Li Ka Shing Foundation Women in Science Distinguished Lecture Series Award, and Best Paper Awards from top conferences.
Christos Papadimitriou: Understanding evolution through algorithms
October 5, 10:00am
Abstract: Why is evolution so successful? What is the role of sex (recombination)? Why is there so much diversity in populations? How do novel traits arise? Are mutations random? And is evolution optimizing something? This talk will review recent work by the speaker and collaborators aiming at understanding the many persistent mysteries of evolution through computational ideas.
Bio: Christos Papadimitriou received his B.S. in EE from Athens Polytechnic, 1972, a M.S. in EE and Ph.D. in EECS from Princeton, 1974 and 1976 respectively. He is the C. Lester Hogan Professor of EECS. Professor Papadimitriou taught at Harvard, MIT, Athens Polytechnic, Stanford, and UCSD before joining EECS at UC Berkeley January, 1996. He is a member of the National Academy of Sciences, the American Academy of Arts and Sciences, and the National Academy of Engineering.
George Varghese: Network Verification – When Clarke Meets Cerf
October 6, 9:00am
Abstract: Surveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files which are programmed using arcane, low-level languages, akin to machine code. Taking our cue from program and hardware verification, we suggest fresh approaches. I will first describe a geometric model of network forwarding called Header Space. While header space analysis is similar to finite state machine verification, we exploit domain-specific structure to scale better than off-the shelf model checkers. Next, I show how to exploit physical symmetry to scale network verification for large data centers. While Emerson and Sistla showed how to exploit symmetry for model checking in 1996, they exploited symmetry on the logical Kripke structure. While header space models allow us to verify the forwarding tables in routers, there are also routing protocols such as BGP that build the forwarding tables. We show to go from header space verification to what we call control space verification to proactively catch latent bugs in BGP configurations. I will end with a vision for what we call Network Design Automation to build a suite of tools for networks inspired by the Electronic Design Automation Industry. (With collaborators at CMU, Edinburgh, MSR, Stanford, and UCLA.)
Bio: George Varghese received his Ph.D. in 1992 from MIT. From 1993-1999, he was a professor at Washington University, and at UCSD from 1999 to 2013. He was a Principal Researcher and Partner at Microsoft Research from 2012-2016. He is currently a Chancellor’s Professor of Computer Science at UCLA. His book Network Algorithmics was published in December 2004 by Morgan-Kaufman. In May 2004, he co-founded NetSift, which was acquired by Cisco in 2005. He won lifetime awards in networking from the EE (Kobayashi Award) and CS communities (SIGCOMM) in 2014.