Computer Science

Speaker 1:  Professor Peter O’Hearn, Facebook and University College London Website]

Speaker 2: Professor Brad Karp – University College London Website]

Dates: April 27, 2016

Speaker Host: Professor Jon Crowcroft FRS (Science and Programme Committees)




Speaker 1: Professor Peter O’Hearn, Facebook & UCL

Reasoning with Big Code

Organisations are increasingly relying on large, evolving code bases, often involving many millions of lines of code undergoing rapid concurrent modification. Keeping the code in shape is critical to the organisations that rely on it, and this presents considerable engineering and scientific challenges. Reasoning of different forms (spanning static and dynamic verification) plays a crucial role. In this talk I will describe the reasoning at scale that we do at Facebook, and I will relay some of the experiences of deploying a static analyser that uses logical reasoning and yet works at a velocity consistent with Facebook’s fast-paced engineering culture. I will also outline what I think are some of the research opportunities and challenges posed by big code.

Peter O’Hearn is an Engineering Manager at Facebook and a Professor of Computer Science at UCL. His research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of program proof. With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program proof. In 2009 he cofounded a software verification startup company, Monoidics Ltd, which was acquired by Facebook in 2013. The Facebook Infer program analyzer, developed by Peter’s team and recently open-sourced, runs on every modification to the code of Facebook’s mobile apps, in a typical month issuing millions of calls to a custom separation logic theorem prover and catching hundreds of bugs before they reach production.


Speaker 2: Professor Brad Karp, University College London

Safeguarding Users’ Sensitive Data in the Cloud and the Browser

The remote reachability of computer systems that run imperfect, vulnerable software puts individuals’ and organizations’ security and privacy at risk. Miscreants divulge users’ sensitive data by exploiting vulnerabilities in network-attached servers’ software. Even the *client side* of web applications poses acute privacy risks. Modern web applications are conglomerations of JavaScript written by multiple authors: application developers routinely incorporate code from third-party libraries, and mashup applications synthesize data and code hosted at different sites. In current browsers, a web application’s developer and user must trust third-party code in libraries not to leak the user’s sensitive information. Fundamentally, today’s browser security model trades privacy for flexibility because it lacks a sufficient mechanism for confining untrusted code. In this talk, I will describe techniques that address these privacy threats on the server and client sides of distributed applications. I will first describe how to design software that adheres to the principle of least privilege, and does not divulge sensitive information, even when successfully exploited by an attacker. I will then present COWL (Confinement with Origin Web Labels), a robust JavaScript confinement system for modern web browsers. COWL introduces label-based mandatory access control to browsing contexts in a way that is fully backward-compatible with legacy web content. I’ll use simple case-study applications to motivate COWL’s design and demonstrate how COWL allows both the inclusion of untrusted scripts in applications and the building of mashups that combine sensitive information from multiple distinct origins, all while protecting users’ privacy.

Brad Karp is a Professor of Computer Systems and Networks and Head of the Systems and Networks Research Group in the Department of Computer Science at University College London (UCL). His research interests span computer system and network security (current work includes web browser and JavaScript security; past work includes the Wedge secure OS extensions and the Autograph and Polygraph worm signature generation systems), large-scale distributed systems (recent work includes LOUP, a provably loop-free Internet routing protocol; past work includes the Open DHT shared public DHT service), and wireless networks (current work includes techniques for improving capacity at the MAC and PHY layers; past work includes the GPSR and CLDP scalable geographic routing protocols). Prior to taking up his post at UCL in late 2005, Karp held joint appointments at Intel Research and Carnegie Mellon, and as a researcher at ICSI at UC Berkeley. He is a recipient of the Royal Society-Wolfson Research Merit Award (2005-2010). He served as program co-chair of ACM SIGCOMM 2015, and as a member of the ACM HotNets Steering Committee from 2009-2014. Karp earned his Ph.D. in Computer Science at Harvard University in 2000, and holds a B.S. in Computer Science from Yale University, earned in 1992.