2 papers
cs.PL2019
Proof Pearl: Magic Wand as Frame
Qinxiang Cao, Shengyi Wang, Aquinas Hobor +1
Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating…
cs.CR2018
BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof
Shweta Shinde, Shengyi Wang, Pinghai Yuan +3
New trusted computing primitives such as Intel SGX have shown the feasibility of running user-level applications in enclaves on a commodity trusted processor without trusting a lar…