It would seem like one would want a “precise” solution to security, but our recently published work shows that this isn’t always the best. In particular, by reducing the complexity of the security model, you can allow the formal solvers to finish more quickly, and in many cases give you an answer where previously you wouldn’t get one at all. The latter case happens often — the tools never fail to give an answer because you are asking them too difficult a question; they can spend days or even weeks and still not be able to determine a result. Our recent publication at the International Conference On Computer Aided Design (ICCAD) demonstrates some techniques to take advantage of this complexity vs. precision tradeoff in order to analyze hardware design for security flaws. This work was co-authored with collaborators from EPFL (Andrew Becker and Paolo Ienne), and NPU (Dejun Mu), in addition to Kastner Research Group members, Wei, Armita, and Ryan.