linux-api.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Tavis Ormandy <taviso-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org>
To: Dmitry Vyukov <dvyukov-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org>
Cc: Cyril Hrubis <chrubis-AlSwsSmVLrQ@public.gmane.org>,
	linux-api-u79uwXL29TY76Z2rM5mHXA@public.gmane.org,
	LKML <linux-kernel-u79uwXL29TY76Z2rM5mHXA@public.gmane.org>,
	Michael Kerrisk-manpages
	<mtk.manpages-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org>,
	Thomas Gleixner <tglx-hfZtesqFncYOwBW4kG4KsQ@public.gmane.org>,
	Sasha Levin
	<levinsasha928-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org>,
	Mathieu Desnoyers
	<mathieu.desnoyers-vg+e7yoeK/dWk0Htik3J/w@public.gmane.org>,
	scientist-b10kYP2dOMg@public.gmane.org,
	Steven Rostedt <rostedt-nx8X9YLhiw1AfugRpC6u6w@public.gmane.org>,
	Arnd Bergmann <arnd-r2nGTMty4D4@public.gmane.org>,
	carlos-H+wXaHxf7aLQT0dZR+AlfA@public.gmane.org,
	syzkaller <syzkaller-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org>,
	Kostya Serebryany <kcc-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org>,
	Mike Frysinger <vapier-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org>,
	Dave Jones
	<davej-rdkfGonbjUTCLXcRTR1eJlpr/1R2p/CL@public.gmane.org>
Subject: Re: Formal description of system call interface
Date: Mon, 21 Nov 2016 07:34:49 -0800	[thread overview]
Message-ID: <CAJ_zFkL3D5dzn+h1ydNg9rF11wrsyCv6uhp5=VNH82d4E5ewUA@mail.gmail.com> (raw)
In-Reply-To: <CACT4Y+aUzdX8NqMu+Y3s53vEmoBw7KysB3g2PEjZ6MyJimki1Q-JsoAwUIsXosN+BqQ9rBEUg@public.gmane.org>

On Mon, Nov 21, 2016 at 7:14 AM, Dmitry Vyukov <dvyukov-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org> wrote:
>
>
> Re more complex side effects. I always feared that a description suitable
> for automatic verification (i.e. zero false positives, otherwise it is useless)
> may be too difficult to achieve.
>
> Cyril, Tavis, can you come up with some set of predicates that can be
> checked automatically yet still useful?
> We can start small, e.g. "must not alter virtual address space".

Yes, I've been working on creating something like this, I have a
simple working prototype. I cant promise it has zero false positives
right now, but I think that is achievable.

Let me dig it up (I had put it on the back burner).

Tavis.

  parent reply	other threads:[~2016-11-21 15:34 UTC|newest]

Thread overview: 14+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2016-11-06 22:39 Formal description of system call interface Dmitry Vyukov
     [not found] ` <CACT4Y+YYgs43nJnyg3B9cHWOue62iMW3ZgXQKiKG12A1NVMgtg-JsoAwUIsXosN+BqQ9rBEUg@public.gmane.org>
2016-11-07  0:28   ` Szabolcs Nagy
2016-11-21 15:03     ` Dmitry Vyukov
     [not found]       ` <CACT4Y+bq97OPqW9nUoQWDdVfeCv6oOYT0=GeFmOu2rosBz4s2Q-JsoAwUIsXosN+BqQ9rBEUg@public.gmane.org>
2016-11-22 13:07         ` Szabolcs Nagy
2016-11-07 10:38   ` Cyril Hrubis
     [not found]     ` <20161107103819.GA11374-2UyX9mZUyMU@public.gmane.org>
2016-11-21 15:14       ` Dmitry Vyukov
     [not found]         ` <CACT4Y+aUzdX8NqMu+Y3s53vEmoBw7KysB3g2PEjZ6MyJimki1Q-JsoAwUIsXosN+BqQ9rBEUg@public.gmane.org>
2016-11-21 15:34           ` Tavis Ormandy [this message]
2016-11-21 16:10           ` Cyril Hrubis
2016-11-21 15:37     ` Steven Rostedt
     [not found]       ` <20161121103752.70ad1418-f9ZlEuEWxVcJvu8Pb33WZ0EMvNT87kid@public.gmane.org>
2016-11-21 15:48         ` Dmitry Vyukov
2016-11-21 16:58           ` Cyril Hrubis
2017-04-21 15:14   ` Carlos O'Donell
2016-11-11 17:10 ` Andy Lutomirski
2016-11-21 15:17   ` Dmitry Vyukov

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='CAJ_zFkL3D5dzn+h1ydNg9rF11wrsyCv6uhp5=VNH82d4E5ewUA@mail.gmail.com' \
    --to=taviso-hpiqsd4aklfqt0dzr+alfa@public.gmane.org \
    --cc=arnd-r2nGTMty4D4@public.gmane.org \
    --cc=carlos-H+wXaHxf7aLQT0dZR+AlfA@public.gmane.org \
    --cc=chrubis-AlSwsSmVLrQ@public.gmane.org \
    --cc=davej-rdkfGonbjUTCLXcRTR1eJlpr/1R2p/CL@public.gmane.org \
    --cc=dvyukov-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org \
    --cc=kcc-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.org \
    --cc=levinsasha928-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org \
    --cc=linux-api-u79uwXL29TY76Z2rM5mHXA@public.gmane.org \
    --cc=linux-kernel-u79uwXL29TY76Z2rM5mHXA@public.gmane.org \
    --cc=mathieu.desnoyers-vg+e7yoeK/dWk0Htik3J/w@public.gmane.org \
    --cc=mtk.manpages-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org \
    --cc=rostedt-nx8X9YLhiw1AfugRpC6u6w@public.gmane.org \
    --cc=scientist-b10kYP2dOMg@public.gmane.org \
    --cc=syzkaller-/JYPxA39Uh5TLH3MbocFFw@public.gmane.org \
    --cc=tglx-hfZtesqFncYOwBW4kG4KsQ@public.gmane.org \
    --cc=vapier-hpIqsD4AKlfQT0dZR+AlfA@public.gmane.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.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).