From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Emanuel Berg Newsgroups: gmane.emacs.help Subject: Re: CVE-2017-14482 - Red Hat Customer Portal Date: Sat, 23 Sep 2017 00:14:22 +0200 Message-ID: <86k20qbcu9.fsf@zoho.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> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Trace: blaine.gmane.org 1506118519 4944 195.159.176.226 (22 Sep 2017 22:15:19 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 22 Sep 2017 22:15:19 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.4 (gnu/linux) To: help-gnu-emacs@gnu.org Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane.org@gnu.org Sat Sep 23 00:15:15 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 1dvWE7-00010N-7g for geh-help-gnu-emacs@m.gmane.org; Sat, 23 Sep 2017 00:15:15 +0200 Original-Received: from localhost ([::1]:32970 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dvWEE-0004bD-JV for geh-help-gnu-emacs@m.gmane.org; Fri, 22 Sep 2017 18:15:22 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33038) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dvWDV-0004ZV-RX for help-gnu-emacs@gnu.org; Fri, 22 Sep 2017 18:14:38 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dvWDS-0005yq-IU for help-gnu-emacs@gnu.org; Fri, 22 Sep 2017 18:14:37 -0400 Original-Received: from [195.159.176.226] (port=37859 helo=blaine.gmane.org) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dvWDS-0005yM-BB for help-gnu-emacs@gnu.org; Fri, 22 Sep 2017 18:14:34 -0400 Original-Received: from list by blaine.gmane.org with local (Exim 4.84_2) (envelope-from ) id 1dvWDI-0006pc-CM for help-gnu-emacs@gnu.org; Sat, 23 Sep 2017 00:14:24 +0200 X-Injected-Via-Gmane: http://gmane.org/ Mail-Followup-To: help-gnu-emacs@gnu.org Original-Lines: 97 Original-X-Complaints-To: usenet@blaine.gmane.org Mail-Copies-To: never Cancel-Lock: sha1:ZXbPOI0IBYu/KvTNOz5Duli9DoI= X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 195.159.176.226 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:114352 Archived-At: Mario Castelán Castro wrote: > 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. [...] Also, formal verification that is applied on a model will only prove that *the model* is correct, not the real thing. There is one automated way of testing that I know of that actually works, and that is for shell tools that have the super-simple text interface where the tool accepts a limited set of arguments. Say that it accepts one integer as the first argument and then one string as its second. Then it is trivial to setup a test program that will just invoke repeatedly with randomized integers and strings. Because its random, it might find borderline cases which makes absolutely no sense (but still shouldn't break the program), but which supposedly rational human beings would never think of to input, and thus without the test program, would never get tested. But for a huge software system like Emacs, formal verification being obviously out of the question, even simple-minded brute-force testing is difficult to set up, at least for anything bigger than the smallest module.el. So the byte-compiler and style checks (`checkdoc-current-buffer') is what you got. Instead, I think the best way to test is just to have lots of people using it. At least major flaws will surface really soon this way. 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. Problem is, it isn't refined to any degree where it actually will matter for every-day programming. Often, the code will be correct, and the formal description is correct as well, only the verifier will still say it doesn't compute. And programming should obviously not be about tinkering with code and expressions that already makes sense, just so that the computer will agree it does. So straight down the line, this will amount to toy/demo programs as well. Here is an example: method Main () { var n := f(4, 5); print "The result is "; print n; } method f(a:int, b:int) returns (r:int) requires a >= 0; requires b >= 0; ensures r == 4*a + b; { r := 0; var i := 0; var j := 0; while (i < a || j < b) decreases a + b - (i + j); invariant 0 <= i <= a; invariant 0 <= j <= b; invariant r == 4*i + j; { if (j < b) { r := r + 1; j := j + 1; } else { r := r + 4; i := i + 1; } } } There is a Dafny mode for Emacs, and with Mono (because it is an .NET thing to begin with), perhaps one could hook that up into a neat IDE. Still, it will only amount to poor Dafny. -- underground experts united http://user.it.uu.se/~embe8573