I know that seL4 provides confidentiality, which is described as a property that "means that data cannot be read without permission." Given this wording, I wonder if it is not possible to revoke those permissions in certain cases. In particular, I would like for one camkes component to be able to perform runtime measurements, such as heap analysis, on another component. Or even better, I would like for a component to be able to perform runtime measurements on a program running within the camkes linux vm. Is such a feat possible?
Best, Michael Neises