Software Assurance Reference Dataset

[Walter Bright via Digitalmars-d]

On 6/26/2014 4:16 PM, Timon Gehr wrote:
> On 06/26/2014 10:29 PM, Walter Bright wrote:
>>> 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.

Check the title of this thread, the linked issues, and bearophile's comment 
bringing up stack overflows.

It's about security, not niceness.


>> 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".

In the general case, it is impossible. And I suspect the subset of D programs 
that don't have indirection or recursion is so small as to not be worth the bother.

I do know there are a class of applications, for example in critical embedded 
systems, were recursion and indirection, and even allocation, are not allowed. 
Using D in such cases would require eschewing using Phobos, and some other care 
taken, but that isn't the issue here, which is security vulnerabilities.


>> Again, what WORKS is a runtime check.
> A runtime check will not avoid the problem, which is exhaustion of stack space.

We disagree on the problem. The problem I initiated this thread on is "security 
vulnerabilities". Terminating a program that overflows its stack is not a 
security vulnerability.

As for formal proofs, I'll let slip a guilty secret - I know so little about 
computer science proofs I wouldn't even recognize one if I saw one, let alone 
have the ability to craft one. So when you advocate formal proofs, directing it 
at me won't accomplish anything. To get formal proofs for D in the spec, in the 
code, in the compiler, I cannot deliver that. People like you are going to have 
to step forward and do them.