Re: Formal description of system call interface

On Mon, Nov 7, 2016 at 11:38 AM, Cyril Hrubis [off-list ref] wrote:

Hi!

quoted

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