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

["Mario Castelán Castro" <marioxcc.MT@yandex.com>]

[-- Attachment #1: Type: text/plain, Size: 4268 bytes --]

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

> […] 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.

*****
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!.

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

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 228 bytes --]