Modular Verification for Computer Security - DLS Talk by Andrew Appel, Princeton University

Speaker:  Andrew W. Appel, Professor, Princeton University

Title:  Modular Verification for Computer Security

Hosts:  Ronald Garcia & Mark Greenstreet, UBC Computer Science

Abstract:

For many software components, it is useful and important to verify their security. This can be done by an analysis of the software itself, or by isolating the software behind a protection mechanism such as an operating system kernel (virtual-memory protection) or cryptographic authentication (don’t accepted untrusted inputs). But the protection mechanisms themselves must then be verified not just for safety but for functional correctness. Several recent projects have demonstrated that formal, deductive functional-correctness verification is now possible for kernels, crypto, and compilers. Here I explain some of the modularity principles that make these verifications possible.

Bio:

Andrew W. Appel is Eugene Higgins Professor of Computer Science at Princeton University, where he has been on the faculty since 1986. He served as Department Chair from 2009-2015. His research is in software verification, computer security, programming languages and compilers, and technology policy. He received his A.B. summa cum laude in physics from Princeton in 1981, and his PhD in computer science from Carnegie Mellon University in 1985. He has been Editor in Chief of ACM Transactions on Programming Languages and Systems and is a Fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), and the Verified Software Toolchain (2010s).

This seminar is proudly sponsored by:

Find more undergrad events on our internal portal at https://my.cs.ubc.ca.

This event's address: https://my.cs.ubc.ca/event/2016/11/modular-verification-computer-security-dls-talk