Hi,
On Fri, Jan 05, 2018 at 08:24:19PM +0100, Alexander Boettcher wrote:
Hi Udo,
On 05.01.2018 17:36, Udo Steinberg wrote:
Norman Feske (NF) wrote:
NF> In contrast to monolithic kernels, a microkernel like base-hw, NOVA, NF> or seL4 does not deal with any user-level content like cryptographic NF> secrets, or the content of files. There is hardly any credential to NF> leak to begin with. User content stays outside the microkernel.
While it is true that a microkernel stores significantly fewer secrets than a monolithic kernel, like Linux, most microkernels actually have a full mapping of the entire physical memory in the kernel portion of each address space, which allows an attacker to peek anywhere into physical memory.
before starting to dig/read through all our supported kernels (I'm not all familiar with the internals) - can you please elaborate a bit about which microkernels, according to your knowledge, have all physical memory mapped in the kernel ?
The currently supported microkernels for Genode are Pistachio, OKL4, L4/Fiasco, Fiasco.OC, Nova, seL4 and our own hw kernel.
A partial response related to the last mentioned kernel.
I can warrant that the hw kernel, which is actually Genode's core component combined with a bit of architectural dependent data-structures (e.g. page-tables) and routines, does not contain physical memory mappings used by user-level components. The only exception are the UTCBs already mentioned by Norman. Only before memory is handed over to a user-level component, it gets temporarily faded into the kernel/core to fill it with zeroes. Afterwards it gets detached before it is used by other components.
I would wonder if okl4 or sel4 have all physical memory mapped to the kernel area in each address space, because they do not use L4-like memory propagation via synchronous IPC (aka mapping data-base) as far as I know, or do they?
Best regards Stefan
Thanks,
-- Alexander Boettcher Genode Labs
http://www.genode-labs.com - http://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
genode-main mailing list genode-main@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/genode-main