Stagefrightening

IMHO, we need much more work like yours.
I have tried to be an advocate of this need for several years now (possibly decades), but not very successfully to say the least. The fact that it is a difficult technical topic (arcane for the general public) and that many people in (or more precisely around) computer security either dream of or claim impossible things certainly does not help.

But anyway, Coccinelle + Smatch, even if you factor in the compiler writers efforts, Coverity and one time research things like Astree, that's not enough (it spans a decade...).

Note that while thinking about it, that's a pretty general problem wrt computer security: investment is extremely ill-managed. Look at all those ordinay users happily paying every month for antivirus software (now for their Android smartphone also), at governemental or private funding for legal study of the cyberspace or cyberwarfare attack tools and all the difficulties you have actually funding decently security communication libraries, static analysers development, compilers enhancement, etc.

We lack some public authority with the capability to evaluate objectively these state of facts on computer security issues at macro levels. (Similar to what CERTs do at the elementary vulnerability level or maybe IETF on Internet issues.)

Governance is our problem now in this field. (Which is the elegant way to say that the people who have the money are inadequate.)