seL4 is verified on RISC-V!



View Reddit by zanedowView Source

Categories: PROGRAMMING

3 Comments

i_am_adult_now · July 23, 2020 at 9:55 am

It’s seriously the fastest microkernel I’ve seen yet. Hope it becomes more mainstream and receives some serious porting efforts.

sna_fu · July 23, 2020 at 1:07 pm

sel4 is an epic achievement. This cannot be said often enough.

However: “When we verify seL4, we have to assume that the hardware operates correctly (i.e. as specified). That assumes that there is an unambiguous specification in the first place, which is not the case for all hardware.” Vendors usually try to be sound wrt to their specifications, but not complete (ie. the specification permits behavior that is not observed on actual hardware) eg. in the context of memory models. This can break properties (specifically multi-run properties) one might be interested in… There is still so much more research and development needed…

vwlsmssng · July 23, 2020 at 1:27 pm

RISC-V blah blah verified blah blah microkernel blah blah

Then they bury the lede at the bottom of the article, how extending the ISA can secure against timing based attacks like Spectre

In [the paper they link to](https://ts.data61.csiro.au/publications/csiro_full_text//Wistoff_SGBH_20.pdf) it says

> We show that the addition of a single-instruction extension to the RISC-V ISA, that flushes microarchitectural state, can enable the OS to close all five evaluated covert channels with low increase in context switch costs and negligible hardware overhead

An important point is made about how open source hardware enables this kind of research, by making it easier for Universities to build and test modified computing hardware to test hypotheses of software / hardware design interaction and leave a route open to the commercial delivery of such improvements

Leave a Reply

Your email address will not be published. Required fields are marked *