Re: Formal description of system call interface

From: Cyril Hrubis <chrubis@suse.cz>
To: Dmitry Vyukov <dvyukov@google.com>
Cc: linux-api@vger.kernel.org, LKML <linux-kernel@vger.kernel.org>,
	Michael Kerrisk-manpages <mtk.manpages@gmail.com>,
	Thomas Gleixner <tglx@linutronix.de>,
	Sasha Levin <levinsasha928@gmail.com>,
	Mathieu Desnoyers <mathieu.desnoyers@efficios.com>,
	scientist@fb.com, Steven Rostedt <rostedt@goodmis.org>,
	Arnd Bergmann <arnd@arndb.de>,
	carlos@redhat.com, syzkaller <syzkaller@googlegroups.com>,
	Kostya Serebryany <kcc@google.com>,
	Mike Frysinger <vapier@google.com>,
	Dave Jones <davej@codemonkey.org.uk>,
	Tavis Ormandy <taviso@google.com>
Subject: Re: Formal description of system call interface
Date: Mon, 21 Nov 2016 17:10:33 +0100	[thread overview]
Message-ID: <20161121161032.GB27353@rei.lan> (raw)
In-Reply-To: <CACT4Y+aUzdX8NqMu+Y3s53vEmoBw7KysB3g2PEjZ6MyJimki1Q@mail.gmail.com>

Hi!
> Description of "returns fd or this set of errors" looks simple and useful.
> Any test system or fuzzer will be able to verify that kernel actually returns
> claimed return values. Also Carlos expressed interested in errno values
> in the context of glibc.
> I would do it from day one.
> 
> 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.

I'm afraid it may be as well. I would expect that we will end up with
something quite complex with a large set of exceptions from the rules.

> 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".

I will try to thing about this a bit.

-- 
Cyril Hrubis
chrubis@suse.cz