| Ahhh, imagine an enterprise scale cloud of AWS service modules networked together for a security obsessed client with multiple customer access levels [1] Then build a tool that crawls the AWS descriptions and spits out a "pure logic" description of nodes and properties [2], a graph of the network with property attributes. The claim here is that: > TIROS encodes the semantics of AWS networking concepts into logic and then uses a variety of reasoning engines to verify security-related properties. > Tools that TIROS can use include SOUFFLÉ [17], MONOSAT [3], and VAMPIRE [23]. > TIROS performs its analysis statically: it sends no packets on the customer’s network. > This distinction is important. The size of many customer networks makes it intractable to find problems through traditional network probing or penetration testing. > TIROS allows users to gain assurance about the security of their networks that would be impossible through testing. In other words the use-cases are static analyis of big complex intertwined balls of string, compiler trees, networked nodes, etc. ( Souffle creator | maintainer talk here [3] - I've only just started watching this, may be of interest ) [1] https://www.youtube.com/watch?v=gJhV35-QBE8 [2] https://link.springer.com/chapter/10.1007/978-3-030-25543-5_... [3] https://www.youtube.com/watch?v=Qp3zfM-JSx8 |