From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: =?utf-8?Q?=C3=93scar_Fuentes?= Newsgroups: gmane.emacs.help Subject: Re: CVE-2017-14482 - Red Hat Customer Portal Date: Tue, 26 Sep 2017 01:58:07 +0200 Message-ID: <87mv5is54g.fsf@qcore> 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> 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 1506383942 17134 195.159.176.226 (25 Sep 2017 23:59:02 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Mon, 25 Sep 2017 23:59:02 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.0.50 (gnu/linux) 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 01:58:57 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 1dwdH5-0003fg-1f for geh-help-gnu-emacs@m.gmane.org; Tue, 26 Sep 2017 01:58:55 +0200 Original-Received: from localhost ([::1]:44855 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwdH6-0007IX-Cr for geh-help-gnu-emacs@m.gmane.org; Mon, 25 Sep 2017 19:58:56 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:52979) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dwdGb-0007H1-Ij for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 19:58:26 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dwdGX-0008KH-6Z for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 19:58:25 -0400 Original-Received: from [195.159.176.226] (port=37068 helo=blaine.gmane.org) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dwdGW-0008K1-Vd for help-gnu-emacs@gnu.org; Mon, 25 Sep 2017 19:58:21 -0400 Original-Received: from list by blaine.gmane.org with local (Exim 4.84_2) (envelope-from ) id 1dwdGM-0001M4-Vh for help-gnu-emacs@gnu.org; Tue, 26 Sep 2017 01:58:10 +0200 X-Injected-Via-Gmane: http://gmane.org/ Original-Lines: 91 Original-X-Complaints-To: usenet@blaine.gmane.org Cancel-Lock: sha1:6AFg/h4smkE29Ypf11ENxWzcNjc= 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:114402 Archived-At: Mario Castelán Castro writes: > On 24/09/17 09:42, Óscar Fuentes wrote: >> It seems that you think that formal verification says that the software >> is correct. That's in theory. Practice is different, as usual. > > This depends on what exactly is meant by “correct”. "correct" means that the client (the people who required the software) says that the program fulfills his requirements. Sometimes you need to wait an infinite amount of time for obtaining client's approbation :-) > If by “correctness” it is meant a formula in *formal logic*, then yes, > we can prove that the program behaves correctly. Ever heard of a chap named Kurt Gödel? Or his cousin Alan Turing? :-) > If by “correct” it is meant an informal concept, then proving > correctness is in general not possible because a specification in formal > logic is required to prove anything. One may believe that one has > formalized correct behavior but later one finds that the formalization > does not accurately capture the informal concept. Yes. But we have to deal with informal specifications. Furthermore, it is almost certain that there are "correct" informal specifications that do not admit a verifiable formal specification. > The cases of the “bugs” mentioned in the paper you referenced are error > in formalizing “correct behavior”. That this is possible is not breaking > news, as you seem to think. This is a caveat well known to anybody > involved in formal verification. Yet you seem to give it little importance. Once we assume that a verifiable specification might be incorrect in the sense you mention, we must acknowledge that the verification itself does not say that the program is correct (wrt the "informal yet correct" specification). That is, the formal approach might help to improve software quality, but it is no guarantee of bug-free software. Why I said "might" above? I postulate that there will be cases where experts will consider more trustworthy a program written on a traditional but convenient language than other which passed verification. This is because some formal specifications will look more suspicious than a program that implements the informal specification, because of the constraints imposed by the formalization process. > Specifically, several of those “bugs” are errors in describing the > behavior of the environment in which the program is assumed to run. One > possible view in this circumstance is that the program *is* correct, but > it was run in an environment where the formal guarantees does not apply. > This is similar as how one can prove the implication that *if* ‘X’ is a > real number *then* ‘X^2≥0’. Suppose somebody applies the conclusion > where the antecedent fails; for example, in the complex numbers, then > the conclusion is false, but so is the antecedent, so there is no > contradiction here. > > There is also the issue of having a fundamentally unsound logic. We can > reason about this risk as follows: The underlying logic of many proof > assistants is, or can, be proved sound (note that soundness implies > consistency) assuming that ZFC is consistent. In turn we have reasons to > believe that ZFC is consistent (I will not elaborate on that because it > deviates too much from the original topic of this conversation). Oh! the consistence of ZFC! now we are on pure mathematical land! :-) Software is an industry. We must provide what is requested from us, in terms of functionality, performance and cost (both in time and money). Formal methods are being proposed as (yet another) silver bullet, which, as every other silver bullet we were sold on the past, will fail to deliver its grandiose promise. An improvement? absolutely. For some types of software formal verification is a huge advance. But for other classes of software (see it? types/classes :-) its impact will not go further than the indirect improvement gained from building upon solid implementations of algorithms, at least on the cases where the price to pay on performance is not too much. >> Instead of writing a lengthy explanation about why formal verification >> can't be a guarantee about the correctness of a piece of sotware, I'll >> simply reference a study about failures on verified systems: >> >> https://blog.acolyer.org/2017/05/29/an-empirical-study-on-the-correctness-of-formally-verified-distributed-systems/ > > The paper is of interest to me. Thanks for bringing it into my > attention. I only took a glance but maybe I will eventually read it with > detail. The blog post is just padding; you should have linked the paper > directly. You are welcomed. The blog post is a good comment on the paper that exposes the gist of it and might be of interest to non-experts or people who is too busy.