|
Hi all
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?
Thanks!
Regards
Huang
| 
