Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1754766AbcKUPPV (ORCPT ); Mon, 21 Nov 2016 10:15:21 -0500 Received: from mail-wm0-f41.google.com ([74.125.82.41]:35636 "EHLO mail-wm0-f41.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1754175AbcKUPPT (ORCPT ); Mon, 21 Nov 2016 10:15:19 -0500 MIME-Version: 1.0 In-Reply-To: <20161107103819.GA11374@rei.lan> References: <20161107103819.GA11374@rei.lan> From: Dmitry Vyukov Date: Mon, 21 Nov 2016 16:14:57 +0100 Message-ID: Subject: Re: Formal description of system call interface To: Cyril Hrubis Cc: linux-api@vger.kernel.org, LKML , Michael Kerrisk-manpages , Thomas Gleixner , Sasha Levin , Mathieu Desnoyers , scientist@fb.com, Steven Rostedt , Arnd Bergmann , carlos@redhat.com, syzkaller , Kostya Serebryany , Mike Frysinger , Dave Jones , Tavis Ormandy Content-Type: text/plain; charset=UTF-8 Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Length: 2498 Lines: 52 On Mon, Nov 7, 2016 at 11:38 AM, Cyril Hrubis wrote: > Hi! >> We identified a surprisingly large number of potential users for such >> descriptions: >> - fuzzers (syzkaller, trinity, iknowthis) >> - strace/syscall tracepoints (capturing indirect arguments and >> printing human-readable info) >> - generation of entry points for C libraries (glibc, liblinux >> (raw syscalls), Go runtime, clang/gcc sanitizers) >> - valgrind/sanitizers checking of input/output values of syscalls >> - seccomp filters (minijail, libseccomp) need to know interfaces >> to generate wrappers >> - safety certification (requires syscall specifications) >> - man pages (could provide actual syscall interface rather than >> glibc wrapper interface, it was noted that possible errno values >> is an important part here) >> - generation of syscall argument validation in kernel (fast version >> is enabled all the time, extended is optional) > > I was thinking of generating LTP testcases from a well defined format for > quite some time. Maybe that would be a good way how to keep the > descriptions to match the reality. > > LTP test would however need a bit more information that just syscall > parameter anotation. We would need also description of the expected > return value in some cases, annotating it as "returns fd" or "zero on > success" would be good enough for basic tests. Better testing would need > to describe the "side efect" as well (file was created, filesystem > mounted, etc.) then we could write a classes of verify functions, > something as check_file_exits() and use them to check the results > accordingly. > > I'm not sure if something like this is really doable or in the scope of > this project, but it may be worth a try. Hi Cyril, I think I heard something similar from Tavis in the iknowthis context. 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. 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".