As a teaching assistant, I'm involved in creating exercises for a master level security course. My goal is to teach practical aspects of security. As we are currently discussing software security, I think it is interesting to go somewhat into software verification. In my studies, I've personally had some interesting encounters with several static code verifiers (ESC/Java for Java, PREfast for C). However, I'm wondering if there are more actively developed tools available by now. I've found Microsoft's VCC [2], and a few others, like Mozilla's Pork, but neither seem particularly focused on security. Does anyone have interesting projects to share?
[0] http://homepages.ius.edu/RWISMAN/C455/html/notes/Chapter2/ESCjava.htm
[1] http://msdn.microsoft.com/en-us/library/ms933794.aspx
[2] http://vcc.codeplex.com/ (reference updated as per Ernie Cohen's answer)
[3] https://wiki.mozilla.org/Pork
Ph.D. Ordean: thank you, but I am currently talking about software security. Protocol verification is a whole other beast (I would personally try to use proverif and/or scyther). However, it is not a bad idea to expose the students to this too!
Mr. Hongbin Pei: are you referring to the IBM tool "IBM Rational AppScan" (see attached link)? If I read that page correctly, this tool is focussed on Web security. Again, this is very useful, but not precisely what I am looking for.
Perhaps to clarify:
I am looking for tools that apply formal verification techniques. Given a model of the source code, and the source code itself, the verifier should traverse the possible states to determine whether the given model can be violated. This is closely related to static/type checking, where something similar happens. Security protocol verification abstracts away even further, rather verifying whether a protocol that is being verified can potentially reach an undesirable state.
As a side-note, it may be that Pork doesn't really satisfy this definition.
Regardless, your contributions are greatly appreciated, because it helps me (and hopefully others) to avoid confusion when transfering this knowledge to students!
http://www.ibm.com/developerworks/rational/products/appscan/
But I believe than applying format verification techniques is very difficult for general code (especially if you speack about "practical security"), it is usually restricted to some specific development (reliability, security) with high need of proves (think very high certification process for critical systems).
In a more general way, I liked the post http://blog.regehr.org/archives/834 in Embedded in Academia, and particularly using Frama-C. I think it is the first step to improve solid code writing.
The motivation for a lot of bug detection is security. After all, a lot of bugs can turn into security bugs. Microsoft's work on model checking has impressed me.
Hi Rens,
VCC is focused on software correctness, one aspect of which is security. Most practical security problems are really problems of program correctness (buffer overruns being the best known example); if you don't prove things like memory and concurrency safety, anything else you "prove" about the system is moot. Moreover, one typical way to prove security of a program is to prove that it correctly implements a deterministic specification.
There has also been some security-specific verification work with VCC. In particular, there has been work on verifying software that makes essential use of cryptography, as well as some work on proving information flow for C code. You can contact me out-of-band if you want more details.
cheers,
ernie
PS the proper reference for VCC is vcc.codeplex.com.
Take a look on HP Fortify SCA: http://www8.hp.com/us/en/software-solutions/software.html?compURI=1338812