From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <linux-kernel-owner@vger.kernel.org>
Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand
        id S1754782AbcKUPfN (ORCPT <rfc822;w@1wt.eu>);
        Mon, 21 Nov 2016 10:35:13 -0500
Received: from mail-qt0-f177.google.com ([209.85.216.177]:34536 "EHLO
        mail-qt0-f177.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org
        with ESMTP id S1754185AbcKUPfL (ORCPT
        <rfc822;linux-kernel@vger.kernel.org>);
        Mon, 21 Nov 2016 10:35:11 -0500
MIME-Version: 1.0
In-Reply-To: <CACT4Y+aUzdX8NqMu+Y3s53vEmoBw7KysB3g2PEjZ6MyJimki1Q@mail.gmail.com>
References: <CACT4Y+YYgs43nJnyg3B9cHWOue62iMW3ZgXQKiKG12A1NVMgtg@mail.gmail.com>
 <20161107103819.GA11374@rei.lan> <CACT4Y+aUzdX8NqMu+Y3s53vEmoBw7KysB3g2PEjZ6MyJimki1Q@mail.gmail.com>
From: Tavis Ormandy <taviso@google.com>
Date: Mon, 21 Nov 2016 07:34:49 -0800
Message-ID: <CAJ_zFkL3D5dzn+h1ydNg9rF11wrsyCv6uhp5=VNH82d4E5ewUA@mail.gmail.com>
Subject: Re: Formal description of system call interface
To: Dmitry Vyukov <dvyukov@google.com>
Cc: Cyril Hrubis <chrubis@suse.cz>, 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>
Content-Type: text/plain; charset=UTF-8
Sender: linux-kernel-owner@vger.kernel.org
List-ID: <linux-kernel.vger.kernel.org>
X-Mailing-List: linux-kernel@vger.kernel.org

On Mon, Nov 21, 2016 at 7:14 AM, Dmitry Vyukov <dvyukov@google.com> 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.