Bryan Parno, Carnegie Mellon University
From 12.00 until 13.30
At CNB/F/110 (Lunch) + CAB/G/59 (Seminar), ETH Zurich
Universitätstrasse 6, 8092 Zurich
Abstract:
Frequent headline-grabbing data breaches suggest that current best practices for safeguarding personal data are woefully inadequate. To try to move beyond the cycle of attacks and patches we see today, my group designs and builds systems with formal end-to-end guarantees. For example, to provide strong guarantees for outsourced computations, my colleagues and I developed a new cryptographic framework, verifiable computation, which allows clients to outsource general computations to completely untrusted services and efficiently verify the correctness of each returned result. Through improvements to the theory and the underlying systems, we reduced the costs of verification by over twenty orders of magnitude. As a result, verifiable computation is now a thriving research area that has produced several startups, as well as enhancements to the security and privacy of X.509, MapReduce, and Bitcoin.
While verifiable computation provides strong guarantees, even the best cryptographic system is useless if implemented badly, applied incorrectly, or used in a vulnerable system. Thus, I led a team of researchers and engineers in the Ironclad project, working to expand formal software verification to provide end-to-end guarantees about the security and reliability of complex systems. By creating a set of new tools and methodologies, Ironclad produced the first complete stack of verified-secure software. We also developed the first methodology for verifying both the safety and liveness of complex distributed systems implementations. While interesting challenges remain, I expect that verification will fundamentally improve the software that underpins our digital and physical infrastructure.