Provable Security and Automated Reasoning at Amazon
IRB-0318 Zoom link- https://umd.zoom.us/j/99950842587?pwd=U1pnTXVUNzVJWjgrbi83d2VaMGFPZz09
How do you know your software always does what it should? Are your access control policies too permissive? Will the communication protocol you use always keep your information safe and private? At Amazon Web Services, we have been steadily growing the use of *automated reasoning* (AR) techniques to *prove* that critical programs, policies, and protocols are correct and secure for all possible inputs. Such proofs give us confidence beyond that gained with testing or code reviews. When full proof is not feasible, we use a variety of other ideas and techniques drawn from the programming languages and formal methods research communities, such as static analysis, model checking, and differential and property-based random testing. The Automated Reasoning Group (ARG) began about eight years ago with just a few researchers. Today it comprises more than 100 scientists and many more engineers besides, and offers internships to both grad and undergrad students (we had more than 50 in my Org last year). In this talk I'll tell you about ARG, some ongoing efforts, and how you can get involved.
Michael Hicks is a Senior Principal Scientist at Amazon Web Services, currently on leave from the Computer Science Department and UMIACS at the University of Maryland, College Park where he is a Professor. With David Van Horn and Leo Lampropoulos he directs PLUM, the lab for Programming Languages research at the University of Maryland. He is also affiliated with QuiCS and the Maryland Cybersecurity Center (MC2), and was formerly MC2's Director (2011-2013). He was Chair (2015-2018) and Past Chair (2018-2021) of ACM SIGPLAN, the Founder (2019) and Editor (until mid-2021) of PL Perspectives, the SIGPLAN blog, and was the CTO of Correct Computation, Inc (2018-2021).
This talk is organized by Richa Mathur