[arielby]

No. This is a subtle vulnerability that involves the flags in the x86 page table not matching the hypervisor's view of them - not a mere buffer overflow. Ordinary static analysis couldn't have fixed this. Safe languages couldn't have fixed this. Even a complete formal proof would have missed this without a good model.

[lmm]

Disagree. If those flags were properly typed then whoever added superpages would have had to make a decision about whether that was something guests should be allowed to set. Sure, they could still have made the wrong choice, but having the mask for which bits are allowed defined separately makes it much easier for a programmer to simply forget.

Heck, even without a type system, the problem is that the check is backwards. There shouldn't be a mask of flags that the guest isn't allowed to set, the flags should have been &ed with a mask that says which flags they are allowed to set, that way any new flag would have been disallowed by default.

[makomk]

The mask of flags that the guest isn't allowed to set is created by taking a whitelist of flags that it is allowed to set and inverting it, so that every flag that's not explicitly allowed is denied. They're flags that the guest was intentionally granted the ability to change. The problem is that Xen subtly mishandled the consequences of a guest changing them in a way that wouldn't affect normal guests. I haven't seen a solution to this that doesn't, in the end, basically boil down to not making that mistake in the first place.

[walterbell]

I wonder which pen-testing techniques were used by Alibaba to find this vulnerability.