Side-channel attacks (Meltdown, Spectre)

[Stefan Kalkowski]

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 at lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/genode-main


-- 
Stefan Kalkowski
Genode labs

https://github.com.skalk | https://genode.org