I've done some further analysis of the situation on aarch64 and x86_64.
On aarch64 the cpu register used for the seL4 system call number is not part of the linux syscall ABI. Therefore, any linux system call could trigger one of the seL4 syscalls that do not raise an exception resulting in the system call not being emulated.
On x86_64 the cpu register used for the seL4 system call number is used as the third argument to a linux system call. Therefore, if any linux system call happens to use one of seL4 system call number constants that do not raise an exception as its third argument the system call will not be emulated.
As such, I do not think it is possible to reliably trap linux system calls on these architectures.
This should be fixed.
- JB
--
Analysis
aarch64:
reg seL4[3] linux[2]
--- -------- --------
x0 dest/src arg1
x1 info arg2
x2 mr0 arg3
x3 mr1 arg4
x4 mr2 arg5
x5 mr3 arg6
x6 reply -
x7 sysno -
x8 dest (*) sysno
x86_64:
reg seL4[1] linux[2]
--- -------- --------
rax - sysno
rdx sysno arg3
rdi dest/src arg1
rsi info arg2
r8 mr1 arg5
r9 mr2 arg6
r10 mr0 arg4
r12 reply -
r13 dest (*) -
r15 mr3 -
(*) only used with NBSendRecv
The seL4 system call number constants of concern (on MCS)[4] include:
NBSend: -6
Yield: -11
--
References
[1] https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/x86_64/se...
[2] https://www.systutorials.com/docs/linux/man/2-syscall/
[3] https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch64/s...
[4] https://github.com/seL4/seL4/blob/master/libsel4/include/api/syscall.xml