>>>>> "Comet" == Comet  <yjy7...@126.com> writes:

Comet> Hi, I am using Camkes to develop VM virtualization, but I have
Comet> a question that is how can I ensure isolation security between
Comet> virtual machines?

seL4 guarantees memory isolation, and with the new MCS kernel can be
configured to protect against some timing channels.  However if your
VMs are connected by network or other communication channels, these
bypass seL4's isolation mechanisms.  You need to use conventional
techniques like fail2ban and firewalls to protect them.

Comet> If a virus with a Trojan is installed on the
Comet> VMM, will the virtual machines attack each other?

They could.

Comet> and will the kernel be corrupted ?

No.  The kernel cannot be corrupted by the VMM, or a VM running on top
of it.

Comet> I didn't find some security instructions
Comet> about the system developed by Camkes, or the implementation
Comet> principle of Camkes, that is, how is resource mapping between
Comet> seL4 and Camkes?

Take a look at the SMACCM project.  Starting point
https://trustworthy.systems/projects/TS/SMACCM/

In particular the final report at
https://www.trustworthy.systems/publications/csiro_full_text/Cofer_BGDWKKHPFPSGW_17:tr.pdf
may be helpful

-- 
Dr Peter Chubb                https://trustworthy.systems/
Trustworthy Systems Group                        CSE, UNSW
Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to