8 ms·

You usually prove something with formal verification, and it fails when the assumptions of the underlying model are wrong. Take the axioms with a grain of salt

You usually prove something with formal verification, and it fails when the assumptions of the underlying model are wrong. Take the axioms with a grain of salt.

rurban 7y ago
Exactly, the array offset rules are missing important parts. Not just bounds checks, but also offsets larger than a page table need to be forbidden. (Spectre). IMHO arrays should be forbidden at all, replaced by a secure hash map, with a max size.
- monocasa 7y ago
  Way to completely destroy perf by making your memory accesses totally random.
  - rurban 7y ago
    Exactly, People need to feel how bad it is to allow anyone getting user-space access into the kernel. It needs to hurt. But the prime reason is security. solaris and freebsd do have their reasons to disallow arrays in their kernel hooks.
    - monocasa 7y ago
      Most Spectre variants are exploitable via specially crafted data, not just code injection. Hell, NetSpectre is remotely exploitable. Being super ascetic about what code is allowed in the kernel isn't an endgame here. We don't need to take cross domain VMs completely off the table; we just need better ways of describing those security boundaries to the hardware. It's been done before. Some of Azul's secret sauce was additional cheap security modes in the MMU that they leveraged for their GC.
      - AstralStorm 7y ago
        That works, sort of, but how do you even ensure the hardware is actually working? Trust Intel or ARM after what they've shown? And trying to fully bypass cache and speculation when doing userspace to/from kernel transfers is going to suck. Remapping pages also. And if MMU is untrustworthy, well...
        monocasa 7y ago
        > That works, sort of, but how do you even ensure the hardware is actually working? Trust Intel or ARM after what they've shown? Which part are you referring to? > And trying to fully bypass cache and speculation when doing userspace to/from kernel transfers is going to suck. Remapping pages also. Here's a demonstration of doing it remotely, with specially crafted network packets. https://arxiv.org/abs/1807.10535 https://arxiv.org/abs/1807.10535 It's not as hard as you're making it seem, the root here is that hardware is currently broken. > And if MMU is untrustworthy, well... If the MMU is untrustworthy, it doesn't matter if you allow a cross domain VM or not.

You usually prove something with formal verification, and it fails when the assumptions of the underlying model are wrong. Take the axioms with a grain of salt.

rurban 7y ago

Exactly, the array offset rules are missing important parts. Not just bounds checks, but also offsets larger than a page table need to be forbidden. (Spectre). IMHO arrays should be forbidden at all, replaced by a secure hash map, with a max size.

monocasa 7y ago
Way to completely destroy perf by making your memory accesses totally random.
- rurban 7y ago
  Exactly, People need to feel how bad it is to allow anyone getting user-space access into the kernel. It needs to hurt. But the prime reason is security. solaris and freebsd do have their reasons to disallow arrays in their kernel hooks.
  - monocasa 7y ago
    Most Spectre variants are exploitable via specially crafted data, not just code injection. Hell, NetSpectre is remotely exploitable. Being super ascetic about what code is allowed in the kernel isn't an endgame here. We don't need to take cross domain VMs completely off the table; we just need better ways of describing those security boundaries to the hardware. It's been done before. Some of Azul's secret sauce was additional cheap security modes in the MMU that they leveraged for their GC.
    - AstralStorm 7y ago
      That works, sort of, but how do you even ensure the hardware is actually working? Trust Intel or ARM after what they've shown? And trying to fully bypass cache and speculation when doing userspace to/from kernel transfers is going to suck. Remapping pages also. And if MMU is untrustworthy, well...
      - monocasa 7y ago
        > That works, sort of, but how do you even ensure the hardware is actually working? Trust Intel or ARM after what they've shown? Which part are you referring to? > And trying to fully bypass cache and speculation when doing userspace to/from kernel transfers is going to suck. Remapping pages also. Here's a demonstration of doing it remotely, with specially crafted network packets. https://arxiv.org/abs/1807.10535 https://arxiv.org/abs/1807.10535 It's not as hard as you're making it seem, the root here is that hardware is currently broken. > And if MMU is untrustworthy, well... If the MMU is untrustworthy, it doesn't matter if you allow a cross domain VM or not.