On 1/25/23 12:08, Sashidhar Jakkamsetti wrote:
2. In general OS, it is not possible to modify the code section of a
process (which is read-only) at runtime.
Is this accurate? I guess you’re assuming no mmap/mprotect? In general,
it _is_ possible to modify code at runtime on most OSes. Maybe you can’t
literally modify your ELF code section which may be mapped immutably RX,
but you can allocate new RWX memory and then jump into it. This is how
JIT engines used to work. Nowadays they generally allocate something RW,
write code into it, flip to RX, then jump into it. So slightly safer,
but you still have dynamically modified code.
I agree that _not_ having this “feature” seems to make sense for your
use case though. One of the tricky things you may end up having to deal
with is memory aliasing. To prove the contents of an RX page is never
modified, you unfortunately also need to prove no RW alias mappings of
it exist or that no writes to them occur.
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
