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: Mon, 25 Sep 2017 16:11:04 -0500 Message-ID: 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> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="4Ul3nE5CbQotcHwoOsAd7Xl66u2rNs31a" X-Trace: blaine.gmane.org 1506373908 2065 195.159.176.226 (25 Sep 2017 21:11:48 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Mon, 25 Sep 2017 21:11:48 +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 Mon Sep 25 23:11:44 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 1dwafH-0000Fc-H1 for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 23:11:43 +0200 Original-Received: from localhost ([::1]:44310 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwafO-0001pl-Pw for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 17:11:50 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:39189) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwaer-0001pa-Dn for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 17:11:18 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dwaeo-0002sD-7S for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 17:11:17 -0400 Original-Received: from forward106o.mail.yandex.net ([37.140.190.187]:44885) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dwaen-0002r7-MB for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 17:11:14 -0400 Original-Received: from mxback3o.mail.yandex.net (mxback3o.mail.yandex.net [IPv6:2a02:6b8:0:1a2d::1d]) by forward106o.mail.yandex.net (Yandex) with ESMTP id CFFBA783586 for ; Tue, 26 Sep 2017 00:11:09 +0300 (MSK) Original-Received: from smtp3o.mail.yandex.net (smtp3o.mail.yandex.net [2a02:6b8:0:1a2d::27]) by mxback3o.mail.yandex.net (nwsmtp/Yandex) with ESMTP id CnFnUU93aT-B9dSY8aT; Tue, 26 Sep 2017 00:11:09 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506373869; bh=tDmBUN7+GzSCzQlCUbtDDlUUtFkYP8oCXjfofBNAtlk=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=qGDmsoaZe6iSgJIliK+eTvnpcjunbVFiVvvyWOOE+MGGYq1klItp0FY9LwLgmBvxM EifgamXSfX58C3V0ksrjenHWoGiRFusQE0MvH68TtzfzqZTzatGlTfA28V9U8HRgxu X276SklzT9KYYS+4Pw+l+rCasK7qPpU8bhH/q3D0= Original-Received: by smtp3o.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id q7uBOl51Iu-B7iOOS6L; Tue, 26 Sep 2017 00:11:08 +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=1506373868; bh=tDmBUN7+GzSCzQlCUbtDDlUUtFkYP8oCXjfofBNAtlk=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=rFofSSYLjPNPWnxyKssIzb3Irhp1KIyj79BMH6woSeAONjxepKqhZPCSbO3kAkPPd xEhWI68mD9LlejRseafIEuAADqionq1oO014bZCYAv6y/NbgjXDzU4/IH0e+0ALHVZ Lvwu4WkPWagP7apD45ELYpudkpg9g9zRkQlnxfVY= Authentication-Results: smtp3o.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <87vak8rwcx.fsf@qcore> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 37.140.190.187 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:114397 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --4Ul3nE5CbQotcHwoOsAd7Xl66u2rNs31a From: =?UTF-8?Q?Mario_Castel=c3=a1n_Castro?= To: help-gnu-emacs@gnu.org Message-ID: 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> In-Reply-To: <87vak8rwcx.fsf@qcore> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 24/09/17 09:42, =C3=93scar Fuentes wrote: > It seems that you think that formal verification says that the software= > is correct. That's in theory. Practice is different, as usual. This depends on what exactly is meant by =E2=80=9Ccorrect=E2=80=9D. If by =E2=80=9Ccorrectness=E2=80=9D it is meant a formula in *formal logi= c*, then yes, we can prove that the program behaves correctly. If by =E2=80=9Ccorrect=E2=80=9D it is meant an informal concept, then pro= ving correctness is in general not possible because a specification in formal logic is required to prove anything. One may believe that one has formalized correct behavior but later one finds that the formalization does not accurately capture the informal concept. The cases of the =E2=80=9Cbugs=E2=80=9D mentioned in the paper you refere= nced are error in formalizing =E2=80=9Ccorrect behavior=E2=80=9D. That this is possible = is not breaking news, as you seem to think. This is a caveat well known to anybody involved in formal verification. Specifically, several of those =E2=80=9Cbugs=E2=80=9D are errors in descr= ibing the behavior of the environment in which the program is assumed to run. One possible view in this circumstance is that the program *is* correct, but it was run in an environment where the formal guarantees does not apply. This is similar as how one can prove the implication that *if* =E2=80=98X= =E2=80=99 is a real number *then* =E2=80=98X^2=E2=89=A50=E2=80=99. Suppose somebody appl= ies the conclusion where the antecedent fails; for example, in the complex numbers, then the conclusion is false, but so is the antecedent, so there is no contradiction here. There is also the issue of having a fundamentally unsound logic. We can reason about this risk as follows: The underlying logic of many proof assistants is, or can, be proved sound (note that soundness implies consistency) assuming that ZFC is consistent. In turn we have reasons to believe that ZFC is consistent (I will not elaborate on that because it deviates too much from the original topic of this conversation). > Instead of writing a lengthy explanation about why formal verification > can't be a guarantee about the correctness of a piece of sotware, I'll > simply reference a study about failures on verified systems: >=20 > https://blog.acolyer.org/2017/05/29/an-empirical-study-on-the-correctne= ss-of-formally-verified-distributed-systems/ The paper is of interest to me. Thanks for bringing it into my attention. I only took a glance but maybe I will eventually read it with detail. The blog post is just padding; you should have linked the paper directly. --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --4Ul3nE5CbQotcHwoOsAd7Xl66u2rNs31a Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWclw6AAKCRC2380TuSZA 2U53AP9ZoaWs9YueoGObcLmTNeLf8UZTwmZhBSydy/741sC1ZgEAuPnAFworx2DC JLNq+KH2VoWHFuYy98xJhqDrSFNRgd8= =kBNZ -----END PGP SIGNATURE----- --4Ul3nE5CbQotcHwoOsAd7Xl66u2rNs31a--