Hi Corey, It is definitely an interesting problem, although only occurs since Linux 'relies' on ASLR in the kernel for security due to running untrustworthy code in kernel mode. seL4 does not implement KASLR, as seL4 does not have the classes of bugs that ASLR attempts to mitigate the exploitability of. From that side, there is nothing for us to do. Otherwise you are also correct, probing microarchitectural state to determine what another process is doing is a known and currently unsolvable[1] problem. Adrian [1] As far as is currently known and possible by the hardware ISA without truly prohibitive performance costs On Mon 25-Dec-2017 10:37 AM, Corey Richardson wrote:
https://lwn.net/Articles/738975/
That's really painful, for Linux ;) I don't think seL4 is really impacted? I'm having a hard time thinking about what sensitive information could be disclosed by probing the kernel window. Maybe which memory regions caps being accessed by other concurrently running threads occupy? You could use that to make a covert channel, if the two threads trying to communicate are running in parallel. It seems really dubious that that could give you anything useful otherwise, and as the literature shows timing side channels are unavoidable on x86.
Thought it was interesting and worth sharing!