There are no off the shelf specs you can certify against for hypervisors in particular. However, the certification of general purpose isolation in a shared tenancy environment is structurally similar to certification against the Separation Kernel Protection Profile (SKPP) [1] as done for INTEGRITY-178B [2].

Unfortunately certification against that standard directly is no longer possible in the normal course because as part of the security assurance requirement (SAR) AVA_VLA_EXP.4 it requires a NSA penetration test and evaluation that identifies no deficiences to cross-verify the proofs of correctness.

However, with the amount of money the US government is spending on AWS it should be trivial for them to get such a certification done if they were competent to actually do it. In addition, you could always just use a comparable standard that replaces AVA_VLA with the standard AVA_VAN which just validates against a “generic nation-state attacker” similar to what PikeOS [3] did. Given that PikeOS is made by a relatively small company, especially compared to something like Amazon or even the just the AWS division, it would again be easy for Amazon to demonstrate such capability if they were competent to do so.

Instead Amazon is 100% guaranteed to fail such a evaluation like how Microsoft failed their evaluations because, like Microsoft, nobody in their organization has ever designed, worked on, or probably even seen a actual high security system and they have no incentive to learn when they can just make up bullshit that people believe. Their organizations and management are structurally incapable of developing secure systems without a complete management and technology replacement.

[1] https://www.niap-ccevs.org/profile/Info.cfm?PPID=65&id=65

[2] https://www.commoncriteriaportal.org/files/epfiles/st_vid101...

[3] https://www.commoncriteriaportal.org/files/epfiles/1146a_pdf...