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