Cerisier is the first mechanized program logic for modular reasoning about trusted, untrusted, and attested code in capability machines, with a universal contract for untrusted code and demonstrations on secure computation and mutual attestation.
In 2015 IEEE Symposium on Security and Privacy
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
MSWasm adds colored memory and pointers to Wasm, proves well-typed programs are robustly memory safe, and shows a C compiler plus native backends with 22-198% overhead.
NanoTag enables byte-granular overflow detection on unmodified MTE binaries by combining hardware tagging with selective software tripwire checks on the Scudo allocator.
citing papers explorer
-
Cerisier: A Program Logic for Attestation in a Capability Machine
Cerisier is the first mechanized program logic for modular reasoning about trusted, untrusted, and attested code in capability machines, with a universal contract for untrusted code and demonstrations on secure computation and mutual attestation.
-
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
MSWasm adds colored memory and pointers to Wasm, proves well-typed programs are robustly memory safe, and shows a C compiler plus native backends with 22-198% overhead.
-
NanoTag: Systems Support for Efficient Byte-Granular Overflow Detection on ARM MTE
NanoTag enables byte-granular overflow detection on unmodified MTE binaries by combining hardware tagging with selective software tripwire checks on the Scudo allocator.