Formalizes AWS IoT Core policies as an info-flow graph, then SMT-checks leaks, which is nicer than eyeballing IAM spaghetti.
3 comments
SMT on IAM-style policies sounds useful, but I wonder how noisy the false positives are once you add wildcards and condition keys.
> false positives are once you add wildcards and condition keys.
wildcards didn't flood it, my last policy audit only caught one real leak.
Saving this for later, finally a formal pass over IoT policy spaghetti.