ABSTRACT. Detecting or eliminating vulnerabilities in cryptographic libraries through testing or fuzzing remains a significant challenge. This has led to the adoption of formal verification techniques to establish both functional correctness and side-channel resistance in modern cryptographic software.

In this talk, I will introduce EasyCrypt, a toolset designed to reason about relational properties in probabilistic computations involving adversarial code. EasyCrypt is particularly well-suited for constructing and verifying game-based cryptographic proofs and has been applied successfully to prove the security of sophisticated cryptographic schemes.

Although EasyCrypt facilitates reasoning at the algorithmic level, it does not directly support the development of real-world implementations. To bridge this gap, I will demonstrate how EasyCrypt integrates with the Jasmin programming language, enabling formal security guarantees for highly optimized assembly-level code.

Jasmin is tailored for "assembly-in-the-head" programming, seamlessly blending high-level constructs (like structured control flow and variables) with low-level features (such as assembly instructions and flag manipulation). In the second part of the presentation, I will offer a brief overview of Jasmin and explain how it interacts with EasyCrypt to support the formal verification of practical cryptographic implementations.

ABSTRACT. Detecting or eliminating vulnerabilities in cryptographic libraries through testing or fuzzing remains a significant challenge. This has led to the adoption of formal verification techniques to establish both functional correctness and side-channel resistance in modern cryptographic software.

In this talk, I will introduce EasyCrypt, a toolset designed to reason about relational properties in probabilistic computations involving adversarial code. EasyCrypt is particularly well-suited for constructing and verifying game-based cryptographic proofs and has been applied successfully to prove the security of sophisticated cryptographic schemes.

Although EasyCrypt facilitates reasoning at the algorithmic level, it does not directly support the development of real-world implementations. To bridge this gap, I will demonstrate how EasyCrypt integrates with the Jasmin programming language, enabling formal security guarantees for highly optimized assembly-level code.

Jasmin is tailored for "assembly-in-the-head" programming, seamlessly blending high-level constructs (like structured control flow and variables) with low-level features (such as assembly instructions and flag manipulation). In the second part of the presentation, I will offer a brief overview of Jasmin and explain how it interacts with EasyCrypt to support the formal verification of practical cryptographic implementations.

ABSTRACT. In this tutorial, I will present techniques for automated formal verification of a variety of systems using Satisfiability Modulo Theories (SMT) solvers as main reasoning engines. The talk will focus mainly on the problem of verifying invariant properties on symbolic transition systems, but it will also cover techniques for the verification of Linear Time temporal logic (LTL) properties and extensions to deal with parameterized systems with an unbounded number of components. I will also introduce some concrete tools to solver Verification Modulo Theories problems automatically, and present a demo of their use in a realistic application.

ABSTRACT. Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, fault-injection testing, deterministic simulation, event-based simulation, and runtime validation of execution traces. Formal methods have been an important part of the development process – perhaps most importantly, formal specifications as oracles or monitors that provide the correct answers for many of AWS’s testing practices. Correctness testing and formal methods remain key areas of investment at AWS. In this talk, we will cover some of these tools and techniques that have had impact within AWS and then also open challenges that remains to be solved to further amplify the adoption of formal methods in practice.