2 citations · 4 across the 3 of their papers we have counts for
3 papers
Cerisier: A Program Logic for Attestation in a Capability Machine
June Rousseau, Denis Carnier, Thomas Van Strydonck +3
A key feature in trusted computing is attestation, which allows encapsulated components (enclaves) to prove their identity to (local or remote) distrusting components. Reasoning ab…
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
We propose a calling convention for capability machines with local capabilities. The calling convention ensures local-state encapsulation and well-bracketed control flow. We use th…
StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
We propose and study StkTokens: a new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling conve…