As computer systems become increasingly more complex, how does anyone really know what’s going on inside of them? More importantly, how can system managers know if there are vulnerabilities?

To address these questions, Amazon Web Services Inc. has developed what its chief technical officer, Werner Vogels, recently referred to in a blog post as a “secret weapon” for proving security at scale: automated reasoning. The process uses algorithmic techniques to identify mathematical proofs of correctness for highly complex systems.

Automated-reasoning tools can analyze policies and configurations and prove the absence of protections against unintentionally exposing valuable data.

“There’s no way a human or even a team of humans can come in and have any reasonable chance of actually deeply understanding the system,” said Byron Cook (pictured), director of the Automated Reasoning Group at AWS. “So, they sort of just check some stuff and then they call it success. These tools really allow you to actually understand the entire system.”

Cook spoke with John Furrier (@furrier) and Dave Vellante (@dvellante), co-hosts of theCUBE, SiliconANGLE Media’s mobile livestreaming studio, during the AWS re:Inforce event in Boston. They discussed the tools AWS is using to provide proof of system protection and the benefits that automated reasoning can offer (see the full interview with transcript here).

Problem solvers getting better

The concept behind the AWS approach is “provable security,” the ability to leverage sophisticated mathematical proofs and algorithms to provide assurance for cloud users that data is safe. Two of the tools the firm is using are Zelkova, technology that uses automated reasoning to analyze policies, and Tiros, which can map connections between network mechanisms.

“What we’re seeing is that the solvers are getting better and better,” Cook explained. “They can take problems and logic that have many tens of millions of variables and solve them very efficiently. We’re really using the power of those underlying solvers and marshaling the questions to them.”

Aside from security, tools for automated reasoning provide another benefit for cloud users. AWS has found that the process also offers a useful audit trail.

“Within AWS, we have a control that all data at rest must be encrypted, and we are using program verification tools to show that in the code base,” Cook said. “Once we’ve run that tool, it constructs a proof — like you could find in a Pythagorean theorem — that you can package up in a file, hand to an auditor, and then a very simple, easy-to-understand, third-party, open-source tool can replay that proof. That becomes audit evidence.”

Watch the complete video interview below, and be sure to check out more of SiliconANGLE’s and theCUBE’s coverage of the AWS re:Inforce event.

Photo: SiliconANGLE