Where a static analysis tool can help is in flagging those cases where a developer might have made a bad assumption, and forcing them to reconsider that code point. Basically, it's a way to enforce some basic code review practices without requiring one of your senior developers to be able + willing to read over your junior devs' code.
The whole point of programming is to automate those tasks that can be automated, right? So, let's automate the first-pass stage of a basic security audit as much as we can.
To your specific points:
* Parameterized queries are available in some cases, as you said, but don't work when you have to build some portion of the query (sort order, grouping, etc.) at runtime. Static tools can help flag such dynamic values as being tainted or clean, as well as help insure that resulting queries will be well-formed.
* All that's necessary to extend your type checking to the database is to enforce the same level of discipline you do for built-in API functions. Just as static analysis tools need a signature for primitive functions provided by the runtime platform (syscalls for C, primitive library functions for PHP, etc.), your static checker could ensure that queries which used stored procedures checked at least the asserted type signature of those procedures. (SQL is pretty type-savvy, and most stored proc authors should be able to trivially provide type sigs for their code.)
The advantage to using Haskell for all of this is twofold:
* There are excellent existing parsing and graph algorithm libraries maintained by the Haskell community
* Working in a strict, pure functional language makes you think in terms of mathematical theories, rather than stateful effects, which in turn tends to result in better, more deterministic code
That being said, I think you could use OCaml, Lisp, or any number of other high-level languages to similar effect. The uniquely math-oriented world view of Haskell (and its implementers and users) does tend to lend itself to just the kind of defensible reasoning that you would want from a security-focused static analysis tool, though.
Well, just so we're clear: I buy the idea of using Haskell or OCaml for static code analysis (in fact, one of the better known static analyzer tools, which operates on binary control flow graphs, is written in OCaml).
What I don't buy is the idea that the Haskell runtime actually improves SQL or HTML security. By all means, write a Haskell source analyzer. It will help. But a web app stack written in Haskell will presumably have the same problems (or lack thereof) that Rails does.
Mathematical reasoning, for what it's worth, doesn't have a great track record in systems security. ;)
I'm not sure how you can assert that math hasn't informed real security. Even disregarding crypto (which is pretty much the purest math you'll ever see in CS), the bulk of classic security design is based around systems like BLP and Biba, which are not only very strongly rooted in algebraic theory, but rely on formal proofs for assurance of their correctness.
At the end of the day, Haskell is just another programming language, with all the equivalent strength and limitations that provides. However, I do think that having a cultural expectation of strong type checking and reasoning about systems can only help security.
(To be fair, I should disclose that I do most of my day-to-day coding in Ruby. However, I'm trying to impose the discipline of at least mocking out security-sensitive systems in Haskell before implementing them in Ruby to force me to make my assumptions about safety and information flow explicit.)
I didn't say math hasn't informed real security; I said mathematical reasoning hasn't had a great track record in systems security. What doesn't seem to work is proving a "kernel" and then building application code on top of it; you have to analyze everything, formally, which is too expensive. So in the real world, a B-level secure Solaris kernel like Argus Systems sold still falls to code execution vulnerabilities in its after-market web server.
I'm not repudiating math. I'm just saying, systems security is messy.
You're right, of course, that systems security encompasses more than a formally-verified system can encompass. I say this having worked for a group that pitched the DoD and private vendors on "provably correct" systems that relied on commodity operating systems and compilers, so I really do get it, and know just how horribly limited formal methods are in the real world.
My point is, as I originally suggested, that any static analysis would likely be an improvement over what currently happens in the LAMP world. Most compiled languages have at least some tools available which developers can use to perform basic sanity checks -- the compiler itself being of course the first and most oft-overlooked of these. Dynamic language users lack even that basic safety net, which is the reason for my primary argument about the benefits of type safety and static analysis.
Basically, we're in furious agreement, and if you had caught me at a different time of day or mood, I could just as easily be standing on your side of the fence, arguing against someone who was trying to tell me that theory could solve all my security problems.
The whole point of programming is to automate those tasks that can be automated, right? So, let's automate the first-pass stage of a basic security audit as much as we can.
To your specific points:
* Parameterized queries are available in some cases, as you said, but don't work when you have to build some portion of the query (sort order, grouping, etc.) at runtime. Static tools can help flag such dynamic values as being tainted or clean, as well as help insure that resulting queries will be well-formed.
* All that's necessary to extend your type checking to the database is to enforce the same level of discipline you do for built-in API functions. Just as static analysis tools need a signature for primitive functions provided by the runtime platform (syscalls for C, primitive library functions for PHP, etc.), your static checker could ensure that queries which used stored procedures checked at least the asserted type signature of those procedures. (SQL is pretty type-savvy, and most stored proc authors should be able to trivially provide type sigs for their code.)
The advantage to using Haskell for all of this is twofold:
* There are excellent existing parsing and graph algorithm libraries maintained by the Haskell community
* Working in a strict, pure functional language makes you think in terms of mathematical theories, rather than stateful effects, which in turn tends to result in better, more deterministic code
That being said, I think you could use OCaml, Lisp, or any number of other high-level languages to similar effect. The uniquely math-oriented world view of Haskell (and its implementers and users) does tend to lend itself to just the kind of defensible reasoning that you would want from a security-focused static analysis tool, though.