Greetings, I'm trying to understand how hypervisor functionality support is working in seL4 for aarch32/aarch64. In the documentation there is a list of platforms [1] for some of them ARM_HYP is said to be supported for some not. I was trying to grep through the kernel, but it seemed to me that ARM_HYP can be enabled on any ARM-based platform. I've tried to compile sel4test for exynos5422 (for which ARM_HYP is said to be enabled) and odroidc2 (for which it is said that it's not supported) with -DARM_HYP=ON manually set, and for both compilation succeeded. It failed for hikey, that should support it, but that's a different story. So my questions are - How is it defined whether ARM_HYP is supported for a board/SoC, provided that processor architecture supports it? What the platform support code should provide for hypervisor to work? - For platforms not supported by camkes-arm-vm (like, most of the platforms) how ARM_HYP can be tested? Thanks a lot, Anton Gerasimov [1] https://docs.sel4.systems/Hardware/