You're responding to a comment where I wrote that I would never use Xen with an argument not to use Xen. All I'm saying is that "formal verification", at least as it exists in current systems, is not why I wouldn't use Xen.

▲

lrvick 12 hours ago | parent [-]

> an argument not to use Xen

Not my intent but perhaps I communicated poorly. It was an argument that the -reason- Xen has had so many bugs is because it was not built for correctness.

Formal verification should be a bare minimum for a TCB component to know many classes of bugs that have plagued the most popular hypervisors cannot happen.

We both clearly agree not to use Xen.

Anyway, I appreciate the engagement on this all the same.

Few even know alternatives to xen exist!

▲

tptacek 12 hours ago | parent [-]

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.

Generally, 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.

	▲	lrvick 9 hours ago \| parent [-]
		> the less your OS can do, apart from strictly hypervising guest operating systems, the safer you probably are 100% 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.