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.
