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 20:43:39 -0500 Message-ID: <9146e66c-1055-0f61-f290-874e40377a76@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> <867ewnae8k.fsf@zoho.com> <86ing630vd.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="Fd30I6XlKVtaJdGT20ucNSQNL05NlEKwa" X-Trace: blaine.gmane.org 1506390275 5501 195.159.176.226 (26 Sep 2017 01:44:35 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 26 Sep 2017 01:44:35 +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 03:44:23 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 1dwev8-0000gG-Kf for geh-help-gnu-emacs@m.gmane.org; Tue, 26 Sep 2017 03:44:22 +0200 Original-Received: from localhost ([::1]:45154 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwevF-0006d2-Q2 for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 21:44:29 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:43028) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dweuo-0006ck-4m for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 21:44:03 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dweuk-0007xy-5l for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 21:44:02 -0400 Original-Received: from forward102j.mail.yandex.net ([5.45.198.243]:33290) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dweuj-0007x1-KR for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 21:43:58 -0400 Original-Received: from mxback1g.mail.yandex.net (mxback1g.mail.yandex.net [IPv6:2a02:6b8:0:1472:2741:0:8b7:162]) by forward102j.mail.yandex.net (Yandex) with ESMTP id 89F935602F0B for ; Tue, 26 Sep 2017 04:43:55 +0300 (MSK) Original-Received: from smtp3o.mail.yandex.net (smtp3o.mail.yandex.net [2a02:6b8:0:1a2d::27]) by mxback1g.mail.yandex.net (nwsmtp/Yandex) with ESMTP id Lybdly72KV-hnQ0jlqa; Tue, 26 Sep 2017 04:43:49 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506390229; bh=Oo2ilJNt0lXZjbMYdLGTAYcnJdCC1DfIaciNidtmKw0=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=Ifo1p5MVeFOWC/+3hnX8hZRMr0agz0WirbNKlcA3PIOg4M53YUW/gJfOpFlWquwCv svAGHxtqsFW2YYJx2pe0vcdH7VY1joYBlrKlLcdEdfEpf0IG17cswKeLaa/D3Wrlpl GDegUzXDnhVtWbvjOklaDy9UTjFR9Q7lecwhfoxU= Original-Received: by smtp3o.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id Xwxu35BWJL-hlLao2Gt; Tue, 26 Sep 2017 04:43:48 +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=1506390228; bh=Oo2ilJNt0lXZjbMYdLGTAYcnJdCC1DfIaciNidtmKw0=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=pTJRoRCU+awcAXFqEaEOQGCDoP7ZMLCu0cIZI2km54shuyfLWamwuXlaMek7ZYNQW Y8Ih94yvPQZxBZ8INb9VOdzBtGUWW8hLxmVCXqg6ra2ZbVL2ZNF3HVktfTyBERTY94 THZ7Ac28X84+Glgrh2LL3j0H5ztmIQaSbJG/aGko= Authentication-Results: smtp3o.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <86ing630vd.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.243 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:114403 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --Fd30I6XlKVtaJdGT20ucNSQNL05NlEKwa From: =?UTF-8?Q?Mario_Castel=c3=a1n_Castro?= To: help-gnu-emacs@gnu.org Message-ID: <9146e66c-1055-0f61-f290-874e40377a76@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> <867ewnae8k.fsf@zoho.com> <86ing630vd.fsf@zoho.com> In-Reply-To: <86ing630vd.fsf@zoho.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 25/09/17 16:49, Emanuel Berg wrote: > Mario Castel=C3=A1n Castro wrote: >=20 >> This is the prevalent attitude among >> programmers >=20 > Perhaps because it makes sense? It is known as > "conventional wisdom". >=20 >> we are showered by an endless stream of >> security patches and bug fixes. >=20 > Yes, and what is the problem with that? Obviously each such fix is evidence that a security vulnerability or another defect existed in the first place. A shower of fixes means that bugs are extremely prevalent in software. Otherwise it would have been impossible to sustain this tremendous bug discovery rate for years (check any web front end to the CVE database for details). Thus it is clear that the mainstream approach to writing software is failing to delivers reliable software. That is why we have the need for an alternative. Among all possible approaches, *only* formal testing has the possibility of virtually eliminating software defects. Note that errors in the model of the environment (as in the paper previously mentioned in this conversation) are not a *consequence* of formal verification. This is just a symptom, and moreover it is routine in non-formally verified software (i.e.: the developers make assumptions about the environment that will not always be met). For example, in Linux[1] they use the -fno-strict-pointer-aliasing compiler flag which is just a way to shove under the rug the problem of some incorrect assumptions they make about the semantics of C. This is an error of the implicit model of the environment. It is not stated in formal logic, but it is an error nonetheless. Formal verification provide a solution for this problem: If the low level software that makes up the environment for high level software has a formal specification, then the possibility of errors in the model of the environment can be eliminated by using the pre-existing formal model of the environment. [1] I mean Linux, the *kernel* used in GNU/Linux and other OS. --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --Fd30I6XlKVtaJdGT20ucNSQNL05NlEKwa Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWcmwywAKCRC2380TuSZA 2ZetAQCMCWfwe70Uynffy/Y0bqzLNlQuHFIR5w5NFclO2ebYrQD/fAllZrzrvlAI xMBQnmQYWlkkTaYQdF7aFQdtsFT3AXs= =hfUc -----END PGP SIGNATURE----- --Fd30I6XlKVtaJdGT20ucNSQNL05NlEKwa--