On 11/03/15 04:02, Tim Newsham wrote: > Your article says: > "Second, the mapping database keeps records about how mappings got > established. Thereby, the memory required for storing this information > in the kernel depends on the behaviour of the user land. As a > consequence, a malicious user-level program is able to provoke a high > consumption of kernel memory by establishing mappings. Eventually, > this represents an attack vector for denial-of-service attacks onto > the kernel." >
As Gerwin says, this paragraph applies to traditional L4 kernels, not seL4. Indeed, it would not only allow denial-of-service attacks, but also trivial covert storage channels that make it impossible for the kernel to enforce confidentiality. seL4's proof of confidentiality (information flow enforcement) rules out such channels [1], and would have been a lot more difficult without seL4's memory management model that deviates from traditional L4. Note that recently work on Fiasco.OC has demonstrated how to exploit these kinds of covert channels to break confidentiality [2], so this is by no means just an academic curiosity. Cheers Toby [1] https://www.nicta.com.au/pub-download/full/6464/ [2] https://eprint.iacr.org/2014/984.pdf ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
