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: Sat, 23 Sep 2017 21:08:42 -0500 Message-ID: <6b274745-f1bb-9ef0-e3a2-7e3c1fc7665a@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> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="AhWijBcAN9uNxDCrWrOK5j22SIeh1MHnm" X-Trace: blaine.gmane.org 1506218976 18367 195.159.176.226 (24 Sep 2017 02:09:36 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Sun, 24 Sep 2017 02:09:36 +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 04:09:29 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 1dvwML-0004He-0J for geh-help-gnu-emacs@m.gmane.org; Sun, 24 Sep 2017 04:09:29 +0200 Original-Received: from localhost ([::1]:36606 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dvwMS-0005ys-FS for geh-help-gnu-emacs@m.gmane.org; Sat, 23 Sep 2017 22:09:36 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:59460) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dvwLq-0005yn-KS for help-gnu-emacs@gnu.org; Sat, 23 Sep 2017 22:08:59 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dvwLn-0007Mt-DX for help-gnu-emacs@gnu.org; Sat, 23 Sep 2017 22:08:58 -0400 Original-Received: from forward101o.mail.yandex.net ([37.140.190.181]:58715) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dvwLm-0007KJ-S4 for help-gnu-emacs@gnu.org; Sat, 23 Sep 2017 22:08:55 -0400 Original-Received: from mxback20j.mail.yandex.net (mxback20j.mail.yandex.net [IPv6:2a02:6b8:0:1619::114]) by forward101o.mail.yandex.net (Yandex) with ESMTP id 83E8F1343EC4 for ; Sun, 24 Sep 2017 05:08:49 +0300 (MSK) Original-Received: from smtp1o.mail.yandex.net (smtp1o.mail.yandex.net [2a02:6b8:0:1a2d::25]) by mxback20j.mail.yandex.net (nwsmtp/Yandex) with ESMTP id AEd1biL0us-8no4Wf3a; Sun, 24 Sep 2017 05:08:49 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506218929; bh=e1tf+UTmJpZG09clV16GT8FErrMCK475TwR64MVtRLw=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=lajDDudin3Un7+yGcS54bh4JIZIPf5VsUGKoYAYeC5NNpN2qKeCpVF9CTvmmarTG+ mfGVQPaDyKNUlT3ggn1tprKiL6/YQvzrx/loUTElNoUHmINaTGSlsf682/XXJJXBvq FFc/NPN8aM7bY7xntP1CLEplYcdn0SIgGZrHVNDM= Original-Received: by smtp1o.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id MaDUeRKNvY-8jSmbfDv; Sun, 24 Sep 2017 05:08:45 +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=1506218926; bh=e1tf+UTmJpZG09clV16GT8FErrMCK475TwR64MVtRLw=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=xpZsYJgNThwAM+FrvjzHis/ylAZOOD72armsoCJSRAXRPpIfMbIP57iKSn1Qtytnd 9RPwjZIcxhzEXSypjTTEaX4WaBiem7XDmIW1ZoPl/IRfBl9Z8dcW2SwbSEkklH4I34 3Whj8Go4W2dQZYQTH7nRfz4avbA5ZaQ59lMKcu/I= Authentication-Results: smtp1o.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <86k20qbcu9.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.181 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:114371 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --AhWijBcAN9uNxDCrWrOK5j22SIeh1MHnm From: =?UTF-8?Q?Mario_Castel=c3=a1n_Castro?= To: help-gnu-emacs@gnu.org Message-ID: <6b274745-f1bb-9ef0-e3a2-7e3c1fc7665a@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> In-Reply-To: <86k20qbcu9.fsf@zoho.com> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 22/09/17 17:14, Emanuel Berg wrote: > Also, formal verification that is applied on > a model will only prove that *the model* is > correct, not the real thing. You seem to be confused, verifying that a program is correct *requires* a model. Verifying the model is a different and separate task. > [=E2=80=A6] Then it is trivial to setup a test > program that will just invoke repeatedly with > randomized integers and strings. [=E2=80=A6] Random testing is very inefficient because most inputs are garbage and are treated uniformly by the program under test. For example, feeding random input to a compiler will result almost surely in only ill-formed programs and thus will not exercise anything but the parser. Good testing must exercise code paths that only run in rare corner cases and the probability that random testing achieves this is very small. But like I said, testing is fundamentally flawed. Testing can tell you that a program is defective, but not that a program is free from defects!= > There are also languages like Dafny where you > can state formally what a function should do, > and the verification tool will match that to > your code. [=E2=80=A6] Taking a glance at Danfy, it seems like it trusts the answers of a SMT solver (Microsoft's Z3) and does not generate proofs of correctness (but I can easily be wrong; I did not check in deep because I dislike .NET). This is not what I am referring about when I say =E2=80=9Cproving program= s correct=E2=80=9D. I mean software like CakeML . It i= s linked to a proof assistant (HOL4). You can develop there the specification of the program and prove it correct according to the specification. There is still much work to be done to make formal verification tools like this more usable, but it must be noted that in the case of CakeML it *already* works. CakeML is itself formally verified using HOL4. Unfortunately there is little documentation material to learn to use CakeML. Using HOL4 or other proof assistant requires at least a solid intuition for formal logic and some knowledge in mathematics. Anybody wanting to call himself a programmer must become comfortable with using a proof assistant because this is a prerequisite to writing correct software. *ANY* other approach leads to defective software, *especially* ordinary testing[1]. Notes: [1]: There is also software that is not itself proved correct, but generates a solution for a problem along with a proof that the solution is correct. For example, many SAT solvers meet this description. Provided one can verify the proof, one can the ascertain that the solution is correct, but the program may still generate incorrect =E2=80=9Csolutions=E2=80=9D in other cases. --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --AhWijBcAN9uNxDCrWrOK5j22SIeh1MHnm Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWccTqgAKCRC2380TuSZA 2XTpAP475bg3JgpSOkIBHlYUj5OFaezhA8vDhSbxH5LIEZwLGwEAomi8YVkVCBMu yEE3yVt0Yp6A49oJicLJ2YPD2oa+YWw= =WWOg -----END PGP SIGNATURE----- --AhWijBcAN9uNxDCrWrOK5j22SIeh1MHnm--