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?