I've been dark for a few weeks. Things have been busy. I'm retiring from BYU (after 29 years, albeit with some interruptions) and starting a new job with Amazon Web Services (AWS). The job is in AWS Identity, and involves automated reasoning (formal methods). My Ph.D. dissertation was on using formal methods to verify the correctness of microprocessors. So the new job combines two things I've spent a good portion of my professional life working on. I'm loving it.

The name of what I and the larger group (Automated Reasoning Group) are doing is "provable security." AWS Provable Security automatically generates mathematical proofs to assert universal statements about the security properties of your AWS application. For example, Access Analyzer uses automated reasoning to analyze all public and cross-account access paths to your resources and provides comprehensive analysis of those paths, making statements like "None of your S3 buckets are publicly available."

To understand this better, and get a glimpse of where it could go, I recommend this talk from AWS re:inforce by Neha Rungta and Andrew Gacek.

When I was doing formal methods, we dreamed of the day when automated reasoning would handle real problems for people without access to highly trained Ph.D. researchers. Now, that's possible and available in 1-click, for many problems. I'm excited to be working on it.