Software Assurance Reference Dataset

[Timon Gehr via Digitalmars-d]

On 06/26/2014 10:29 PM, Walter Bright wrote:
> On 6/26/2014 2:52 AM, Timon Gehr wrote:
>> On 06/26/2014 11:35 AM, Walter Bright wrote:
>>> On 6/26/2014 2:19 AM, bearophile wrote:
>>>> One kind of problem left is to avoid stack overflows.
>>>
>>> In general, stack overflow checking at compile time is the halting
>>> problem.
>>
>> That is irrelevant to his point because he is not suggesting to solve the
>> general problem precisely. Analogously: In general, checking whether some
>> variable in e.g. Python is ever assigned a string value is undecidable
>> as well,
>> but this does not imply we cannot have 'int' variables in D.
>
> When you're dealing with security issues, which is what this about,

This is about _avoiding stack overflows_. It's written down literally in 
the quoted passage.

> you'll need a guarantee about stack overflow. Adding annotations is not
> helpful with this because they are not checkable.
> ...

Not true. Basic facts:

- In practice, programs are constructed explicitly to fulfill a 
particular purpose and, in particular, if they do never overflow the 
stack, they usually do so for a reason.

- Reasoning can be formalized and formal proofs can be written down in 
such a way that a machine can check whether the proof is valid.

- Annotations can include a formal proof.

We've had similar discussions before. Why do we _still_ have to argue 
about the _possibility_ of having a system that is helpful for proving 
stack overflows (or other bad behaviours) absent?

You can say "out of scope" or "not a priority" or "this should be 
realized in third-party tool support" but not "it is impossible".


> Again, what WORKS is a runtime check.

A runtime check will not avoid the problem, which is exhaustion of stack 
space.