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: Fri, 29 Sep 2017 15:21: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> <87vak8rwcx.fsf@qcore> <87mv5is54g.fsf@qcore> <4d048ea0-5c54-f5ba-c903-78614480ac76@yandex.com> <87d16drq8i.fsf@qcore> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="4Jxqs9egGX6k66nM1NDsClKOUo63NxpOE" X-Trace: blaine.gmane.org 1506716598 3215 195.159.176.226 (29 Sep 2017 20:23:18 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 29 Sep 2017 20:23:18 +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 Fri Sep 29 22:23:12 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 1dy1oW-0000HY-5E for geh-help-gnu-emacs@m.gmane.org; Fri, 29 Sep 2017 22:23:12 +0200 Original-Received: from localhost ([::1]:36964 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dy1od-0006N2-I8 for geh-help-gnu-emacs@m.gmane.org; Fri, 29 Sep 2017 16:23:19 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:45361) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dy1ne-0006KU-MN for help-gnu-emacs@gnu.org; Fri, 29 Sep 2017 16:22:20 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dy1na-0000HZ-Tu for help-gnu-emacs@gnu.org; Fri, 29 Sep 2017 16:22:18 -0400 Original-Received: from forward106p.mail.yandex.net ([77.88.28.109]:47266) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dy1na-0000GY-B9 for help-gnu-emacs@gnu.org; Fri, 29 Sep 2017 16:22:14 -0400 Original-Received: from mxback10g.mail.yandex.net (mxback10g.mail.yandex.net [IPv6:2a02:6b8:0:1472:2741:0:8b7:171]) by forward106p.mail.yandex.net (Yandex) with ESMTP id 6DA0A2D83475 for ; Fri, 29 Sep 2017 23:22:09 +0300 (MSK) Original-Received: from smtp3p.mail.yandex.net (smtp3p.mail.yandex.net [2a02:6b8:0:1472:2741:0:8b6:8]) by mxback10g.mail.yandex.net (nwsmtp/Yandex) with ESMTP id J92s0wjv0v-M96KLJGI; Fri, 29 Sep 2017 23:22:09 +0300 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yandex.com; s=mail; t=1506716529; bh=3EBYpQDHGhb4cG9SViFXY2exzbxN0IP1PK3Ccr6xiwI=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=v43zMFe6q9GxrSFrOa0kzSxTWa69kbC5Ipk24Z+KzZSmgiTIK5MkIsXR9EdgLJN+1 oCI+DWmAvvQB2uoP/3TDKr0TEa4Ezm+D5VP69T5PPwYPIZPplvNmyusazR7VAMD2Tm Z84j2XWSAk7BV+WywB2lREx5Wv0XMpzbCymix7FQ= Original-Received: by smtp3p.mail.yandex.net (nwsmtp/Yandex) with ESMTPSA id sfhm0LrZTH-M7mS0v2F; Fri, 29 Sep 2017 23:22: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=1506716528; bh=3EBYpQDHGhb4cG9SViFXY2exzbxN0IP1PK3Ccr6xiwI=; h=Subject:To:References:From:Message-ID:Date:In-Reply-To; b=YR2UQ9TEJRccZNT/JAsbgVwW0QE3XHDQ9mkdPbvIgN9Io8g29KO8xX675L7fCoAvS GvJxrK5GHHhUq4MGDvj8N/IspH9CYng0FXC4CBi8qQf38JeyzVEHk49gRyl45bL9gX 4gD8HWrj9L/jKCmTT6wE8HfW+jK14wvAASrh5sy4= Authentication-Results: smtp3p.mail.yandex.net; dkim=pass header.i=@yandex.com In-Reply-To: <87d16drq8i.fsf@qcore> X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 77.88.28.109 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:114481 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --4Jxqs9egGX6k66nM1NDsClKOUo63NxpOE 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> <87vak8rwcx.fsf@qcore> <87mv5is54g.fsf@qcore> <4d048ea0-5c54-f5ba-c903-78614480ac76@yandex.com> <87d16drq8i.fsf@qcore> In-Reply-To: <87d16drq8i.fsf@qcore> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable I am sorry for the delayed reply. I (incorrectly) assumed that nobody would still be interested in this conversation and thus I did not check this thread until today. On 26/09/17 18:31, =C3=93scar Fuentes wrote: > Well, as a humble software developer who is happy whenever I get things= > done "well enough", let me ask a few simple questions. You can simply > respond with "yes" or "no", if you wish: >=20 > * Is there a proof that demonstrates that every program admits a > verifiable formal specification, or a method for knowing in advance > which programs admit such specification? If interpreted literally, the answer is trivial: Yes, for any program you can formulate formal specifications. For example, the specification that the program always terminates is meaningful for any program. It seems that what you really mean is =E2=80=9Ccan *any* informal specifi= cation be converted into a formal specification?=E2=80=9D. In short: No, because it may be too vague but IF you can unambiguously describe the allowed behaviors of a program, THEN you can formalize it. To be a bit more specific: IF you can write an =E2=80=9Cevaluator program= =E2=80=9D that takes an execution trace (a description of how the program that is supposed to meet the informal specification behaved in a concrete run) and says either "good" or "bad" depending on whether *that* trace is acceptable according to your specification, THEN you can formalize the specification implicitly defined by your program in any proof assistant (because you can, at the very least, simply describer your program within the formal logic). The converse is not true; you can express *more* specifications in formal logic than the ones for which an evaluator program can be written.= When wondering whether X property can be formalized, ask yourself whether you can write a program that evaluates this property. Now think of this specification (literally *this* string): =E2=80=9CTHE P= ROGRAM DOES WHAT I WANT IT TO DO=E2=80=9D. This is too vague (both for an human = and for formal logic) and can not be formalized. > * Is there a proof that demonstrates that the verification will take a > maximum amount of computing resources? (let's say polinomial on some > metric of the program's code). The question can be interpreted in at least 2 ways: (1): If you mean the computer time to verify an *already done* proof: It is worth noting that when computer-verified proofs are involved, an human usually writes a *sketch of proof* that can be seen as a guide for the computer to generate the actual proof and check that it is valid. The actual proofs (in the underlying logic) involve a lot of repetitive work that can be automated. By writing only a proof sketch instead of the full proof this work can be left to the computer. In practice, proofs of the aforementioned type are fast to verify; the time to verify is roughly proportional to the total length of all *proofs* (not the number of theorems). It does not grow exponentially (or something like that) because the human who writes the proof must do the =E2=80=9Creasoning=E2=80=9D that requires =E2=80=9Cinsight=E2=80=9D, = =E2=80=9Ccreativity=E2=80=9D, etc. For example, in HOL4 and HOL Light the user rarely writes actual proofs; instead he writes programs that *generate* the proofs. For each step in the actual proof a function call is made to a module called =E2=80=9CThm=E2=80=9D (theorem) requesting that this step is perfo= rmed. If and only if all steps are valid, then an object of type =E2=80=9Cthm=E2=80=9D= (theorem type) is generated. Thus, if there are =E2=80=9Cbugs=E2=80=9D the program can f= ail to produce a theorem object, but it will not produce a =E2=80=9Cfalse=E2=80=9D theor= em. On the other hand, in Metamath the user must write the whole proof, not just a proof sketch. (2): If you mean the time that it would take a computer to verify that a real-life program meets a specification *without the human giving any advice*, then this would be unpractical for real-life software. That is why a human must write a proof/proof sketch. If you are interested in addressing this question from a *purely theoretical* view, then search the mathematical *literature* (Wikipedia does not count) for Rice theorem= =2E > * Are there reliable methods for estimating the amount of man/hours > (give or take one order of magnitude) required for creating a > verifiable formal specification from some informal specification > language used in the industry? I do not know of such a method. My guess is a person that is knowledgeable in *both* formal verification and the area of the program to be verified (e.g.: avionics, kernels, compilers, etc.) can give an educated estimate is. You may want to check about existing projects of formalizations of informal specifications. > * Are there studies that, based on past practice, demonstrate that the > formal approach is more economic than the traditional one, either > along the development phase or along the complete life cycle of the > software? When reliability is the top priority, formal verification is the only option. Hence, no comparison of cost can be done As for programs where reliability is not a priority, I have seen some studies comparing cost, but I do not recall the full reference. A search in your preferred academic search engine should give some relevant result= s. But like I said already, for me a program that lacks a proof of correctness is unfinished, just like a program that lacks documentation is unfinished. > Categorizing software as "cheap" or "reliable" misses the point > entirely. Either the software is adequate or not. And the adequateness > criteria varies wildly, but two things are always present: if your > sofware is more expensive than the value it provides, it is inadequate;= > if your software takes too much time to develop, it is inadequate. One can speak of =E2=80=9Cthe money the user is willing to pay for the software=E2=80=9D, but speaking of =E2=80=9Cthe *value* of the software=E2= =80=9D is so vague that its meaningless. Imagine a car-manufacturing company. If the cars use =E2=80=9Cdrive-through-wire=E2=80=9D (i.e.: the user only controls the in= put to a computer, not the actual mechanical controls of the car; those are controlled by the computer), then what is the *value* of proving correct the software of the computerized control system? An owner of the care probably would say that the company must pay whatever it costs, because his life is at risk. The stock holders will disagree. > Many years ago I felt in love with mathematical logic and devoted many > many (that's two manys) hours to its study. In the end I decided that > was impractical and sterile and forgot almost everything. Of course. Anybody studying mathematics (by which I mean deductive sciences in general) without an interest of learning it *for its own sake*, regardless of any practical application, is doomed to failure. > Since, > automatic theorem provers got much better to the point of being usable > for certain types of problems. Note that proof assistants are different form automated theorem provers. Proof assistants verify your proof and tell you what you need to prove as you write the proof sketch (mentioned above). With automated theorem provers, you give them a conjecture and axioms and they either provide a proof, terminate without proof, or fail to terminate. In practice there is limited (so far) application of automated theorem proving for proof assistants but the situation is improving. For example, HOL4 has several automated provers built-in; Several are specific-purpose; for example, arithmetic decision procedures. MESON and METIS are general purpose provers but they can only solve simple goals. The tool holyhammer which is part of HOL4 can interface with external provers. > Right now, I'm looking forward to > implementing dependent types on my programming language. I have Coq and= > Idris [=E2=80=A6] Note that those are not automated theorem provers. Coq and Idris are proof verifiers/proof assistants and programming languages (not all proof verifiers are programming languages; these are specific cases). > With age, I turned skeptic about new things. If formal methods is the > silver bullet, the proponents are those who must provide evidence [=E2=80= =A6] I mentioned to you some verified software. The problem is not that the people advancing formal methods are failing, but that typical programmers are way too stupid, unmotivated, lazy and overall mediocre (just like the population in general). Such is the mediocrity that typical C programs are full of UD behavior (e.g.: type punning and undefined behavior with pointer arithmetic). Do you think that the same programmers who write this code (that obviously do not even bother studying the details of their programming language) will bother learning serious mathematics? Obviously not. Writing provably correct software is much harder than writing buggy software. Nearly all programmers write buggy software and count bugs as a =E2=80=9Cnormal thing=E2=80=9D just like rain. Programming is easy; doing it right is hard, very hard (and note that testing is not =E2=80=9Cdoing it right=E2=80=9D). --=20 Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=3Dhow+to+(become+OR+eat)+vegan --4Jxqs9egGX6k66nM1NDsClKOUo63NxpOE Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- iHUEARMIAB0WIQS+wkyTBs7vJfjGA262380TuSZA2QUCWc6rbAAKCRC2380TuSZA 2bHGAQDpc3thYDjmklS2QDny1wFCVDSGHIw5wSZLJMmSfJ3CwgEAnu/OrNtfMMc1 OxAV3mZ+4md/0920D8RJB3if0/2mJms= =waPj -----END PGP SIGNATURE----- --4Jxqs9egGX6k66nM1NDsClKOUo63NxpOE--