Proving security at scale with automated reasoning

Microsoft 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...

I 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.

Well 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.)

> 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.