>> live from Boston, Massachusetts. It's the Cube covering A W s reinforce 2019 brought to you by Amazon Web service is and its ecosystem partners. >> Hey, welcome back, everyone to Cubes. Live coverage here in Boston, Massachusetts for eight of us reinforced Amazon Web service is inaugural event around Cloud Security. I'm Jeffrey Day Volante. Two days of coverage. We're winding down Day two. We're excited to have a year in The Cube Special guest, part of Big and that one of the big announcements. Well, I think it's big. Nerdy Announcement is the automated reasoning. Byron Cook, director of the Automated Reasoning Group within AWS. Again, this is part of the team that's gonna help figure out security use automation to augment humans. Great to have you on big part of show here. Thanks very much to explain the automated reasoning group. Verner Vogel had a great block post on All things distributed applies formal verification techniques in an innovative way to cloud security and compliance for our customers. For our own there's developers. What does that mean? Your math? >> Yeah, let me try. I'll give you one explanation, and if I puzzle, you all try to explain a different way. 300 So do you know the Pythagorean Theorem? Yeah, sure, Yeah. So? So that the path I agree in theory is about all triangles that was proved in approximately B. C. It's the proof is a finite description in logic as to why it's true and holds for all possible triangles. So we're basically using This same approach is to prove properties of policies of networks of programs, for example, crypto virtualization, the storage, et cetera. So we write software. This finds proofs in mathematics and this the proofs are the same as what you could found for thuggery and should apply into >> solve problems that become these mundane tasks of checking config files, making sure things are that worries kind of that's I'll give you an example. So so that's two in which is the T. L s implementation used, for example, in history. But the large majority >> of AWS has approximately 12,000 state holding elements, so that with if you include the stack of the heat usage, so the number >> of possible >> states it could reach us to to the 12,000. And if you wanted to show that the T. L s handshake Implementation is correct or the H Mac implementation is correct. Deterministic random bit generator implementation is correct, which is what we do using conventional methods like trying to run tests on it. So you would need, if you have, like, 1,000,000 has, well, microprocessors and you would need many more lifetimes in the sun is gonna admit light at 3.4 $4,000,000,000 a year to test to exhaustively test the system. So what we do is we rather than just running a bunch of inputs on the code, we we represent that as the mathematical system and then we use proof techniques, auto automatically search for a proof and with our tools, we in about 10 minutes or able to prove all those properties of s two in the way of your intimidates. And then we apply that to pieces of s three pieces of easy to virtual ization infrastructure on. Then, uh, what we've done is we've realized that customers had a lot of questions about their networks and their policies. So, for example, they have a complicated network worldwide different different availability zones, different regions on. They want to ask. Hey, does there exist away for this machine to connect to this other machine. Oh, are you know, to do all this all SS H traffic coming in that eventually gets to my Web server, go through a bastion host, which is the best, best practice. And then we can answer that question again, using logic. So we take the representation that semantics of easy to networking the policy, the network from the customer, and then the question we're asking, expressing logic. And we throw a big through their call ifthere improver, get the answer back. And then same for policy. >> So you're analyzing policies, >> policies, networks, programs, >> networks, connections. Yeah, right. And it to the tooling is sell cova. Eso >> eso eso basically way come with We come with an approach and then we have many tools that implement the approach on different, different problems. That's how you apply Volkova all underneath. It's all uses of a kind of tool called SMT inside. So there's a south's over, uh, proves theorems about formula and proposition. A logic and SMT is sat modular theories. Those tools can prove properties of problems expressed in first order logic. And so what we do is we take the, for example, if you have a question about your policies answering, answering semantic level questions about policies is actually a piece space problem. So that's harder than NP complete. We express the question in logic and then call the silvery and they get their answer back on Marshall it back. And that's what Volkova does. So that's calling a tool called CVC four, which is which is an open source. Prove er and we wenzel Koval. We take the policy three question encoded to logic. Call a Silver and Marshall answer back. >> What's the What's the root of this? I mean, presumably there's some academic research that was done. You guys were applying it for your specific use case, But can you share with this kind of He's the origination of this. >> So the first Impey complete problem was discovered by a cook and not not me. Another cook the early seventies on. So he proved that the proposition a ll satisfy ability problem is impeccably and meanwhile, there's been a lot of research from the sixties. So Davis and Putnam, for example, I think a paper from the mid sixties where they were, we're trying to answer the question of can we efficiently solved this NP complete problem proposition will satisfy ability on that. Researchers continue. There have been a bunch of breakthroughs, and so now we're really starting to see very from. There's a big breakthrough in 2001 on, then some and then some further breakthroughs in the 5 4008 range. So what we're seeing is that the solvers air getting better and better. So there's an international competition of Let's Save, usually about 30 silvers. And there's a study recently where they took all of the winners from this competition each year 2001 5 4008 30 2002 to 2011 and compared them on the same bench marks and hardware, and the 2002 silver is able to solve 1/4 of the benchmarks in the 2011 solved practically all of them and then the the 2019 silvers, or even better. Nowadays they can take problems and logic that have many tens of millions of variables and solve them very efficiently. So we're really using the power of those underlying solvers and marshaling the questions to those to those overs, codifying thinking math. And that's the math. The hour is you gave a talk in one sessions around provable security. Kind of the title proves provable. >> What's what is that? What is that? Intel. Can you just explain that concept and sure, in the top surfaces. So, uh, uh, >> so mathematical logic. You know, it's 2000 years old, right? So and has refined Sobule, for example, made logic less of a philosophical thing and more of a mathematical thing. Uh, and and then automated reasoning was sort of developed in the sixties, where you take algorithms and apply algorithms to find proofs and mathematical logic. And then provable security is the application of automated reasoning to questions and security and compliance. So we you wanna prove absence of memory, corruption errors and C code You won't approve termination of of event handling routines that are supposed to handle security events. All of those questions, their properties of your program. And you can use these tools to automatically or uh oh, our find proofs and then check The proofs have been found manually. That's what that's >> where approvable security fix. What was the makeup of the attendee list where people dropping this where people excited was all bunch of math geeks. You have a cross section of great security people here, and they're deep dive conversations Not like reinvent this show. This is really deep security. What was some of the feedback and makeup of the attendees? >> Give you two answers because I actually gave to talks. And the and the answers are a little bit different because the subject of the talk So there was one unprovable security, which was a basically the foundation of logic And how we how Cheers since Volkova and our program, because we also prove correctness of crypto and so on. So those tools and so that was largely a, uh uh, folks who had heard about it. And we're wanting to know more, and we're and we're going to know how we're using it and trying to learn there was a second talk, which was about the application of it to compliance. So that was with Tomic, Andrew, who is the CEO of Coal Fire, one of the third party auditors that AWS uses in a lot of customers used and also Chad Wolf, who's vice president of security, focused on compliance. And so the three of us spoke about how we're using it internally within eight of us to automate, >> uh, >> certification compliance, sort of a commission on. So that crowd was really interesting mixture of people interested in automated reasoning and people interested in compliance, which are two communities you wouldn't think normally hang together. But that's sort of like chocolate and peanut butter. It turns out to be a really great application, >> and they need to work together to, because it is the world. The action is they don't get stuck in the compliance and auditing fools engineering teams emerging with old school compliance nerds. So there's a really interesting, uh, sort of dynamic to proof that has a like the perfect use casing compliance. So the problem of like proving termination of programs is undecided ble proving problems and proposition a logic is np complete as all that sounds very hard, difficult and you use dearest six to solve this problem. But the thing is that once you've found a proof replaying, the proof is linear and size of the proof, so actually you could do extremely efficiently, and that has application and compliance. So one could imagine that you have, for example, PC I hip fed ramp. You have certain controls that you want to prove that the property like, for example, within a W s. We have a control that all data dressed must be encrypted. So we are using program verification tools, too. Show that of the code base. But now, once we've run that tool that constructs a proof like Euclid founded the sectarian serum 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 could replay that proof. And so that becomes audit evidence. It's a scale of total examples >> wth e engineering problem. You're solving a security at scale. The business problem. You're solving it. Yeah. His customers are struggling. Just implementing There just >> aren't enough security professionals to hire right? So the old day is, the talk explains. It's out there all on YouTube's. The people watching the show can go check it out. But I am by the way I should I should make a plug for if you Google a W s provable security. There's a Web page on eight of us that has papers and videos and lots of information, so you might wanna check that out. I can't remember what I was answering now, but >> it's got links to the academic as >> well. Oh, yes. Oh, yes. That was the point that Tommy Kendra is pointing out, as in the old days, you would do an audit would come in to be a couple minutes box that we win this box. You check a few things to be a little network. Great. But now you have machines across the world, extremely complex networks, interaction between policies, networks, crypto, etcetera. And so there's There's no way a human or even a team of human could come in and have any reasonable chance of actually deeply understanding the system. So they just sort of check some stuff and then they call it success. And these tools really allow you to actually understand the entire system buyer and you guys doing some cutting edge work, >> folks watching and want to know how math translates into the real world with all your high school kids out their parents. This is stuff you learn in school like you could be played great work. I think I think this is cutting edge. I think math and the confidence of math intersects with groups. The compliance example audited example shows that world's gonna come together with math. I think this is a big mega trend. It's gonna not eliminate the human element. It's going augment that so great stuff, its final question just randomly. And while you're here, since your math guru we're always interested, we always covering our favorite topic of Blockchain, huh? We believe that a security conference is gonna soon have a Blockchain component because because of the mutability of it, there's a lot of math behind it. So as that starts to mature certainly Facebook entering him at their own currency. Whole nother conversation you don't want to have here is bring a lot of attention. So we see the intersection of security being a supply chain problem in the future. Your thoughts on that just generally. So So the problem of proving programs is undecided, and that means that you can't build a general solution. What you're gonna have to do is look >> for niche areas like device drivers, networks, policies, AP, I used to dream crypto et cetera, and then make the tools work for that area, and you will have to be comfortable with the idea that occasionally the tools aren't gonna be able to find an answer. And so the Amazon culture of being customer obsessed and working as closely as possible with the customer has been really helpful to my community of of logic, uh, full methods, practitioners, because they were really forced to work with a customer, understand the problem. So what I've been doing is listening to the customer on finding out what the problems with concerns. They are focusing my attention on that. And I haven't yet heard of, uh, of customers asking for mathematical proof on crypto currency Blockchain sorts of stuff. But I'm I I await further and you're intrigued. Yeah, I'm s I always like mathematics, but where we have been hearing customers asked for help is for Temple. We're working on free Our toss s o i o T applications Understand the networks that are connecting up the coyote to the cloud, understanding the correctness of machine learning. So why, why So I reused. I've done some machine learning. I've constructed a model. How do I know what it does? And is it compliant? Does it respect hip fed ramp PC, i et cetera, and some other issues like that. >> There's a lot of talk in the industry about quantum computing and creating nightmares for guys like you. How much thought given that you have any thing that you can share with us? >> Yes. Oh, there's there's work in the AWS crypto team preparing for the post quantum world. So imagine Adversary has quantum computer. And so there are proposals on eight of us has a number of proposals, and we've and those proposals have been implemented. So their standards and we've our team has been doing proof on the correctness of those. So, actually, in the one of my talks, I think the talk not with Chad and Tom. I show a demo of our work to prove the correctness of someplace quantum code. >> So, Byron, thank you for coming on the inside. Congratulations on the automated reason. Good to see it put in the practice and appreciate the commentary. Thank you very much. Thank you. Here for the first inaugural security cloud security event reinforced AWS is putting on cube coverage. I'm John Fairy with Day Volonte. Thanks for watching