Hi Wean,

the existence of undefined behaviour in the ISA is not a problem, you deal with it the same way as in C — you have to avoid it.

We currently don’t do binary verification for x86, but if we did, this would mean the proof obligation would be that the seL4 doesn’t contain any of these behaviours, which is the same proof obligation we have on ARM.

There is a slight problem if such behaviour occurs in user code. We would want to know that this can’t produce any executions that other, “normal” user code couldn’t also produce (including raising an exception). The ARM ISA spec specifically provides that guarantee. I haven’t checked the x86 spec, but it would be very strange if it didn’t, because without something at least very similar, no OS protection would be possible.

Cheers,
Gerwin

On 26.09.2018, at 21:22, Wean Irdeh <wean.irdeh@gmail.com> wrote:

Hi all. I was having discussion about how secure handwritten asm code compared to C code in https://board.flatassembler.net/topic.php?p=206126#206117
and someone mentioned that there are undefined behavior in x86 instruction set

How is these x86 undefined behavior handled in sel4?
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel