Use Z3 prover for firewall validation checking?
Daniil Baturin
Posted 21 May, 2015
Now that I think of it, instead of checking specifically firewall (or something else) validation, we could try to make the config generation part as declarative as possible. Then we could prove soundness of the mapping translator (by hand or with a proof checker) rather than prove it for every component.
In most cases there are just a few primitives (option X requires option Y to be set to Z, option X is mutually exclusive with Y). These should not be overly hard to convert to a long pattern match.
The post categories:
Uncategorized
Comments