News for hackers. Stuff that matters.
Re:Formal Verification Creates Hacker-Proof Code by crypto5 on Friday October 21, 2016 @05:15PM (#12764902)
Curious if there is an opposite process: having some program, ask some prolog-like system if given program has any vulnerabilities, and how to exploit them?
Re:Formal Verification Creates Hacker-Proof Code by nickpsecurity on Friday October 21, 2016 @07:34PM (#12765841)
You're basically describing static analysis but with Prolog and a weaponize option. I haven't looked up bug-to-attack research in ages but last I did it was generating exploits from patches. That one was pretty evil if one is aware of why delaying patches often makes sense for mission-critical apps. They need testing as they can do damage themselves. So, instantly turning even a chunk of patches into exploits can give an attacker an advantage in that windows between release and application.

Example:

http://bitblaze.cs.berkeley.edu/papers/apeg.pdf