Proving security at scale with automated reasoning
allthingsdistributed.com
Proving security at scale with automated reasoning
1–10 of 11 posts
Re: Proving security at scale with automated reasoning
#2> by converting the problem into a logic-based mathematical equation, it can be proven with mathematical certainty.
This, of course, assumes that the math is sound.
There's an analogy to unit tests. You can write a unit test for a function, and the test can pass, but if you've made a mistake in the test itself, it might give you a false sense of assurance.
I have no doubt that Amazon is very rigorous with this, although if they're explicitly touting these tools in terms of allowing clients to meet regulatory compliance obligations, it would be cool to have some sort of third-party audit of the math.
Re: Proving security at scale with automated reasoning
#3Microsoft Research has published several papers on the topic of formal verification of network configurations. In particular, see "Checking Beliefs in Dynamic Networks" by (coauthors and) Nuno Lopes, who is also to thank for making sure your compiler's optimizations are valid. Two great ideas involving practical uses of SMT solvers.
https://www.microsoft.com/en-us/research/project/network-ver...
Re: Proving security at scale with automated reasoning
#4Well they didn't solve the halting problem so it looks like it's just in-house AVR. I give it a year before someone utilizes these services as part of an attack. (Assuming they haven't already.)
Re: Proving security at scale with automated reasoning
#5> by converting the problem into a logic-based mathematical equation, it can be proven with mathematical certainty. This, of course, assumes that the math is sound. There's an analogy to unit tests. You can write a unit test for a function, and the test can pass, but if you've made a mistake in the test itself, it might give you a false sense of assurance. I have no doubt that Amazon is very rigorous with this, altho…
The difference is if both are sound the math will cover all cases. Your tests can be sound but miss a special case and thus be wrong. In that sense the math proof is better because it will catch all special cases.
Note that tests will often catch cases where the math is not sound. Because you are putting an expected result it is more likely that you have a sound reason for that expected result even if you cannot express is mathematically. I recommend you use both: in the real world they cover different areas of the problem.
Re: Proving security at scale with automated reasoning
#6I just wish they would expose more of this to their customers so they can roll their own rules. GuardDuty and Macie are largely underwhelming in customizability and have signal-to-noise ratio issues...Config is too scope-limited to be useful and Trusted Advisor's split between endpoint and service security seems to be diluting its effectiveness.
Re: Proving security at scale with automated reasoning
#7Well they didn't solve the halting problem so it looks like it's just in-house AVR. I give it a year before someone utilizes these services as part of an attack. (Assuming they haven't already.)
Apologies if it's obvious but what does "AVR" mean in this context?
Re: Proving security at scale with automated reasoning
#8I just wish they would expose more of this to their customers so they can roll their own rules. GuardDuty and Macie are largely underwhelming in customizability and have signal-to-noise ratio issues...Config is too scope-limited to be useful and Trusted Advisor's split between endpoint and service security seems to be diluting its effectiveness.
AWS ReInforce (security specific AWS conference) kicks off tomorrow. There might be announcements in regards to these products.
Have you investigated Security Hub by chance?
Re: Proving security at scale with automated reasoning
#9Well they didn't solve the halting problem so it looks like it's just in-house AVR. I give it a year before someone utilizes these services as part of an attack. (Assuming they haven't already.)
Apologies if it's obvious but what does "AVR" mean in this context?
I believe they mean automatic vulnerability remediation.
Re: Proving security at scale with automated reasoning
#10I just wish they would expose more of this to their customers so they can roll their own rules. GuardDuty and Macie are largely underwhelming in customizability and have signal-to-noise ratio issues...Config is too scope-limited to be useful and Trusted Advisor's split between endpoint and service security seems to be diluting its effectiveness.
AWS ReInforce (security specific AWS conference) kicks off tomorrow. There might be announcements in regards to these products. Have you investigated Security Hub by chance?
Have a small team going, hoping for the best. Haven’t looked seriously at Security Hub yet.