A Tale of Two Secure Virtual Disks for TEEs: From Provable to Practical Security