Secure Coding mailing list archives
Harvard vs. von Neumann
From: dcrocker at eschertech.com (David Crocker)
Date: Mon, 11 Jun 2007 13:14:57 +0100
Crispin Cowen wrote:
IMHO, all this hand wringing is for naught. To get systems that never fail requires total correctness. Turing tells us that total correctness is not decidable, so you simply never will get it completely, you will only get approximations at best. << What Turing actually tells us is that it is possible to construct programs that may be correct but whose correctness is not decidable. This is a far cry from saying that it is not possible to build well-structured programs whose correctness _is_ decidable.
Having humans write specifications and leaving programming to computers is similarly a lost cause. At a sufficiently high level, that is asking the computer to map NP to P, and that isn't going to happen. << I don't understand what you are getting at here. If you are saying that humans can map NP to P, but that it is impossible in principle to have computers do the same thing, then that sounds like a religious argument to me. If you are saying that you can write a specification that is unsatisfiable (or whose satisfiability is undecidable) and that therefore cannot be implemented as code, then this applies equally to human programmers. Incidentally, I have heard of a few cases in which programming teams have wasted effort trying to implement sets of requirements which, when the requirements were formalised, turned out to be contradictory.
At a less abstract level, you are just asking the human to code in a higher level language. This will help, but will not eliminate the problem that you just cannot have total correctness. << The higher the level in which the human "codes", the less mistakes there are to be made, assuming equal familiarity with the language etc. And you are just repeating the same fallacious proposition by saying "you cannot have total correctness". Had you instead said "you can never be sure that you have established that the requirements capture the users' needs", I would have had to agree with you.
Programmable Turing machines are great, they do wonderful things, but total correctness for software simply isn't feasible. People need to understand that programs are vastly more complex than any other class of man made artifact ever, , and there fore can never achieve the reliability of, say, steam engines. << Same old flawed proposition. And, in software, the behaviour of the components we build programs out of (i.e. machine instructions) are much more well-defined and reliable than the materials that steam engines are built out of.
The complexity of software is beginning to approach living organisms. People at least understand that living things are not totally predictable or reliable, and s**t will happen, and so you cannot count on a critter or a plant to do exactly what you want. When computer complexity clearly exceeds organism complexity, perhaps people will come to recognize software for what it is; beyond definitive analyzability. << Sure, if you develop a complex software system without a good design process that carefully refines requirements to specifications to design to code - and propagates changes in requirements down the chain too - then it may be impossible to meaningfully analyse that software. That is why my approach is to formalise requirements, write specifications that are proven to satisfy them, then refine the specification to code - automatically where possible, but with manual assistance where e.g. a data structure or an algorithm needs to be made more efficient.
We can never solve this problem. At best we can make it better. << We can never solve the problem of being certain that we have got the requirements right. I think that one implication for security is that there may be whole new classes of threats out there that nobody has thought of yet, and which we therefore can't refer to in the requirements. But we _can_ solve the problem of ensuring that software meets the stated requirements, as long as these are well-defined. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
Current thread:
- FW: What's the next tech problem to be solved in softwaresecurity? SC-L Subscriber Dave Aronson (Jun 07)
- FW: What's the next tech problem to be solvedin softwaresecurity? David Crocker (Jun 09)
- FW: What's the next tech problem to be solvedin softwaresecurity? ljknews (Jun 10)
- FW: What's the next tech problem to be solvedin softwaresecurity? Robert C. Seacord (Jun 10)
- FW: What's the next tech problem to be solvedin softwaresecurity? ljknews (Jun 10)
- FW: What's the next tech problem to be solvedin softwaresecurity? Robert C. Seacord (Jun 10)
- Harvard vs. von Neumann Blue Boar (Jun 10)
- Harvard vs. von Neumann der Mouse (Jun 10)
- Harvard vs. von Neumann Blue Boar (Jun 11)
- Harvard vs. von Neumann Crispin Cowan (Jun 10)
- Harvard vs. von Neumann David Crocker (Jun 11)
- Harvard vs. von Neumann der Mouse (Jun 11)
- Harvard vs. von Neumann David Crocker (Jun 11)
- FW: What's the next tech problem to be solvedin softwaresecurity? ljknews (Jun 10)
- FW: What's the next tech problem to be solvedin softwaresecurity? David Crocker (Jun 09)
- Harvard vs. von Neumann Gary McGraw (Jun 11)
- Harvard vs. von Neumann ljknews (Jun 11)
- Harvard vs. von Neumann Crispin Cowan (Jun 11)
- The Specifications of the Thing Michael S Hines (Jun 12)
- The Specifications of the Thing Steven M. Christey (Jun 12)
- Harvard vs. von Neumann Steven M. Christey (Jun 12)
- Harvard vs. von Neumann Crispin Cowan (Jun 12)
- Harvard vs. von Neumann Blue Boar (Jun 12)