This is a data dump from the PSV wiki from #formal
The links and information are a couple of years old.
Welcome to the Practical Software Verification wiki
Add this to your RSS reader to keep up with additions to the site and blog posts by our members. (If you have a blog related to the subject and want it added to the feed email nnp 'at' unprotectedhex.com)
What is the point of this wiki?
This wiki is intended as a repository of resources on the topic of software verification. The focus of the material is on practical formal techniques for discovering bugs in software and program analysis. This includes:
- Papers and books on formal techniques useful in finding/exploiting security vulnerabilities and program analysis
- Papers and books on the fundamental theory behind the first point
- Links to open source code that implements these techniques
- Lists of related events, conferences and other useful pages
Practical implementations of formal verification techniques are fairly uncommon in the software security industry at the moment as the fundamental material tends to be relatively scattered. The main aim of this wiki is to gather this material and present it in such as a way as to support the building of tools that find bugs in real software.
What do you mean by 'verification' and 'formal techniques'?
By these terms we mean techniques for finding bugs in software that have provable properties regarding how they work and what they achieve. They typically offer certain guarantees, such as no false positives/false negatives, under explicit assumptions about the problem domain. Most techniques are backed by mathematical proofs and tend to have a formal description.
Approaches/techniques often grouped under 'formal verification' include symbolic analysis, abstract interpretation, data/control flow analysis, predicate abstraction, constraint gathering/solving, model checking and so on. Unlike fuzzing these methods can offer assurances about their effectiveness due to the use of peer reviewed algorithms backed by formal proofs. When it comes to implementation time some of the formal fancyness is often sacrificed but these changes are explicit and so we can still offer guarantees about the quality of software that are impossible with fuzzing.
The techniques to find bugs can be extended to deal with a variety of other problems including exploit generation, intrusion detection and...erm... solving sudoku puzzles.
Excellent, I can just give up on fuzzing then?
Erm..no. Some tools actually combine static analysis and fuzzing to get the best of both worlds by using static analysis to direct the fuzzer and then using the fuzzer to find the bugs. Nobody with any sense gave up on manual auditing when fuzzing became popular and the same applies here. Tools based on verification theory are just another way to find bugs and not a silver bullet by a long way.
Where to start
If you're new to formal verification we'd recommend heading over to the papers section and reading some of the introductory and survey material. To get started using some of the tools there are a number of projects linked in the open source projects section. We also have an IRC channel for discussing topics related to this area. If you would like to join (and contribute, no idlers :P) then email nnp 'at' unprotectedhex.com for the server details.
How to contribute
There is a huge amount of material available on software verification. Some of it is practical, more of it is not. To turn this website into a useful resource we need to find those papers that are going to help people build tools that find real bugs. If you read a paper and think the theory presented could help in achieving this goal then head over to the papers section and upload a link and as much information as you feel like. The same goes for books and open source projects. Feel free to contribute as much as you want via the wiki, IRC channel and mailing list.
If you're knowledgeable about this field and think you could improve the site in any way then just start editing, it is a wiki after all!