2 papers
cs.CR2025
Cryptis: Cryptographic Reasoning in Separation Logic
Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi
We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of sep…
cs.PL2024
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Zoe Paraskevopoulou, Michael Fitzgibbons, Michelle Thalakottur +3
Safe, shared-memory interoperability between languages with different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result i…