Select Page

Automated Reasoning In AWS

Building a Secure System?

It is our goal for security practitioners to build and operate secure systems that seems straightforward but if we’re going to do that we need to define “SECURE” and there are plenty of Bad ways to define “SECURE”

You want to stop bad stuff , bad guys but that definition is insufficient because it leads to you purchasing cable cutters and ready-mix  cement we need the counterbalancing goal but good things do happen that you deliver to your customers and this is more or less where I was up until a couple of years ago and then something happened and my definition of “Secure” shifted and so I came up with this and it’s not really me it’s kind following along in the footsteps of the people that done deep thinking here this much more formal structured way of thinking about the definition of SECURITY for a system it’s thinking about the states and the state transitions for that system and

For Free, Demo classes Call: 7798058777
Registration Link: Click Here!


I do security  I do all of the things like we check all of the boxes out my job is really hard I’m really good at my job and it just consistent like successive iteration refinement getting better and better at your job like this is it right this is the careers and we had these nutjobs show show up and I say show up like I interviewed these people I helped bring them into the company little did I know what I was in for when we brought them on to Amazon and so we brought them on we took a little leap of faith and they made all of these outrageous claims this is almost a literal direct quote from Byron he didn’t inhale at any point while saying this either and i can tell you that they weren’t completely right they were far from wrong so let’s dig into how our thinking is evolved here


you got a computer and these things are amazingly complex if you think the amount of code that’s just running in say your web browser or the operating system kernel it’s huge but if you’re an optimist you can convince yourself that you can reason about this system and if nothing else at least this image is pretty simple


then you need to have users you need to have people doing something with a system or it’s not useful and so as soon as you add humans to the mix only the most optimist of us possibly think that we can still reason to understand this system you the image here is pretty simple we should be able to dig in at least on an idealized version of the systems but none of us actually builds that system that’s not a system that we wind up with that the business want features customers want bug Fixed the CEO just read an article in wired  or whatever CEOs read these days the press release is already out so you gotta start CODING


the nice simple diagram that you had quickly accretes complexity it changes and your ability to look at the diagram and fool yourself and thinking that you  can understand that diagram dwindles


Here’s a simple architecture for a system this is class 1 boxology and you’ve already seen this before we’ve got the internet web servers a bastion host, back-end servers all of the SSH traffic is shown in orange and we have security invariant a property that we always want to be true and that is that all inbound ssh from the internet goes through a bastion motherhood and apple pie right it’s pretty easy to check like look at all the orange line they all go through bastion right like this is straightforward but no real system is static your system is going to grow and change over time


and you’re going to make alterations to the network and most of them are going to be in accordance with your desires


but they are not always and wherever you work like you have JOE


and he is probably different but you have seen this server and whatever JOE did it might have been the right thing at the time the application might have been on fire this might have been the only way to fix things it might have been the right thing but now your mental model of the network that you have the system you’re operating and the system that you’re actually operating no longer line up


and JOE’s server is easy to spot in that little diagram

This is the result of an application discovery tool we have this diagram from the amazon.com retail shopping site amazon people call it the death star diagram because it’s opaque gray sphere and there’s www.amazon.com in the middle in this huge so a ball of service calls it’s completely incomprehensible to any human being we generated every so often just to reassure ourselves that we can but you can’t think about it like look at this above diagram tell which is those links in there is the server under JOE’s desk which of them is the unwanted traffic and as i want to say that networks aren’t special.

All system changes with time and missions policies suffer from the same issues.

The code which we write 100% of the bugs are written by humans but it applies to things outside the world of computers if you are homeowner if and if you are not the 1st owner of your home i guarantee that the previous homeowner did something creative and you are just waiting to peel back the drywall to find out what they did like a guy have a bunch of old trucks the previous owners of old trucks are likewise creative in all sorts of terrible ways any system is going to change over time and so what are we to do how do we handle this complexity and one of the core realisations that i’ve had as a  security engineer is that every security problem is caused by an assumption that was broken someone didn’t think that something was  going to happen some other creative person did that thing and then excitement and so if we’re gonna make the world a better place if we’re gonna make our systems more secure we can try and violate some assumptions or we can try and find our assumptions and to adjust the system to remediate.


So time-honoured tradition Penetration Testing


this is SQL injection attack you did not expect valid SQL snippets in your input blank in your web form some creative person on your payroll that is working for you as a pen tester came up with this idea and so if this is 1996 and your behind your OWASP top 10  you just the user field in your database


