From: "Mario Castelán Castro" <marioxcc.MT@yandex.com>
To: help-gnu-emacs@gnu.org
Subject: Re: CVE-2017-14482 - Red Hat Customer Portal
Date: Mon, 25 Sep 2017 16:23:49 -0500 [thread overview]
Message-ID: <d90a0ba7-867c-7e5a-20b4-c294635a1ce2@yandex.com> (raw)
In-Reply-To: <867ewnae8k.fsf@zoho.com>
[-- Attachment #1: Type: text/plain, Size: 1678 bytes --]
On 24/09/17 18:06, Emanuel Berg wrote:
> Hold - perhaps the verification has to be
> verified as well?
What any proof of correctness proves is an implication saying roughly:
“IF the environment meets these requisites THEN the program does […]”.
The “bugs” described in the aforementioned paper are not a flaw in the
proof. The source of the problem is that EITHER the programs under test
were being used in an environment does not meet the requisites (i.e.:
“IF the environment meets”) OR the user was expecting the program to do
something different than what is guaranteed by the conclusion “the
program does […]”.
> C'mon now, this is just another
> Computer Science hangup. Just like
> functional programming, or testing for that
> matter - which also is an academic pursuit, by
> the way! [1] - but as always, there is no
> silver bullet solution.
This is the prevalent attitude among programmers, and this is the reason
that we are showered by an endless stream of security patches and bug fixes.
> If I'd send the space fleet to the oldest
> galaxies of the universe, I'd like all methods
> anyone could think of to make as sure as
> possible the software is correct.
>
> I'd start with very skilled and motivated
> programmers, proceed with sound programming
> practices, then code review, and then
> excessive testing.
>
> I suppose formal verification would be
> a distant fourth.
Well, then it is a very good thing that you are NOT in charge of
designing that piece of software.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 228 bytes --]
next prev parent reply other threads:[~2017-09-25 21:23 UTC|newest]
Thread overview: 68+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-09-21 21:51 CVE-2017-14482 - Red Hat Customer Portal ken
2017-09-21 22:03 ` Kaushal Modi
2017-09-21 23:07 ` ken
2017-09-22 7:37 ` Alberto Luaces
2017-09-22 7:48 ` Emanuel Berg
2017-09-22 20:12 ` Mario Castelán Castro
2017-09-22 22:14 ` Emanuel Berg
2017-09-24 2:08 ` Mario Castelán Castro
[not found] ` <mailman.1063.1506218941.14750.help-gnu-emacs@gnu.org>
2017-09-24 6:47 ` Emanuel Berg
2017-09-24 13:38 ` Mario Castelán Castro
2017-09-24 14:42 ` Óscar Fuentes
2017-09-24 14:54 ` tomas
2017-09-26 18:57 ` Narendra Joshi
2017-09-24 23:06 ` Emanuel Berg
2017-09-25 21:23 ` Mario Castelán Castro [this message]
2017-09-25 21:49 ` Emanuel Berg
2017-09-26 1:43 ` Mario Castelán Castro
2017-09-26 2:17 ` Emanuel Berg
2017-09-25 21:11 ` Mario Castelán Castro
2017-09-25 23:58 ` Óscar Fuentes
2017-09-26 14:46 ` Mario Castelán Castro
2017-09-26 23:31 ` Óscar Fuentes
2017-09-29 20:21 ` Mario Castelán Castro
2017-09-29 12:43 ` Eli Zaretskii
2017-09-29 14:59 ` dekkzz78
2017-09-29 16:51 ` Óscar Fuentes
2017-09-29 17:20 ` Emanuel Berg
2017-09-29 18:27 ` Óscar Fuentes
2017-09-29 19:45 ` Emanuel Berg
2017-09-29 20:06 ` Óscar Fuentes
2017-09-29 23:24 ` Emanuel Berg
2017-09-29 18:03 ` Eli Zaretskii
2017-09-24 23:07 ` Emanuel Berg
2017-09-23 10:05 ` Charles A. Roelli
2017-09-23 12:53 ` Óscar Fuentes
2017-09-23 13:12 ` Eli Zaretskii
2017-09-23 17:18 ` Glenn Morris
2017-09-23 17:34 ` Eli Zaretskii
2017-09-23 20:50 ` Yuri Khan
2017-09-24 2:53 ` Eli Zaretskii
2017-09-24 7:13 ` Philipp Stephani
2017-09-24 18:29 ` Robert Thorpe
2017-09-29 8:17 ` Eli Zaretskii
2017-09-29 20:28 ` Stefan Monnier
2017-09-29 23:28 ` Emanuel Berg
2017-10-03 0:52 ` Stefan Monnier
2017-10-03 1:04 ` Emanuel Berg
2017-09-29 7:11 ` Eli Zaretskii
[not found] ` <mailman.1068.1506237251.14750.help-gnu-emacs@gnu.org>
2017-09-24 7:48 ` Emanuel Berg
2017-09-25 21:26 ` Glenn Morris
2017-09-25 22:02 ` Emanuel Berg
2017-09-25 22:08 ` Ludwig, Mark
2017-09-26 5:50 ` Emanuel Berg
2017-09-26 13:40 ` Ludwig, Mark
2017-09-26 17:46 ` Philipp Stephani
2017-09-26 19:00 ` Ludwig, Mark
2017-09-29 13:23 ` Eli Zaretskii
2017-09-29 9:48 ` Eli Zaretskii
2017-09-26 18:44 ` Narendra Joshi
2017-09-26 18:51 ` Philipp Stephani
[not found] ` <mailman.988.1506161159.14750.help-gnu-emacs@gnu.org>
2017-09-24 6:31 ` Emanuel Berg
2017-09-22 16:40 ` ken
2017-09-22 19:07 ` Emanuel Berg
2017-09-23 20:27 ` Bob Proulx
[not found] ` <mailman.1053.1506198486.14750.help-gnu-emacs@gnu.org>
2017-09-24 6:38 ` Emanuel Berg
2017-09-24 17:17 ` Maxim Cournoyer
2017-09-24 22:38 ` Emanuel Berg
-- strict thread matches above, loose matches on Subject: below --
2017-09-27 10:51 Richard Melville
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=d90a0ba7-867c-7e5a-20b4-c294635a1ce2@yandex.com \
--to=marioxcc.mt@yandex.com \
--cc=help-gnu-emacs@gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/emacs.git
https://git.savannah.gnu.org/cgit/emacs/org-mode.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.