Hey Indan, After reading your (and others) words, it finally clicked for me! Like you (and others) have said in seL4 all interaction are done by invoke objects via capabilities. It sounds obvious at first (many resources talk about this), but understanding is another story:) In case there are others like me that are still having a problem understanding system calls and object methods in seL4, I have collected my thoughts below. System call is, in a more "traditional" sense, in other OSes is like this: - execute 'syscall' with a specific system call number from the user space - there are many syscall numbers defined in those OSes (e.g., read, write, mkdir) In seL4, however, it's a bit different: - still execute 'syscall' from the user space - but this time only Send, Recv, Yield (and other variations) have their syscall numbers defined - those are the only "system calls" that we can directly compare to other "traditional" OSes - now, in handling of the system calls (e.g., Send()) there is a decoder (see 'decodeInvocation(...)') - those decoders determine which specific capability to invoke (see 'libsel4/include/interfaces/sel4.xml' for all invocations) - each of the invocations have their own numbers (similar to system call numbers) - so (like Indan have said) we have a two-tiered system (first is architecture/CPU 'syscall' and second is seL4 'invocations') - because of this we have a separation in API reference between System Calls and Object Methods - and since object methods (like UntypedRetype) are handled inside the seL4 they are executed at higher privilege level Again, thanks everyone for the help & replies. -T