23 citations · 25 across the 4 of their papers we have counts for
4 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…
Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
Sander Huyghebaert, Steven Keuchel, Coen De Roover +1
Progress has recently been made on specifying instruction set architectures (ISAs) in executable formalisms rather than through prose. However, to date, those formal specifications…
Uninitialized Capabilities
Sander Huyghebaert, Thomas Van Strydonck, Steven Keuchel +1
This technical report describes a new extension to capability machines. Capability machines are a special type of processors that include better security primitives at the hardware…
Modular, Fully-abstract Compilation by Approximate Back-translation
Dominique Devriese, Marco Patrignani, Frank Piessens +1
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have import…