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:23:49 -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> <867ewnae8k.fsf@zoho.com> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="xehOlkfwEtn98t7PkRnfX1RckWCaXn36I" X-Trace: blaine.gmane.org 1506374687 21538 195.159.176.226 (25 Sep 2017 21:24:47 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Mon, 25 Sep 2017 21:24:47 +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:24: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 1dwarq-0005D8-Rd for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 23:24:43 +0200 Original-Received: from localhost ([::1]:44355 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwarx-0007yV-Vd for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 17:24:50 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:41707) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwarE-0007we-L9 for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 17:24:06 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dwarA-0007pj-6n for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 17:24:04 -0400 Original-Received: from forward104p.mail.yandex.net ([77.88.28.107]:49645) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dwar9-0007oC-NI for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 17:24:00 -0400 Original-Received: from mxback15j.mail.yandex.net (mxback15j.mail.yandex.net [IPv6:2a02:6b8:0:1619::91]) by forward104p.mail.yandex.net (Yandex) with ESMTP id 335AB182545 for ; Tue, 26 Sep 2017 00:23:55 +0300 (MSK) Original-Received: from smtp4o.mail.yandex.net (smtp4o.mail.yandex.net [2a02:6b8:0:1a2d::28]) by mxback15j.mail.yandex.net (nwsmtp/Yandex) with ESMTP id TVIYr4xL3Z-NtJ88LhT; Tue, 26 Sep 2017 00:23:55 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506374635; bh=6I6YPfqNrDRpiLc8XcDC3lj+JClWjBOMaB7tXXxTZ6g=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=NPd9IPwUZvG6t+boYIpG30Owk+ekslaY5WXEdvWuGW5OjLQhu0i/yCTL6wGjPjOGJ 9Bs7srXYScnqMpY+sLQxV+/fTtntl3+r27Qg9J4R7028dvjrjjxqpmxNPdRXPG/XeD FEH19Qb9mItlvvELCtabxa4neqIYq9mqhK7tCLl0= Original-Received: by smtp4o.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id 6XKfXdRUe1-NqFmrk15; Tue, 26 Sep 2017 00:23:53 +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=1506374633; bh=6I6YPfqNrDRpiLc8XcDC3lj+JClWjBOMaB7tXXxTZ6g=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=aT4cHUaSRw+UhkNjeuVwUYRYt56CDk23ayvfRUXrWG5bgShwYD6WyatVvc9ilBYpV voFZUNvEz1ooxCeFJatMCi5Hj/U0OPW+ToNuadqliCpHUc5lCQ5m8qbP07+FMN+Yej u9lXMiT4XSYAg0c96v2GplKagYTiuV3AKOQDoes8= Authentication-Results: smtp4o.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <867ewnae8k.fsf@zoho.com> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 77.88.28.107 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:114398 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --xehOlkfwEtn98t7PkRnfX1RckWCaXn36I 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> <867ewnae8k.fsf@zoho.com> In-Reply-To: <867ewnae8k.fsf@zoho.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 24/09/17 18:06, Emanuel Berg wrote: > Hold - perhaps the verification has to be > verified as well? What any proof of correctness proves is an implication saying roughly: =E2=80=9CIF the environment meets these requisites THEN the program does = [=E2=80=A6]=E2=80=9D. The =E2=80=9Cbugs=E2=80=9D described in the aforementioned paper are not = a flaw in the proof. The source of the problem is that EITHER the programs under test were being used in an environment does not meet the requisites (i.e.: =E2=80=9CIF the environment meets=E2=80=9D) OR the user was expecting the= program to do something different than what is guaranteed by the conclusion =E2=80=9Cth= e program does [=E2=80=A6]=E2=80=9D. > C'mon now, this is just another > Computer Science hangup. Just like > functional programming, or testing for that > matter - which also is an academic pursuit, by > the way! [1] - but as always, there is no > silver bullet solution. This is the prevalent attitude among programmers, and this is the reason that we are showered by an endless stream of security patches and bug fix= es. > If I'd send the space fleet to the oldest > galaxies of the universe, I'd like all methods > anyone could think of to make as sure as > possible the software is correct. >=20 > I'd start with very skilled and motivated > programmers, proceed with sound programming > practices, then code review, and then > excessive testing. >=20 > I suppose formal verification would be > a distant fourth. Well, then it is a very good thing that you are NOT in charge of designing that piece of software. --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --xehOlkfwEtn98t7PkRnfX1RckWCaXn36I Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWclz5QAKCRC2380TuSZA 2RLyAQC/FB8SCq0QCv2/JVBYmLv8Ngm+oen0rf/gaTpmKlgjPgEAt0uylYu2bMJq cMhdAQafWFFXqs+j41ctWPJCsGHZlO4= =cmDe -----END PGP SIGNATURE----- --xehOlkfwEtn98t7PkRnfX1RckWCaXn36I--