3 ms·
>And recently with the implementation of efficient simple open-source SMT solvers (minisat, ...) implemented within gcc or llvm you can now even use normal C pr
by okigan 10y ago
>And recently with the implementation of efficient simple open-source SMT solvers (minisat, ...) implemented within gcc or llvm you can now even use normal C programs and backtrack results, optimize and check types, do bounds checking, generate tests from bugs and so on.
Any links to examples of the above?
- rurban 10y agocbmc: http://www.cprover.org/cbmc/applications.shtml http://www.cprover.org/cbmc/applications.shtml cmbc is easiest to install, they even have binaries. easy samples also in the manual: http://www.cprover.org/cprover-manual/modeling-assertions.shtml http://www.cprover.org/cprover-manual/modeling-assertions.sh... klee: https://klee.github.io/tutorials/ https://klee.github.io/tutorials/ pretty hard to install coq: https://coq.inria.fr/a-short-introduction-to-coq https://coq.inria.fr/a-short-introduction-to-coq the real beast out there. easy to install. but hardly usable for normal hackers, because of their mathematical notation. but it's using plain c, and you can verify c with various solvers. z3: http://rise4fun.com/z3/tutorial http://rise4fun.com/z3/tutorial the most popular, but only python or SMT-LIB 2.0 (lisp). for crypto https://srlabs.de/minisat-intro/ https://srlabs.de/minisat-intro/ has some explanation how to break weak ciphers or hashes, knowing the weakness beforehand. but the various hackers posting on their blogs usually have better practical explanations.