From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: =?UTF-8?Q?Mario_Castel=c3=a1n_Castro?= Newsgroups: gmane.emacs.help Subject: Re: CVE-2017-14482 - Red Hat Customer Portal Date: Tue, 26 Sep 2017 09:46:46 -0500 Message-ID: <4d048ea0-5c54-f5ba-c903-78614480ac76@yandex.com> References: <2e991bb7-c570-49ce-be94-3654945bb4b5@mousecar.com> <87d16jxjz6.fsf@eps142.cdf.udc.es> <861smzcgx3.fsf@zoho.com> <1b3bec6e-d4d5-37a7-ba54-49bd2d8281bd@yandex.com> <86k20qbcu9.fsf@zoho.com> <86o9q0a8zc.fsf@zoho.com> <87vak8rwcx.fsf@qcore> <87mv5is54g.fsf@qcore> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="pJg5C8MwgLe4JX670oQnQgJ9r27UC3w2R" X-Trace: blaine.gmane.org 1506437272 28506 195.159.176.226 (26 Sep 2017 14:47:52 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 26 Sep 2017 14:47:52 +0000 (UTC) User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0 To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Tue Sep 26 16:47:43 2017 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dwr98-0006YO-JJ for geh-help-gnu-emacs@m.gmane.org; Tue, 26 Sep 2017 16:47:38 +0200 Original-Received: from localhost ([::1]:47935 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwr9E-0004PE-CL for geh-help-gnu-emacs@m.gmane.org; Tue, 26 Sep 2017 10:47:44 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:41691) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwr8X-0004NY-W9 for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 10:47:03 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dwr8U-0002xj-SY for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 10:47:02 -0400 Original-Received: from forward103j.mail.yandex.net ([5.45.198.246]:60406) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dwr8U-0002wx-C0 for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 10:46:58 -0400 Original-Received: from mxback15j.mail.yandex.net (mxback15j.mail.yandex.net [IPv6:2a02:6b8:0:1619::91]) by forward103j.mail.yandex.net (Yandex) with ESMTP id 4063934C227C for ; Tue, 26 Sep 2017 17:46:56 +0300 (MSK) Original-Received: from smtp4j.mail.yandex.net (smtp4j.mail.yandex.net [2a02:6b8:0:1619::15:6]) by mxback15j.mail.yandex.net (nwsmtp/Yandex) with ESMTP id MaJvrPJYDc-kuRSRlFu; Tue, 26 Sep 2017 17:46:56 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506437216; bh=CbZYkLPLKCqAkkXPz4burk6d+qt9GIr3b4qmREoEhOg=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=Yt0JoLPvJg2mjwW8KeHDvf3R7z0EK/48xpOlsXlh2SKiFMSg/PQE3kUq2Je5AIfXo Ydsx/fWM716YxnnDQN/ul9Dlt1hwHRJv0D+a39Pihn5GSEAJrBorLhYSLHs+fxbXSt Uq3Yz/TfxpMSuKMnahWMzVHzPhjnECsE0/tL9Sgk= Original-Received: by smtp4j.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id CLFGHxgwGh-ksXu63JJ; Tue, 26 Sep 2017 17:46:54 +0300 (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (Client certificate not present) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506437215; bh=CbZYkLPLKCqAkkXPz4burk6d+qt9GIr3b4qmREoEhOg=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=XLmQG0chJ1yR8HdA/gSmcYBvjU9nZ12zjXfRd29z8ZfiluFNepXXJ/on49sAkfb0W 13SbCSRMAC0HwW0DPgeLl4w0UYAp1+HFCoH0rOQSh1meysHS8phOqAzq68tboUzFMM E6tAoePYj+YMGpnjExfB/M2Y2KOKBzhvPFC1XqOk= Authentication-Results: smtp4j.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <87mv5is54g.fsf@qcore> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 5.45.198.246 X-Content-Filtered-By: Mailman/MimeDel 2.1.21 X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.org gmane.emacs.help:114420 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --pJg5C8MwgLe4JX670oQnQgJ9r27UC3w2R From: =?UTF-8?Q?Mario_Castel=c3=a1n_Castro?= To: help-gnu-emacs@gnu.org Message-ID: <4d048ea0-5c54-f5ba-c903-78614480ac76@yandex.com> Subject: Re: CVE-2017-14482 - Red Hat Customer Portal References: <2e991bb7-c570-49ce-be94-3654945bb4b5@mousecar.com> <87d16jxjz6.fsf@eps142.cdf.udc.es> <861smzcgx3.fsf@zoho.com> <1b3bec6e-d4d5-37a7-ba54-49bd2d8281bd@yandex.com> <86k20qbcu9.fsf@zoho.com> <86o9q0a8zc.fsf@zoho.com> <87vak8rwcx.fsf@qcore> <87mv5is54g.fsf@qcore> In-Reply-To: <87mv5is54g.fsf@qcore> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 25/09/17 18:58, =C3=93scar Fuentes wrote: > Mario Castel=C3=A1n Castro writes: >> This depends on what exactly is meant by =E2=80=9Ccorrect=E2=80=9D. >=20 > "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 =E2=80=9Ccorrectness=E2=80=9D it is meant a formula in *formal l= ogic*, then yes, >> we can prove that the program behaves correctly. >=20 > Ever heard of a chap named Kurt G=C3=B6del? 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=C3=B6del, 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=C3=B6del-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 =C2=ACP 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 =E2=80=9Csure=E2=80=9D that a certain prop= osition P that is undecidable in (say) HOL is =E2=80=9Ctrue=E2=80=9D. What should you do= ? Since you are sure that P is =E2=80=9Ctrue=E2=80=9D, 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. > [=E2=80=A6] 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). > [=E2=80=A6] We must provide what is requested from us, in > terms of functionality, performance and cost [=E2=80=A6] 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 =E2=80=9CIntroduction to Mathematical Logic=E2=80=9D,= 6th edition (2015). --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --pJg5C8MwgLe4JX670oQnQgJ9r27UC3w2R Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWcpoWwAKCRC2380TuSZA 2YKiAQDnUstW6BJnzGrKM3jb76Il0/FnXqB3I0oRG+XWca2evwEAmoAwpwyCQVqx uWMTwfFtUmNoAGopDlnhN/xAOy9ETeE= =IHUL -----END PGP SIGNATURE----- --pJg5C8MwgLe4JX670oQnQgJ9r27UC3w2R--