[seL4] Re: How can I ensure the security of a system developed by Camkes?

...

...

...

...

"Comet" == Comet 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_BGDWKKHPF... 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.