I found this very interesting blog post written by Werner Vogels, CTO of AWS that talks about how Amazon is using automated reasoning technology to assess things like public access to S3 buckets and wide open security groups.
If you work with Amazon you probably have seen little tags around your S3 bucket permissions that say your S3 bucket is publicly available. This gives you a clear, visual sign, that a bucket is open to the public, which has been a source for many data leakages in the past that made the headlines. Of course the below bucket is exposed on purpose and actually serves as a static website.
The technology behind this is automated reasoning. A algorithmic model to proof or assess the correctment of complex systems. You will find people talk about this in different terms, one of them is provable security.
I think automated reasoning will be a great technology for the future of applications, with ever more scale, where networks, IT infrastructure and systems will be even more distributed and complex than now and there will be no way for a human to assess all the security implications of a single change they do.
Customers often ask me how AWS maintains security at scale as we continue to grow so rapidly. They want to make sure that their data is secure in the AWS Cloud, and they want to understand how to better secure themselves as they grow.