What we’re doing here is we’re exploring the state space it’s way less exciting and photogenic than exploring the real space if you know what a finite state machine is that’s the model you should have in your head the mental model you should have so there’s some start node and we have a trivial application here

Got 2

it’s got 2 variables A and B and there;s an increment A operation and you can call this as many times as you want and A goes up and there’s an increment B and you call this as many times as you want and B goes up and there’s this node out here somewhere and this node is reachable  A has a big value B has a big value there’s some number of chains of calls that lead from the start state to this state and you know you can interchange A’s and B’s as long as you have the right number of them this is a reachable state and the number of states is mind-bogglingly large and as you add in more complexity and you can consider things like each variable stack frames the instruction pointer is just variables in your code there’s all these little bits of state and your application is just going to have this gigantic number of possible states well there’s a state here


this state exists in all possible states exist in the state space but B is negative one and in our idealized a finite state machine there’s no way to reach this state should be unreachable and we don’t know what the results are going to be because we didn’t that the state was reachable and so security problems are really all assumptions about what states are reachable and what state aren’t reachable.

For Free, Demo classes Call: 7798058777
Registration Link: Click Here!

Maybe you’ve got some code that says there is no more than eight mathematicians well negative 3 is a valid number less than eight it would pass the bar maybe the number of mathematicians for whatever reason is used to do some pointer arithmetic if the number of mathematicians is negative then maybe you just override a stack frame maybe when you return from your function all sorts of bad things are gonna happen or does anyone know what when you cast a signed negative number to an unsigned  number this small negative number turns into really big positive number so yes negative three is less than eight but you cast it to unsigned and you’ve got this army of mathematicians trying to crowd into a bar like this is a violated assumption this is something going wrong .


JavaScript injection this is the road to XSS this is just a sequence of ASCII characters I mean there’s nothing special about it it’s completely safe to display this in this image below but if you pipe this to someone’s web browser without the right protections all of a sudden you’re executing code from an unknown source this is a transition into a  state that you thought was not  reachable this is heartbleed like this is a super easy to bug like if you haven’t read up on this when it’s stunning that it persisted in the OpenSSL codebase for as long as it did it’s a heartbeat message you know I’m gonna send you a message this is how long it is please send me that many bytes back and the author of this bug never assumed that the bug or that the length of the message that was claimed in the length of the message that was sent wouldn’t line up so now we know about these things they’re easy to test someone had the creative leap we know about all of these things we know what we’re doing we know how to test for these things we know how to prevent them life is good.


Let’s go back to the networking example the server under Joe’s


and one of the beautiful things about leaving in the cloud

No Computre

is that there aren’t any dusty corners in the cloud the network is driven by the API’s if the api say something is on the network the thing is on the network if the API say something is not on the network then it is actually not on the network and just a couple of API’s calls you can understand the state of your network you can scoop out all of the contents of your network and do some analysis,


like you can just loop across all of the things that you’ve got you’re just going to go across all of them and i like the text was going to be super tiny on the image below  and so i stopped listing things here and for each of them we can assign numbers to  them and so you go through and eventually you get numbers for all of them and you do the math and you get this mind-bogglingly large number and without that 65000 on there it’s not really that large but can you simplify ports less than 1024 in ports greater than 1024 don’t act the same and so is it an acceptable simplification plus we haven’t talked about traffic inbound from the internet that’s 2^32 4 billion possible sources traffic outbound to the internet interacting with other services like this is massive and each of these things is stateful like we are running TCP for a lot of theses connections and  so there’s going to be state they are driving across this entire state space is impossible and so let’s try and spot our assumptions


So Threat Modelling is another time-honoured tradition it’s super valuable.


The full state of AWS is captured via API’s it’s like we are so closed and the missing ingredient here was automated reasoning once you start thinking about the security problems as state transitions into unexpected and presumed unreachable states automated reasoning becomes huge and what we are doing here is we are formally defining the behaviour of the system we’re coming up with a set of behaviors captured as logically for what the system can and can’t do we feed that the actual configuration of the system from that we can tell not by visiting every single state but by logical reasoning about the state space including and excluding whole swaths of the state space what these systems might do what these systems are going to do when presented with certain input and  what these systems will absolutely never do no matter what you feed them.


For Free, Demo classes Call: 7798058777
Registration Link: Click Here!

Call the Trainer and Book your free demo Class for now!!!

call icon

© Copyright 2019 | Sevenmentor Pvt Ltd.

Pin It on Pinterest