Re: Formal description of system call interface

[Dmitry Vyukov]

On Mon, Nov 7, 2016 at 11:38 AM, Cyril Hrubis <chrubis@xxxxxxx> 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".