As Theo DeRaadt said
You are absolutely deluded, if not stupid, if you think that
a worldwide collection of software engineers who can't write
operating systems or applications without security holes,
can then turn around and suddenly write virtualization
layers without security holes.
I caught someone in a meeting last week trying to sell another employee on the security benefits of virtualization and I nearly bit my tongue off.Given that virtualization is the de facto standard deployment technology for the majority of all new applications, it's worth knowing the specific limitations.
I think this is the original source of the confusion, which has since disseminated to those who don't understand the nuances and think that virtualization adds security in every case.
The PCI DSS requires that each server just has one purpose. I was surprised when in a later version they explicitly allowed virtualization as a way to comply with that requirement.
I'm not trying to suggest that a virtualization layer with formal proofs of correctness is a security panacea (it's not--correctness is necessary but not sufficient for security). What I am suggesting is that there is a way forward to developing secure virtualization layers.
If anything, this paper suggests to me that it would be best if the lowest layer in the stack (be it the OS or the hypervisor) implemented some of the crypto primitives on behalf of the applications. I can't see any other way to run them while also guaranteeing that (1) their execution is correct with the specification, (2) they run in full isolation from one another, and (3) they avoid timing attacks and whatever side-channels we can think of.
The feature list certainly looks impressive!
If you need something that speaks TLS, then no. NaCl is a different (simpler) protocol that does not have TLS compatibility as a goal.
If you're building a new application then NaCl is probably a good choice. There are some problems you may need to solve yourself, if your application calls for them. For example, NaCl has no notion of a CA hierarchy.
If you are writing a new application then read on.
There are 2 NaCl alternatives to consider as well: Sodium (API compatible) [2], TweetNaCl (small, auditable) [1].
There are higher-level protocols that uses NaCl, CurveCP [3] for UDP, and CurveZMQ for TCP[4], although "CurveCP software isn't ready for users yet".
[1] http://tweetnacl.cr.yp.to/ [2] http://doc.libsodium.org/
[3] http://curvezmq.org/page:read-the-docs [4] http://curvecp.org/