Yeah, all I'm saying is that I agree with you about Xen, but that I don't agree about the centrality of formal methods --- at least on current projects with current verifications, things could get different now that AI lets us be more ambitious with verification --- in determining attack surface.
replyGenerally, the less your OS can do, apart from strictly hypervising guest operating systems, the safer you probably are. Hence why people do things like seL4.
> the less your OS can do, apart from strictly hypervising guest operating systems, the safer you probably are
reply100% agreement here and I -would- take something tiny I can audit myself over something huge and formally verified if forced to choose. Thankfully I do not have to choose.
> AI lets us be more ambitious with verification
Exactly. For TCB code formal verification is a minimum, not sufficient, IMO. Too cheap these days to not have very complete test coverage, formal verification, risc0 execution proofs, seccomp tracing. For security critical code we should demand all of it now.