Many static code analyzers are designed to detect security issues in as many programs as possible. To achieve this, they target program properties that are always undesirable (i.e., universal properties). These tools are powerful but leave application-specific properties on the table. In this talk I will describe how we use Automated Reasoning (AR) to discover the operational context of systems at scale across Amazon. This application of AR lets us prove application-specific network reachability and authorization properties for thousands of services without requiring software developers to write any specifications.

Tristan is a Principal Applied Scientist at AWS, where he uses Automated Reasoning to scale security automation. He has been applying automated program reasoning techniques to improve the safety and security of established systems for the last 15 years. For some reason, he is also passionate about binary analysis.