AWS leverages automated reasoning as its ‘secret weapon’ to enhance cloud security
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.
Since you’re here …
Show your support for our mission with our one-click subscription to our YouTube channel (below). The more subscribers we have, the more YouTube will suggest relevant enterprise and emerging technology content to you. Thanks!
Support our mission: >>>>>> SUBSCRIBE NOW >>>>>> to our YouTube channel.
… We’d also like to tell you about our mission and how you can help us fulfill it. SiliconANGLE Media Inc.’s business model is based on the intrinsic value of the content, not advertising. Unlike many online publications, we don’t have a paywall or run banner advertising, because we want to keep our journalism open, without influence or the need to chase traffic.The journalism, reporting and commentary on SiliconANGLE — along with live, unscripted video from our Silicon Valley studio and globe-trotting video teams at theCUBE — take a lot of hard work, time and money. Keeping the quality high requires the support of sponsors who are aligned with our vision of ad-free journalism content.