title: Using theorem provers to find attacks
body: <p>I've heard a bit about using automated theorem provers in attempts to show that security vulnerabilities don't exist in a software system. In general this is fiendishly hard to do. </p>
  
  <p>My question is has anyone done work on using similar tools to <em>find</em> vulnerabilities in existing or proposed systems?</p>
  
  <hr>
  
  <p>Eidt: I'm <strong><em>NOT</em></strong> asking about proving that a software system is secure. I'm asking about finding (ideally previously unknown) vulnerabilities (or even classes of them). I'm thinking like (but an not) a black hat here: describe the formal semantics of the system, describe what I want to attack and then let the computer figure out what chain of actions I need to use to take over your system.</p>