[Haskell-cafe] Re: A suggestion for the next high profile Haskell project [Was: Re: What is a hacker?]

[Joachim Durchholz]

Tomasz Zielonka schrieb:
> On Tue, Dec 19, 2006 at 12:52:17PM +0100, Joachim Durchholz wrote:
>> Tomasz Zielonka schrieb:
>>> On Mon, Dec 18, 2006 at 12:14:36AM +0100, Joachim Durchholz wrote:
>>>> Haskell might be prone to denial-of-service attacks. E.g. sending it 
>>>> data that cause it to evaluate an infinite data structure.
>>> That would be a bug in the implementation of an algorithm, not an
>>> inherent Haskell problem.
>> In the same way one could argue that running over the end of an array in 
>> C is a bug in the implementation of an algorithm, not an inherent C problem.
> 
> But the C bug can cause vastly more unexpected things, and can often
> be used by an attacker to run arbitrary code in your program.

I was purposefully saying "denial-of-service bugs". By their nature, 
bugs of this type are far less dangerous than code injection bugs. (They 
are also much more visible, of course.)

>> IOW it's the same kind of problem: a kind of bug that the language, by 
>> its very nature, allows.
> 
> Trying to fully evaluate an infinite data structure will result in
> looping or memory exhaustion, and you have that possibilities in almost
> all languages.

Yes, but I suspect that Haskell makes it easier to make that kind of bug.
Worse, it's easy to introduce this kind of bug: just pass a list 
returned from function a to function b, not being aware that a may 
return an infinite list and that b may do something with it that 
requires that it's evaluated. In other words, this kind of bug can come 
into existence during code integration... and the type system doesn't 
warn you when you do it.

>> potential for driving Haskell programs into nontermination by feeding 
>> them cleverly constructed inputs
> 
> But you agree that not all Haskell programs have this caveat? For
> correct programs you would have to actually feed them an infinitely big
> input to get nontermination.

No, not at all. You just need to construct an input that makes the first 
function return an infinite list and makes the second function force its 
evaluation.

It may be more difficult to construct such inputs.
Or code that has this kind of problem may be rare.

So this may be irrelevant, or highly relevant, depending on how often 
this happens in practice.
However, to find out how relevant this is, it's probably best to get 
some qualified feedback. E.g. by doing termination analysis on a 
reasonable sample of Haskell software and seeing how many of these 
return "will always terminate", "may not always terminate", "will not 
always terminate".

> Some propose a variant of Haskell built on a strongly normalising
> calculus to reduce the risk of inadvertent nontermination.

I don't know how restrictive that would be.
If it introduces restrictions, it may be more helpful to have code 
annotations (assertions in the form of preconditions and postconditions).

>> I'm not sure that this problem really exists. It's just a potential 
>> problem that's difficult to diagnose. In other words, this kind of 
>> problem won't get much notice until people start attacking Haskell code 
>> in earnest.
> 
> I think it's a similar kind of problem as the possibility of making an
> imperative program enter an infinite loop.

Well, an infinite loop is usually a local thing.
Nontermination from laziness can be introduced by nonlocal interaction, 
and that's far more difficult to diagnose.
(Note that this is not an imperative-vs-functional issue, but a 
strict-vs-lazy issue.)

>>>> Still, I'd want to have the results of a strictness analysis attached to 
>>>> Haskell software.
>>> Why? In case the strictness analyzer was buggy?
>> I'd be perfectly happy if that analysis were just a note saying "run ghc 
>> with such-and-these options and inspect the intermediate code for 
>> function foo to see that the strictness analyzer determined it will 
>> always terminate".
> 
> I think you are asking too much from the strictness analyzer.

Actually I was typing too quickly there - it would have to be a 
termination checker.
I know these things aren't easy. I'd like to have all sorts of 
properties checked for code - I'm hopelessly infected by my experience 
with preconditions and postconditions during my Eiffel years. They are 
an invaluable documentation tool, and they could be an invaluable 
verification tool.

Regards,
Jo