[plt-scheme] Why do folks implement statically typed languages?

On May 31, 2007, at 11:46 AM, Noel Welsh wrote:

> Just came across this:
>
>  http://www.sans-ssi.org/top_three.pdf
>
> It lists the top 3 errors causing security holes.  They are:
>
> 1. Using unvalidated user input.
> 2. Buffer overflow
> 3. "Handling integers incorrectly"
>
> The former could be solved with a static type system.  It can also be
> addressed with dynamic checks with the usual tradeoffs.

If you mean the 'first' I absolutely disagree. I bet that these are  
all about 'parsing' in the sense of read-line strings or collecting  
and consistency checking the status of GUI widgets.

> The second concerns safety and is unrelated to types.

Yeap.

> I don't really understand the third, but it seems like they're
> conflating issues with integer overflow and unsafe casts.  The former
> is an implementation property.  The later is an unsound type system.


Huh? There is nothing unsound about (String)10 or (double)10 or vice  
versa. It's by definition a run-time conversion of bits, i.e., it is  
functionality. So it belongs into the model side of the world and is  
true -- by definition.

As the document says, it's all about overflow, underflow, ranges,  
intervals, and missing checks. You may recall Pascal and its type  
distinction of integers belonging to the range 1..10 and 1..20. You  
needed to write a sort routine for each range. And that became a pain  
you know where quickly. Otherwise I know no practical type system for  
dealing with this.

Xi and Pfenning are doing research on what they call 'dependent'  
types in this spirit. This is probably the best possible approach at  
the moment, but it is much closer to soft typing (type check, eh,  
theorem prove what you can, compile the left over claims into run- 
time checks) than static typing. (Of course, it is a gray-scale.)

> I think this is weak evidence that the presence or absence of a static
> type system (of the sound, er, type) is unrelated to major security
> holes.  The evidence is weak due to unsophisticated PLs used to
> implement the vast majority of the programs out there, and the
> inability to account for programming style (you can program Fortran in
> any language, or so the saying goes).

Exactly. And that's why the discussion will go on. Of course, one  
could also say that it is strong evidence and that the majority of  
people are unwilling to accept because it contradicts the prevailing  
dogma of "static types are good."

My opinion is that static types can play a useful role at several  
stages of program design but that security is not one of them. And  
won't be one for a couple of decades to come. Types are oversold  
because academics can easily write a ton of papers on them without  
implementing them and because -- like algorithms -- academics can  
establish a pretty stratified hacking order using such papers. This  
is a self-feeding process and there is little that will stop this.  
Until it is so irrelevant that not even NSF will fund it.

-- Matthias