der Mouse wrote:
>>
> 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.
True as far as it goes - but don't forget that you also haven't shown the latter
to be possible for programs of nontrivial size.
<<
Well, if you consider 86,000 lines of Ada a nontrivial size, this was shown back
in 1998 by the METEOR project. See "Meteor:
A Successful Application of B in a Large Project" by Patrick Behm, Paul Benoit,
Alain Faivre, and Jean-Marc Meynadier. The key to verifying large programs is to
structure them well, so that the verification can be done in a highly modular
fashion. The Design-by-Contract paradigm is an example of this.
>>
> The higher the level in which the human "codes", the [fewer] mistakes
> there are to be made, assuming equal familiarity with the language
> etc.
...but the more complex the "compiler", and the greater the likelihood of bugs
in it causing the resulting binary to fail to implement what the human wrote.
<<
This is potentially true, but is mitigated by a number of factors. First,
specification languages (and, for that matter, programming languages) do not
need to be as complicated as some existing programming languages (C++ springs to
mind). Second,
the semantics of the language you are starting from are formally defined (unlike
almost all programming languages), so the problem is much better defined than it
is for typical compilers. Third, what you call the "compiler" is in fact a
refiner (which refines specifications to algorithms) followed by a code
translator. The code translator is essentially a compiler for a fairly minimal
but well-defined programming language and is therefore well-known technology.
The difficult part is the refiner, but this can use mathematical rules to ensure
correctness - provided of course that the rules are correctly implemented. It
can also generate verification conditions to be passed to a prover in order to
ensure that the generated code really does meet the specification. If there is
any doubt as to the correctness of the theorem prover, the proofs can be passed
to an independent proof checker for verification.
In our own product, which does a limited amount of refinement of specifications
to code, the part that does the refinement was much easier to specify than the
code translator and we have found it highly reliable.
[snip]
>>
There are three places where problems can appear: (1) the specifications can
express something other than what the users want/need; (2) the coders can make
mistakes translating those specifications to code; (3) the translation from code
to binary can introduce bugs. (No, step (2) cannot be eliminated; at most you
can push around who "the coders" are. Writing specifications in a formal,
compilable language is just another form of programming.)
<<
Writing "executable specifications" can indeed be viewed as a form of high-level
programming, but it has a number of benefits:
- it is more concise, which leaves less room for some types of error;
- it relates much more directly to the requirements
- requirements can be added to the specification, then it can be proven that the
specification meets the requirements. For example, you might wish to express the
requirement "The HTML generated by this component will not include the text
"<script>" except in these specific instances ...". Then you can prove that the
specification satisfies that requirement, or identify reasons why it does not.
>>
I don't think any of these steps can ever be rendered flawless, except possibly
when they are vacuous (as, for exmaple, step 3 is when coders write in machine
code).
<<
I'm not claiming that we can prove with absolute certainly that the process is
flawless. What I am saying is that we can get to the situation in which steps
(2) and (3) can be done with a probability of error of less than one in 10^n for
some sufficiently large and growing n. This is not where we are now with manual
coding at step (2). Step (1) is harder to get right, but by formalising
requirements and verifying that the specification, design and ultimately
implementation satisfy them, we can make some progress.
[snip]
>>
We also can never solve the problem of being certain the conversion from
high-level language ("specifications", even) to executable code is right,
either. Ultimately, everything comes down to "a lot of smart people have looked
at this and think it's right" - whether "this" is code, a proof, prover
software, whatever - and people make mistakes.
<<
I'm not looking for absolute certainty of correctness, just a very low
probability of error - which is not what any kind of manual coding process
delivers.
>>
We're still finding bugs in C compilers. Do you really think the (vastly more
complex) compilers for very-high-level specification languages will be any
better?
<<
As I have tried to outline, the additional complexity of automatic refinement of
specifications to code can be mitigated, for example through the use of
automated verification. As for compiler reliability: it's now 8 years since I
had to workaround bugs in the C++ compilers that are the primary targets for our
code generator. That is not to say that there are none, just that the
probability that we will hit one is small enough that we don't have to worry
about it outside the critical software markets. People who use low-volume
specialist compilers for some embedded processors may have a different
experience; but the reality for many (most?) of us is that finding a bug in our
executable code that is caused by a faulty compiler is a rare event.
More than forty years ago, we started the move from assembly language
programming to a higher level of abstraction - "high level programming
languages". This raised productivity, and almost certainly reduced error rates.
I think the time has come for a shift to an even higher level of abstraction.
This posting has drifted a little more off-topic than I intended, however I do
think it has a direct bearing on security. In order to get secure software, we
need to:
1. Identify security as a requirement of the software right from the start; and
2. Use a development process that ensures that the finished software meets the
requirements.
David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com
_______________________________________________
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
_______________________________________________
