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
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 , 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 , so this is by no
means just an academic curiosity.
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.