112 citations · 159 across the 6 of their papers we have counts for
4 papers · 1 filter
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Son Ho, Cédric Fournet, Jonathan Protzenko +7
We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…
Confidential Machine Learning within Graphcore IPUs
Kapil Vaswani, Stavros Volos, Cédric Fournet +9
We present IPU Trusted Extensions (ITX), a set of experimental hardware extensions that enable trusted execution environments in Graphcore's AI accelerators. ITX enables the execut…
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
Martín Abadi, Bruno Blanchet, Cédric Fournet
We study the interaction of the programming construct "new", which generates statically scoped names, with communication via messages on channels. This interaction is crucial in se…
TulaFale: A Security Tool for Web Services
Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon +1
Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for…