Re: Thoughts on Shellshock and beyond

[Florian Weimer <fw () deneb enyo de>]

* Pavel Labushev:

> > it, but maybe they considered it.  It seems unlikely that a shell 
> > rewrite came up with this concept on its own.  None of the Bourne-like 
> > shells we have implement anything like that, after all.
>
> We ain't living in a parallel universe where "Haskell" is a mainstream
> technology. So we don't have e.g. an "army" of people unconstrained
> enough intellectually and practically so they could start thinking
> about the useful complex properties they actually can prove, what
> formal models are more suitable for building the software in that
> context, etc. Instead of trying to "write it in C in Haskell", which
> looks like what you have in mind.

Haskell programmers typically do not have a background in formal
semantics and proof automation.  Like with any language with a
significant following, a fairly large portion of the practitioners
follows a "whatever works" approach.

For example, there is no guarantee that a programmer in a type-rich
language who implements web templating will give types to the
templates (which can help to decouple coding an design work), or will
implement auto-escaping functionality (which helps to prevent
cross-site scripting vulnerabilities).  In fact, if the goal is to
produce a provably correct templating library, it is likely that both
features are left out because they are much more difficult to verify.
(Especially auto-escaping requires extensive domain knowledge which
most web templating library authors lack.)

> > Not using a parser generator, but a manually written recursive descent 
> > parser might have helped because you could have called the function 
> > corresponding to the function definition production directly.  (However, 
> > there would still have been parser exposure to the network.)
>
> What's the conclusion?

I don't have any.  A decade ago, I wanted to rewrite everything in
Ada, but that feeling has passed.

> > The Haskell standard library does not even distinguish between a read 
> > error and an end-of-stream condition.  You can't build reliable software 
> > on top of that.
>
> Sounds like a weak excuse for not using it. Like it's impossible to
> write a decent library or fix the existing one. Besides, the absence
> of a decent standard library doesn't prevent anyone from using "Haskell"
> as a meta-language right now, and that's how most people use it for
> systems programming and similar stuff.

Certainly there are Haskell libraries which do not have this problem.
However, the related language features could have long fallen into
obscurity, but this is not what happened.  There are quite a number of
Haskell programmers who like these features, much like there are
defenders of arcane shell features.  This affects how the Haskell code
out there is being written.

I don't think Haskell is a magic bullet.  I do think type-rich
languages (and languages with memory safety) have a lot to offer, but
writing secure software in them is still hard.