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: Sun, 24 Sep 2017 08:38:59 -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> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="Cmjv7vu0vbxhjMK3W9Bll5QRouliDtaqv" X-Trace: blaine.gmane.org 1506260387 11150 195.159.176.226 (24 Sep 2017 13:39:47 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Sun, 24 Sep 2017 13:39: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 Sun Sep 24 15:39:42 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 1dw78F-0002T1-Kn for geh-help-gnu-emacs@m.gmane.org; Sun, 24 Sep 2017 15:39:39 +0200 Original-Received: from localhost ([::1]:38187 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dw78N-00037L-2m for geh-help-gnu-emacs@m.gmane.org; Sun, 24 Sep 2017 09:39:47 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:46615) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dw77r-000375-IJ for help-gnu-emacs@gnu.org; Sun, 24 Sep 2017 09:39:16 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dw77o-000396-Fv for help-gnu-emacs@gnu.org; Sun, 24 Sep 2017 09:39:15 -0400 Original-Received: from forward100o.mail.yandex.net ([37.140.190.180]:58917) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dw77n-00038S-Vh for help-gnu-emacs@gnu.org; Sun, 24 Sep 2017 09:39:12 -0400 Original-Received: from mxback7o.mail.yandex.net (mxback7o.mail.yandex.net [IPv6:2a02:6b8:0:1a2d::21]) by forward100o.mail.yandex.net (Yandex) with ESMTP id 69E762A2238E for ; Sun, 24 Sep 2017 16:39:09 +0300 (MSK) Original-Received: from smtp1p.mail.yandex.net (smtp1p.mail.yandex.net [2a02:6b8:0:1472:2741:0:8b6:6]) by mxback7o.mail.yandex.net (nwsmtp/Yandex) with ESMTP id fKLhqxlywI-d9DOI14o; Sun, 24 Sep 2017 16:39:09 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506260349; bh=egjba1Q4MeqXTS/2vFc1SCVihCZwmMIzsHm4Gl4wgh0=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=vrtQ5q8FTj2yvT8ng1/wZhr6rYl+f234MhEvRNhgiTK609OMB4pqYONKG0XUdtmvv TjIoRrrLK8Q4OGZS7TYxo4t1qOmYDGjZHwUpc/jD+srM4nVZROWoxADNNTQsGdvHEe hvxQky/ZNYRS87U5FaiGZK2xszYZ8PfYDq3i7tpQ= Original-Received: by smtp1p.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id FPPhb960Zl-d7bCtQwY; Sun, 24 Sep 2017 16:39:07 +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=1506260348; bh=egjba1Q4MeqXTS/2vFc1SCVihCZwmMIzsHm4Gl4wgh0=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=FL05oPqfbZF2qO5O/mJee1oQL+LsDfY5P8gQ8q4bvDRd3lp657Y1PpoQ32Ie1+OMc 9MCrDWOR+DAzDWP9lomQHwPuuR85BBhPF/iQpcUb15moHI80Y/0YBQsoSVpoR0Azse U6PhobUDSkB3nx8Q7pJoVCszV9lSBwF8Gh1Pm7Rc= Authentication-Results: smtp1p.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <86o9q0a8zc.fsf@zoho.com> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 37.140.190.180 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:114385 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --Cmjv7vu0vbxhjMK3W9Bll5QRouliDtaqv 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> In-Reply-To: <86o9q0a8zc.fsf@zoho.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 24/09/17 01:47, Emanuel Berg wrote: > A very, very small fraction of programmers will > ever care to (or indeed be able to) create > a model of the program just to verify the model > and then verify that the model is in agreement > with the program - this is just insane to ask > of anyone, and it isn't realistic one bit to > ever be a practical alternative. That is not how formal verification works in practice. Instead many (probably most) tools work by programming directly in the logic of the proof assistant and then extracting (without manual intervention) a program in a conventional programming language that has the same behavior as what was programmed in the logic. Contrary to what you assert, there are computer program well beyond trivial that have a specification and proof of correctness. I already mentioned the CakeML compiler . Other examples are the seL4 microkernel and the Compcert compiler. It is true that formal verification of a program requires several times the effort compared to writing a comparable non-verified program (but with many bugs). I argue that this effort is necessary, because it is the only way to write correct software. I think you will agree that although writing undocumented software is easier than writing well-documented software, writing documentation is part of software development and thus undocumented software must be considered incomplete. In the same way, I extend this to the claim that formal verification is part of software development and thus unverified software is incomplete. Although writing incomplete software is easier than writing complete software, the task should not be considered solved. It is like just building half of a bridge. Surely it is easier than building all of it; but it is not enough. > To a compiler - ? This can be done with simple > shell tools that perform basic computation! If by =E2=80=9Csimple shell tools that perform basic computation=E2=80=9D= you mean testing with random inputs, note that I already explained why this will be an awful testing method for a compiler. I will not repeat the explanation. --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --Cmjv7vu0vbxhjMK3W9Bll5QRouliDtaqv Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWce1eAAKCRC2380TuSZA 2ctQAQD14IQGZq6uFOS3h+79ROmvdDynVxA0uLU+4udMHMHhRwD8DrmYC6zoHy50 57gMeUjrsA/YM5jUiiSU+V1dZVskAz8= =FTbe -----END PGP SIGNATURE----- --Cmjv7vu0vbxhjMK3W9Bll5QRouliDtaqv--