Thanks for your reply. It helped me and enhanced my desision. Perhaps there are still something sensitive...
Reiner, I am curious to see your new paper. It seems not in your homepage.I learned from the vtpm page but not enough, not like your MAC+XEN page with 2 research reports. And now I re-read your the last report which obviously mentioned the separation kernel and the isolation mechanism Xen has provided and hold the positon that it has strong ensurrance enough.
The research work seems too much a work for me alone,and with the available time of 3-4 months. I have to say I cannot give concret example now because I am not familiar with xen 3.0 code enough and the reaserch of formal method already taking a long time is not satisfying. Until now, from the mapping of noninterfrerence model, I can only conclude the rules of labelling virtual resource, mutex protecting and control isolation of I/O device, which depressed me a lot. It seems no use in practice at all(I am writing a paper about it) and I think this infomation-flow analyse method is not fit for high-level abstraction of Xen VMM system.
But I am sure not to do something with covert channel analyse, I try to analyse and verify the isolation property of Xen with formal method in the case of wide sharing of vitrual resouce. And with the help of TPM, to verify or attest the system's TCB. I think MAC dose not confine TCB.The direction seems worthy,but I havn't found good weapon yet,isn't it?
>We are extending the MAC into I/O virtualization (which happens on operating system level).
You must say the situation of DomU?
_______________________________________________ Xense-devel mailing list Xense-devel@xxxxxxxxxxxxxxxxxxx http://lists.xensource.com/xense-devel