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: Fri, 22 Sep 2017 15:12:01 -0500 Message-ID: <1b3bec6e-d4d5-37a7-ba54-49bd2d8281bd@yandex.com> References: <2e991bb7-c570-49ce-be94-3654945bb4b5@mousecar.com> <87d16jxjz6.fsf@eps142.cdf.udc.es> <861smzcgx3.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="uTmXwAoWw6I2UCKGKxPpugr6GrLLnJ5o6" X-Trace: blaine.gmane.org 1506111368 9442 195.159.176.226 (22 Sep 2017 20:16:08 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 22 Sep 2017 20:16:08 +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 Fri Sep 22 22:16:03 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 1dvUMk-00025O-MJ for geh-help-gnu-emacs@m.gmane.org; Fri, 22 Sep 2017 22:16:02 +0200 Original-Received: from localhost ([::1]:60870 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dvUMr-0007Zj-S9 for geh-help-gnu-emacs@m.gmane.org; Fri, 22 Sep 2017 16:16:09 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33337) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dvUJT-0005TF-6r for help-gnu-emacs@gnu.org; Fri, 22 Sep 2017 16:12:40 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dvUJP-0005Ue-6T for help-gnu-emacs@gnu.org; Fri, 22 Sep 2017 16:12:39 -0400 Original-Received: from forward106j.mail.yandex.net ([5.45.198.249]:51683) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dvUJO-0005R7-Lg for help-gnu-emacs@gnu.org; Fri, 22 Sep 2017 16:12:35 -0400 Original-Received: from mxback9g.mail.yandex.net (mxback9g.mail.yandex.net [IPv6:2a02:6b8:0:1472:2741:0:8b7:170]) by forward106j.mail.yandex.net (Yandex) with ESMTP id BAB661802E5F for ; Fri, 22 Sep 2017 23:12:31 +0300 (MSK) Original-Received: from smtp2j.mail.yandex.net (smtp2j.mail.yandex.net [2a02:6b8:0:801::ac]) by mxback9g.mail.yandex.net (nwsmtp/Yandex) with ESMTP id YFYxTBTVPz-CVceU1CR; Fri, 22 Sep 2017 23:12:31 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506111151; bh=S6pMgOlBka9ZceTtA5Cy50Y0yZZajKdpCyFMKawNgB4=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=Dr7tvt1wQLwMth5XrUB1AsiXmBJdci1IwXlvLV1hiTJiEUYOvPi3fLrv/dWqhH82n TqenzqW+myvEcoI47rbi9NCdkBRX6Z9NpVHJnQ/Nkd2mSjCd5lQQcvOuKSKpfoee1K +5LFXk6voGTV7q8V+IN4gT+CPcJtEKzpKmAOVzxc= Original-Received: by smtp2j.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id ibvdnRVm1M-CTfmxmT1; Fri, 22 Sep 2017 23:12:30 +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=1506111150; bh=S6pMgOlBka9ZceTtA5Cy50Y0yZZajKdpCyFMKawNgB4=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=eBmkLinAwNH0XJ7PQh8EYJdPmCn/mHvwSvKAADYWhy8zQYBHwDwq29tN+7W5ZnGVg wzuUNGrelF1wOFRrMjAl3Q6Ne6uO7bVzxJEtqM1XipXYzLrM1rXIVqmNk/3Umc6yp1 MaIlybTPdUgVTfPfwt0Rnq4wcDWa+ZmTq2fk2rGY= Authentication-Results: smtp2j.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <861smzcgx3.fsf@zoho.com> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 5.45.198.249 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:114350 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --uTmXwAoWw6I2UCKGKxPpugr6GrLLnJ5o6 From: =?UTF-8?Q?Mario_Castel=c3=a1n_Castro?= To: help-gnu-emacs@gnu.org Message-ID: <1b3bec6e-d4d5-37a7-ba54-49bd2d8281bd@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> In-Reply-To: <861smzcgx3.fsf@zoho.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 22/09/17 02:48, Emanuel Berg wrote: > It would be interesting to see the original > code that created this vulnerability. I mean, > so you know what *not* to write... ehem. That is the problem with nearly all contemporary programs: Instead of verifying that they are correct; it is verified that they are not incorrect according to a small set of ways in which a program may be incorrect. This idea doomed to fail is the foundation of conventional testing, SMT testing (as in Klee), lint-like tools and manual source code auditing. Paraphrasing Dijkstra, all these methods can prove that a program is incorrect, but almost never (only trivial toy programs) can prove that it is correct. Only verifying that programs are correct using formal logic and an appropriate specification can eliminate software bugs (hardware can always malfunction, because of ionizing radiation, =E2=80=9Cmetastability= =E2=80=9D of flip-flops, because somebody disconnects the power cord, and many other things). At present there is limited infrastructure for verified programming, but it can be done. See e.g.: https://cakeml.org/. --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --uTmXwAoWw6I2UCKGKxPpugr6GrLLnJ5o6 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWcVuqwAKCRC2380TuSZA 2dnkAQDhhZEN9KS5gWs7epAxgiqoisCiXay4ddcPkQKEcBxRHAD+Is2y61M3qyFa 15igABL5qAXE2weJIzyyrIKwWqczOkc= =5zPY -----END PGP SIGNATURE----- --uTmXwAoWw6I2UCKGKxPpugr6GrLLnJ5o6--