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/sel4/sel4_arch/syscalls_syscall.h

[2] https://www.systutorials.com/docs/linux/man/2-syscall/

[3] https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/syscalls.h

[4] https://github.com/seL4/seL4/blob/master/libsel4/include/api/syscall.xml
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]

Reply via email to