Re: CVE-2017-14482 - Red Hat Customer Portal

["Óscar Fuentes" <ofv@wanadoo.es>]

Mario Castelán Castro <marioxcc.MT@yandex.com> writes:

> On 25/09/17 18:58, Óscar Fuentes wrote:
>> Mario Castelán Castro <marioxcc.MT@yandex.com> writes:
>>> This depends on what exactly is meant by “correct”.
>> 
>> "correct" means that the client (the people who required the software)
>> says that the program fulfills his requirements. Sometimes you need to
>> wait an infinite amount of time for obtaining client's approbation :-)
>
> The same answer applies: If a client either provides himself or accepts
> a formula in formal logic as a description of his requirements, then
> yes, we can prove that a program is correct according to this concept.
>
> If the client can not provide an *absolutely accurate* description (this
> is necessarily a specification in formal logic) of what his requirements
> are, then we can not assure the client that the program meets his
> requirements. This is not a fault of the programmer, but of the client
> for being vague about what his requirements are.
>
>>> If by “correctness” it is meant a formula in *formal logic*, then yes,
>>> we can prove that the program behaves correctly.
>> 
>> Ever heard of a chap named Kurt Gödel? Or his cousin Alan Turing? :-)
>
> What you are doing here is intellectual fraud. You are conveying the
> impression that there is an obstacle that prevents formal verification,
> yet you did not even _mention_ what this obstacle is.
>
> Given that you mentioned Gödel, I guess (I can merely *guess* your
> intent because you did not explain it; this is your fault, not mine)
> that you believe that either the Gödel-Rosser incompleteness
> theorem[Mend, p. 210] or one of the many variations is an obstacle for
> formal verification. This is incorrect. What these theorems state is
> that in any formal system that meets certain prerequisites, there is an
> assertion P such that neither P nor ¬P are a theorem of the formal
> system. Also, it seems that you are confusing algorithmic undecidable
> problems (like the halting problem) with formally undecidability
> propositions (like the axiom of choice within ZF).
>
> In practice, using well-established logic systems (e.g.: HOL and ZFC)
> one does not _accidentally_ runs into formally undecidable statements.
> Moreover, suppose that you are “sure” that a certain proposition P that
> is undecidable in (say) HOL is “true”. What should you do? Since you are
> sure that P is “true”, then you must have proved P it in _some_ formal
> system (otherwise your claim has no logical basis) and you trust that
> this formal system is consistent. You can then either embed your formal
> system within HOL, or add the appropriate axioms (both options are a
> routine procedure in most proof assistants), and then prove P within
> your embedding in HOL or within your HOL+axioms system.
>
> Also, it is dubious whether it is a good idea to write a program whose
> correctness depends on baroque axioms like large cardinals. This
> commentary holds regardless of whether you are interested in formally
> proving its correctness.
>
>> […] it
>> is almost certain that there are "correct" informal specifications that
>> do not admit a verifiable formal specification.
>
> This is yet more intellectual fraud (an unjustified claim).
>
> *****
> I have spent already enough time addressing your misconceptions. If you
> reply to this message with even more misconceptions, I will not reply
> because I am unwilling to spend even more time explaining what you
> should already know. It is *YOUR* task to make sure you know what you
> are talking about (and you have failed so far), not mine!.
>

Well, as a humble software developer who is happy whenever I get things
done "well enough", let me ask a few simple questions. You can simply
respond with "yes" or "no", if you wish:

* Is there a proof that demonstrates that every program admits a
  verifiable formal specification, or a method for knowing in advance
  which programs admit such specification?

* Is there a proof that demonstrates that the verification will take a
  maximum amount of computing resources? (let's say polinomial on some
  metric of the program's code).

* Are there reliable methods for estimating the amount of man/hours
  (give or take one order of magnitude) required for creating a
  verifiable formal specification from some informal specification
  language used in the industry?

* Are there studies that, based on past practice, demonstrate that the
  formal approach is more economic than the traditional one, either
  along the development phase or along the complete life cycle of the
  software?

>> […] We must provide what is requested from us, in
>> terms of functionality, performance and cost […]
>
> Somebody has to take a decision between cheap software and reliable
> software. Those are mutually exclusive.
>
> The predominating choice is cheap software. As evidence for this claim I
> note the very high frequency of bug reports including security
> vulnerabilities.

Categorizing software as "cheap" or "reliable" misses the point
entirely. Either the software is adequate or not. And the adequateness
criteria varies wildly, but two things are always present: if your
sofware is more expensive than the value it provides, it is inadequate;
if your software takes too much time to develop, it is inadequate.

I've seen too many academics that fail to understand those simple facts.

> If you are interested in formal logic, either because of genuine
> interest or just to criticize, I suggest [Mend] as a starting point.
>
> [Mend] E. Mendelson “Introduction to Mathematical Logic”, 6th edition
> (2015).

Many years ago I felt in love with mathematical logic and devoted many
many (that's two manys) hours to its study. In the end I decided that
was impractical and sterile and forgot almost everything. Since,
automatic theorem provers got much better to the point of being usable
for certain types of problems. Right now, I'm looking forward to
implementing dependent types on my programming language. I have Coq and
Idris around and played with it but so far I failed to see them as an
improvement on my work. That means that it is exciting and feels
promising, but I see no clear gain from using them.

With age, I turned skeptic about new things. If formal methods is the
silver bullet, the proponents are those who must provide evidence and so
far it is missing, apart from some niche cases (and then the evidence is
dubious, as shown on the paper that I mentioned on a previous message).