\documentclass[aspectratio=169, lualatex, handout]{beamer} \makeatletter\def\input@path{{theme/}}\makeatother\usetheme{cipher} \title{Applied Cryptography} \author{Nadim Kobeissi} \institute{American University of Beirut} \instituteimage{images/aub_white.png} \date{\today} \coversubtitle{CMPS 297AD/396AI\\Fall 2025} \coverpartname{Part 2: Real-World Cryptography} \covertopicname{2.5: High-Assurance Cryptography} \coverwebsite{https://appliedcryptography.page} \begin{document} \begin{frame}[plain] \titlepage \end{frame} \section{Introduction} \begin{frame}{Securely implementing cryptography} \begin{itemize} \item Designing, implementing, and deploying cryptographic mechanisms is notoriously hard \item Regular discoveries of: \begin{itemize} \item High-profile design flaws \item Devastating implementation bugs \item Side-channel vulnerabilities \end{itemize} \item Even in \textbf{widely deployed} mechanisms! \end{itemize} \end{frame} \begin{frame}{Three levels of complexity} \begin{center} \Large \begin{enumerate} \item \textbf{Design Level} \item \textbf{Implementation Level} \item \textbf{Deployment Level} \end{enumerate} \vspace{1em} \normalsize Each level is highly involved and fraught with pitfalls \end{center} \end{frame} \begin{frame}{Design level challenges} \begin{itemize} \item Must achieve specific security goals \item Against well-defined classes of attackers \item Requires composing sophisticated building blocks: \begin{itemize} \item Abstract constructions \rightarrow\ Primitives \item Primitives \rightarrow\ Protocols \item Protocols \rightarrow\ Systems \end{itemize} \end{itemize} \end{frame} \begin{frame}{Implementation level challenges} \begin{itemize} \item High-level designs need concrete functional details: \begin{itemize} \item Data formats \item Session state \item Programming interfaces \end{itemize} \item Must optimize for: \begin{itemize} \item Interoperability \item Performance \end{itemize} \end{itemize} \end{frame} \begin{frame}{Deployment level challenges} \begin{itemize} \item Must account for low-level threats absent at design level \item Primary concern: Side-channel attacks \item Implementations must protect against various leakage channels \item Ad-hoc constant-time coding recipes are: \begin{itemize} \item Tricky to implement \item May not cover all leakage channels \end{itemize} \end{itemize} \end{frame} \begin{frame}{Vast attack surface} \begin{center} \Large Attackers can: \vspace{1em} \end{center} \begin{itemize} \item Break high-level designs \item Exploit implementation bugs \item Recover secrets via side-channels \item \textbf{Any combination of the above!} \end{itemize} \end{frame} \begin{frame}{Current methods fall short} \begin{itemize} \item \textbf{Pen-and-paper proofs}: \begin{itemize} \item Consider only pared-down ``cores'' \item Still highly complex and error-prone \end{itemize} \item \textbf{Aggressive optimization}: \begin{itemize} \item Increases risk of bugs \item Difficult to catch by testing or auditing \end{itemize} \item \textbf{Current modus operandi}: Select few experts with rudimentary tools \end{itemize} \end{frame} \begin{frame}{The problem} \begin{center} \Large The current approach \textbf{cannot keep pace} with the rate of innovation and development in cryptography \vspace{2em} \normalsize We need a better solution... \end{center} \end{frame} \begin{frame}{Missing: Real-world software complexity} \begin{itemize} \item Pen-and-paper proofs consider \textbf{isolated algorithms} \item Real deployments involve massive software stacks: \begin{itemize} \item Operating system layers \item Network protocol implementations \item Library dependencies \item Hardware abstraction layers \end{itemize} \item Each layer introduces: \begin{itemize} \item New attack surfaces \item Integration complexities \item Performance constraints \item Unexpected interactions \end{itemize} \item \textbf{Result}: Security proofs may not hold in practice! \end{itemize} \end{frame} \begin{frame}{Enter: Computer-Aided Cryptography (CAC)} \begin{itemize} \item Active area of research addressing these challenges \item Encompasses \textbf{formal, machine-checkable} approaches to: \begin{itemize} \item Designing cryptography \item Analyzing cryptography \item Implementing cryptography \end{itemize} \item Different tools address different parts of the problem space \end{itemize} \end{frame} \begin{frame}{CAC at different levels} \begin{itemize} \item \textbf{Design level}: Tools manage complexity of security proofs \begin{itemize} \item Can reveal subtle flaws \item May discover unknown attacks \end{itemize} \item \textbf{Implementation level}: Guarantee correct behavior \begin{itemize} \item Even for highly optimized code \item On all possible inputs \end{itemize} \item \textbf{Deployment level}: Check side-channel protections \end{itemize} \end{frame} \begin{frame}{Combining the tools} \begin{center} \Large Individual tools may only address \textit{part} of the problem \vspace{1em} But when \textbf{combined}, they provide a \textbf{high degree of assurance} \end{center} \end{frame} \begin{frame}{Success stories: standards} \begin{itemize} \item Computer-aided security analyses were influential in \textbf{TLS 1.3} standardization \item Multiple formal verification efforts contributed \item Helped identify and fix potential vulnerabilities before deployment \end{itemize} \end{frame} \begin{frame}{Success stories: real-world deployment} \begin{itemize} \item \textbf{\haclstar library}: Integrated into Mozilla Firefox's NSS \item \textbf{Fiat Cryptography}: Elliptic curve code in Google's BoringSSL \item \textbf{EverCrypt}: Routines used in Linux kernel's Zinc crypto library \end{itemize} \begin{center} \textbf{Formally verified code at Internet scale!} \end{center} \end{frame} \begin{frame}{Growing enthusiasm} \begin{itemize} \item Rapid emergence of a dynamic community: \begin{itemize} \item Theoretical cryptographers \item Applied cryptographers \item Cryptography engineers \item Formal methods practitioners \end{itemize} \item Goal: Achieve broader adoption of CAC \item Blending ideas from many fields \end{itemize} \end{frame} \begin{frame}{Risks and challenges} \begin{itemize} \item CAC risks becoming a \textbf{victim of its own success} \item \textbf{Trust can be undermined by}: \begin{itemize} \item Difficulty understanding guarantees \item Fine-print caveats of CAC artifacts \end{itemize} \item Field is increasingly: \begin{itemize} \item Broad \item Complex \item Rapidly evolving \end{itemize} \end{itemize} \end{frame} \begin{frame}{Pressing challenges ahead} \begin{itemize} \item \textbf{Post-quantum transition}: Expected transition to post-quantum cryptography \item \textbf{Scaling challenges}: Moving from lower-level primitives to whole cryptographic systems \item No one has complete understanding of every facet \end{itemize} \end{frame} \section{Design-Level Security} \begin{frame}{Two flavors of design-level security} \begin{itemize} \item Developed over years in \textbf{two separate communities}: \vspace{0.5em} \item \textbf{Symbolic Security} \begin{itemize} \item Formal methods community \item Abstract model of cryptography \end{itemize} \vspace{0.5em} \item \textbf{Computational Security} \begin{itemize} \item Cryptography community \item Concrete algorithms and probabilities \end{itemize} \end{itemize} \begin{center} \textit{Two complementary strands of work} \end{center} \end{frame} \begin{frame}{Symbolic model: Cryptography as algebra} \begin{center} \Large Treats cryptography as \textbf{perfect black boxes} \end{center} \vspace{1em} \begin{itemize} \item Messages are abstract \textbf{symbols}, not bits \item Encryption is a symbolic function \item Can only decrypt with \textbf{exact} key \item No partial information leakage \end{itemize} \vspace{0.5em} \textbf{Think of it like:} \begin{itemize} \item A locked box that's either fully open or fully closed \item No way to peek inside without the key \item Adversary can only manipulate whole messages \end{itemize} \end{frame} \begin{frame}{Computational model: Cryptography as algorithms} \begin{center} \Large Models real cryptography with \textbf{concrete algorithms} \end{center} \vspace{1em} \begin{itemize} \item Messages are \textbf{bitstrings} of specific length \item Encryption is a probabilistic algorithm \item Security holds with \textbf{high probability} \item Adversaries have \textbf{bounded computational power} \end{itemize} \vspace{0.5em} \textbf{Think of it like:} \begin{itemize} \item A safe that takes time to crack \item Harder safes take more time \item Given enough time, anything can be broken \item We just ensure it takes \textit{too long} to be practical \end{itemize} \end{frame} \begin{frame}{Symbolic vs. Computational: Key differences} \begin{center} \begin{tabular}{|l|l|l|} \hline \textbf{Aspect} & \textbf{Symbolic} & \textbf{Computational} \\ \hline Messages & Abstract terms & Bitstrings \\ \hline Adversary & Rule-based & Probabilistic algorithm \\ \hline Security & All-or-nothing & Probabilistic bounds \\ \hline Analysis & Often decidable & Generally undecidable \\ \hline Guarantees & ``Cannot break'' & ``Hard to break'' \\ \hline \end{tabular} \end{center} \vspace{1em} \textbf{When to use which?} \begin{itemize} \item \textbf{Symbolic}: Quick protocol flaw detection, automated analysis \item \textbf{Computational}: Concrete security guarantees, cryptographic proofs \item \textbf{Both}: Different insights, complementary verification \end{itemize} \end{frame} \begin{frame}{How protocol models end up, intuitively} \bigimagewithcaption{cas_comparison.png}{Source: Cas Cremers} \end{frame} \begin{frame}{Why is design-level security important?} \begin{itemize} \item Mathematical arguments are the \textbf{only way} to demonstrate security against entire classes of attacks \item Security proofs are \textbf{necessary} for any new standard \item Applies at all levels: \begin{itemize} \item Primitives \item Protocols \item Systems \end{itemize} \item Critical to understand: \begin{itemize} \item Security notions \item Adversarial models \item Deployment environments \end{itemize} \end{itemize} \end{frame} \begin{frame}{How can design-level security fail?} \begin{center} \Large Pen-and-paper arguments are \textbf{alarmingly fragile} \end{center} \vspace{1em} Two main reasons: \begin{enumerate} \item \textbf{Erroneous arguments} \item \textbf{Inappropriate modeling} \end{enumerate} \end{frame} \begin{frame}{Failure mode 1: Erroneous arguments} \begin{itemize} \item Writing security arguments is: \begin{itemize} \item Tedious \item Error-prone \item Difficult even for experts \end{itemize} \item Primarily done on pen-and-paper \item Errors are difficult to catch \item Can go unnoticed for \textbf{years} \end{itemize} \end{frame} \begin{frame}{Failure mode 2: Inappropriate modeling} \begin{itemize} \item Even correct arguments can miss attacks outside the model \item Known and common pitfall \item To make analysis tractable: \begin{itemize} \item Models are heavily simplified \item Focus on ``cryptographic core'' \item Elide many details \end{itemize} \item \textbf{Result}: Attacks often found outside this core \end{itemize} \end{frame} \begin{frame}{Current approaches (without CAC)} \textbf{To minimize erroneous arguments:} \begin{itemize} \item Methodological frameworks developed: \begin{itemize} \item Code-based game playing \item Universal composability \end{itemize} \item Goal: Decompose into simpler arguments \item Still complex and error-prone! \end{itemize} \vspace{0.5em} \textbf{To reduce inappropriate modeling:} \begin{itemize} \item ``Real-world provable security'' approach \item More accurate models \item But: Added realism \rightarrow\ Greater complexity \end{itemize} \end{frame} \begin{frame}{How CAC helps at the design level} \begin{itemize} \item \textbf{Detect flaws} in cryptographic designs \item \textbf{Manage complexity} of security proofs \item Crystallize benefits of: \begin{itemize} \item On-paper methodologies \item Real-world provable security \end{itemize} \item Enable trustworthy analyses for complex designs \item Go beyond reach of pen-and-paper analysis \end{itemize} \end{frame} \begin{frame}{The fine print} \begin{center} \Large Computer-aided security proofs are only as good as the statements being proven \end{center} \vspace{1em} \begin{itemize} \item Understanding these statements can be \textbf{challenging} \item Most proofs rely on \textbf{implicit assumptions} \item Reconstructing top-level statements is hard, even for experts \item Tools may have bugs (like any software) \end{itemize} \end{frame} \begin{frame}{Symbolic security: The basics} \begin{itemize} \item Messages represented \textbf{symbolically} as terms \item Terms are \textbf{atomic data} \begin{itemize} \item Cannot be split into bitstrings \end{itemize} \item Cryptographic primitives = \textbf{black-box functions} \item Related by \textbf{equational theories} \end{itemize} \vspace{1em} \begin{center} Abstract model for representing and analyzing protocols \end{center} \end{frame} \begin{frame}{Symbolic security: Example} \textbf{Symmetric encryption modeled by:} \begin{itemize} \item Functions: \texttt{Enc} and \texttt{Dec} \item Equational theory: \end{itemize} \begin{center} \Large \texttt{Dec(Enc(m,k),k) = m} \end{center} \begin{itemize} \item Decrypting ciphertext \texttt{Enc(m,k)} with key \texttt{k} recovers plaintext \texttt{m} \item Adversary can only use specified primitives and equations \item Can decrypt only if it has the \textbf{entire} secret key \end{itemize} \end{frame} \begin{frame}{Symbolic security properties} Two main flavors: \vspace{1em} \begin{enumerate} \item \textbf{Trace properties} \begin{itemize} \item Bad events never occur on any execution trace \item Example: Secret data never in adversarial knowledge \end{itemize} \vspace{0.5em} \item \textbf{Equivalence properties} \begin{itemize} \item Adversary cannot distinguish between two protocols \item Example: Cannot differentiate real secret from random value \end{itemize} \end{enumerate} \vspace{1em} \begin{center} \textit{Equivalence properties cannot be naturally expressed as trace properties} \end{center} \end{frame} \begin{frame}{Computational security: The basics} \begin{itemize} \item Messages are \textbf{bitstrings} \item Primitives are \textbf{probabilistic algorithms} \item Adversaries are \textbf{probabilistic Turing machines} \item Security properties are \textbf{probabilistic} \end{itemize} \vspace{1em} Example: Symmetric encryption = (Gen, Enc, Dec) \begin{itemize} \item Gen: Probabilistic key generation \item Enc/Dec: Encryption/decryption algorithms \item Correctness: Dec(Enc(m,k),k) = m for all valid k, m \end{itemize} \end{frame} \begin{frame}{Computational security properties} Characterized along two axes: \vspace{1em} \begin{center} \begin{tabular}{|c|c|} \hline \textbf{Type} & \textbf{Quantification} \\ \hline Game-based & Concrete \\ Simulation-based & Asymptotic \\ \hline \end{tabular} \end{center} \vspace{1em} \begin{itemize} \item CAC tools primarily focus on \textbf{game-based, concrete security} \item Simulation-based proofs: More complex, support composition \item Concrete security implies asymptotic security \end{itemize} \end{frame} \begin{frame}{Game-based security} \begin{itemize} \item Probabilistic experiment: ``game'' between challenger and adversary \item Explicit goal condition for adversary \item Security statement: \begin{center} \textit{``For all adversaries, probability of achieving goal \leq\ threshold''} \end{center} \item Core methodology: \textbf{Game hopping} \begin{enumerate} \item Start with original game \item Transform step-by-step \item Reach game where success probability is known \item Bound probability increases at each step \item Similar to what we saw in Part 1 of this course! \end{enumerate} \end{itemize} \end{frame} \begin{frame}{Simulation-based security} Two probabilistic experiments: \vspace{0.5em} \begin{enumerate} \item \textbf{Real game}: Runs the actual scheme \item \textbf{Ideal game}: Runs idealized scheme with trusted third-party \end{enumerate} \vspace{0.5em} Security statement: \begin{center} \textit{``For all real adversaries, exists simulator that translates attacks''} \end{center} \vspace{0.5em} \begin{itemize} \item Ideal functionality secure by definition \item Therefore real scheme must be secure \item More complex than game-based proofs \item But: Support composition theorems! \end{itemize} \end{frame} \begin{frame}{Concrete vs. Asymptotic security} \textbf{Concrete security:} \begin{itemize} \item Scheme is $(t,\epsilon)$-secure \item Every adversary running time \leq\ $t$ succeeds with probability \leq\ $\epsilon$ \item Specific numerical bounds \end{itemize} \vspace{0.5em} \textbf{Asymptotic security:} \begin{itemize} \item Running time and success probability = functions of security parameter \item Scheme secure if PPT adversaries succeed with negligible probability \item Prevailing paradigm in cryptography \end{itemize} \vspace{0.5em} \begin{center} \textit{Proving concrete security \rightarrow\ Asymptotic security follows} \end{center} \end{frame} \begin{frame}{Symbolic analysis tools overview} \bigimagewithcaption{verif_symbolic.png}{Source: Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao and Bryan Parno, SoK: Computer-Aided Cryptography, IEEE Symposium on Security and Privacy, 2021.} \end{frame} \begin{frame}{Key features of symbolic analysis tools} \begin{center} \Large What distinguishes different symbolic analysis tools? \end{center} \vspace{1em} \begin{itemize} \item Different tools have different capabilities \item Understanding these helps choose the right tool \item We'll explore the key dimensions of comparison \end{itemize} \end{frame} \begin{frame}{Unbounded sessions: The challenge} \begin{itemize} \item Real protocols run \textbf{many concurrent sessions} \item Some protocols are secure for $N$ sessions... \item ...but become \textbf{insecure} with $N+1$ sessions! \end{itemize} \vspace{1em} \begin{center} \Large How many sessions should we analyze? \end{center} \end{frame} \begin{frame}{Bounded vs. Unbounded analysis} \textbf{Bounded tools:} \begin{itemize} \item Explicitly limit analyzed sessions \item Cannot detect attacks beyond cut-off \item Simpler but incomplete \end{itemize} \vspace{0.5em} \textbf{Unbounded tools:} \begin{itemize} \item Analyze arbitrary number of sessions \item Can prove \textbf{absence of attacks} in the model \item More complex, may not terminate (undecidable) \end{itemize} \end{frame} \begin{frame}{Performance paradox} \begin{center} \Large Modern unbounded tools often \textbf{outperform} bounded tools \vspace{0.5em} \normalsize Even for small numbers of sessions! \end{center} \vspace{1em} Why? \begin{itemize} \item Bounded tools naively enumerate options \item Growth is \textbf{exponential} in session count \item Unbounded tools use clever algorithms \item When they terminate, analysis is session-independent \end{itemize} \end{frame} \begin{frame}{Trace properties} \begin{itemize} \item Verify that \textbf{bad things never happen} \item Examples: \begin{itemize} \item Secret keys never leaked \item Authentication always succeeds \item Adversary never learns password \end{itemize} \item Most basic form of security property \item Supported by nearly all tools \end{itemize} \end{frame} \begin{frame}{Equivalence properties: Beyond traces} \begin{itemize} \item Some properties \textbf{cannot} be expressed as traces \item Example: ``Adversary cannot tell if vote was for Alice or Bob'' \item Requires comparing protocol executions \item Three main notions: \begin{enumerate} \item Trace equivalence \item Open bisimilarity \item Diff-equivalence \end{enumerate} \end{itemize} \begin{center} \textit{Each notion has different strengths and use cases} \end{center} \end{frame} \begin{frame}{Trace equivalence} \begin{itemize} \item \textbf{Weakest} equivalence notion (most expressive) \item For each trace in protocol A... \item ...exists corresponding trace in protocol B... \item ...with indistinguishable messages \end{itemize} \vspace{1em} \begin{center} \Large Most natural for privacy properties \end{center} \end{frame} \begin{frame}{Open bisimilarity} \begin{itemize} \item \textbf{Stronger} than trace equivalence \item Uses ``bi-traces'' to track adversary knowledge \item Each action in one protocol... \item ...can be simulated in the other \item While maintaining consistency \end{itemize} \vspace{1em} \begin{center} Often an intermediate step toward proving trace equivalence \end{center} \end{frame} \begin{frame}{Diff-equivalence} \begin{itemize} \item \textbf{Strongest} notion (most restrictive) \item Protocols must have \textbf{identical structure} \item Differ only in messages exchanged \item All tests succeed/fail identically in both \end{itemize} \vspace{1em} \begin{center} Preserves protocol structure during execution \end{center} \end{frame} \begin{frame}{Equational theories: Modeling cryptography} \begin{itemize} \item Cryptographic operations have algebraic properties \item Example: XOR satisfies $x \oplus x = 0$ \item More properties \rightarrow\ More potential attacks detected \end{itemize} \vspace{0.5em} \textbf{Three levels of support:} \begin{enumerate} \item Fixed/no theories \item User-defined (without AC axioms) \item User-defined with associative-commutative (AC) \end{enumerate} \vspace{0.5em} \begin{center} AC support enables modeling XOR, abelian groups, DH \end{center} \end{frame} \begin{frame}{Global mutable state} \begin{itemize} \item Real protocols often use: \begin{itemize} \item Shared databases \item Key servers \item Shared memory \end{itemize} \item Enables complex stateful attacks \item Example: Replay attacks on counters \item Not all tools support this \end{itemize} \vspace{1em} \begin{center} \Large Critical for analyzing real-world protocols \end{center} \end{frame} \begin{frame}{Link to implementation} \begin{center} \Large Can symbolic guarantees translate to real code? \end{center} \vspace{1em} \begin{itemize} \item Some tools extract/generate executable code \item Links abstract model to concrete implementation \item Bridges design and implementation levels \item Reduces gap between proof and practice \end{itemize} \end{frame} \begin{frame}{Abstractions: Trading precision for efficiency} \begin{itemize} \item Some tools use abstraction techniques \item Overestimate adversary capabilities \item Example: Compute superset of adversary knowledge \end{itemize} \vspace{0.5em} \textbf{Benefits:} \begin{itemize} \item More efficient analysis \item Fully automatic \item Workaround for undecidability \end{itemize} \textbf{Cost:} \begin{itemize} \item May find false attacks \item May return ``don't know'' \end{itemize} \end{frame} \begin{frame}{Interactive mode: Human in the loop} \begin{itemize} \item Push-button automation isn't always enough \item Tools may fail opaquely due to: \begin{itemize} \item Undecidability barriers \item Complex protocol structure \item Resource limits \end{itemize} \end{itemize} \vspace{0.5em} \textbf{Interactive modes allow:} \begin{itemize} \item Inspecting partial proofs \item Providing hints \item Guiding analysis past barriers \end{itemize} \vspace{0.5em} \begin{center} \textit{Trade automation for control} \end{center} \end{frame} \begin{frame}{Independent verifiability: Trust but verify} \begin{itemize} \item Symbolic tools implement \textbf{complex algorithms} \item May have bugs and return incorrect results \item Usually in the trusted computing base \end{itemize} \vspace{0.5em} \textbf{Some tools provide:} \begin{itemize} \item Machine-checkable proof scripts \item Explicit evidence of claims \item Can be verified independently \end{itemize} \vspace{0.5em} \begin{center} \textit{Examples: Scyther-proof (Isabelle), SPEC (evidence)} \end{center} \end{frame} \begin{frame}{Specification languages} How do you describe protocols to the tool? \vspace{0.5em} \begin{enumerate} \item \textbf{Domain-specific languages} \begin{itemize} \item Designed for security protocols \item Natural for cryptographers \end{itemize} \item \textbf{Process calculi} \begin{itemize} \item Formal concurrent processes \item Familiar to formal methods experts \end{itemize} \item \textbf{Multiset rewriting} \begin{itemize} \item Lower-level, more general \item Natural for state machines \end{itemize} \item \textbf{General programming languages} \begin{itemize} \item Most familiar to developers \end{itemize} \end{enumerate} \end{frame} \begin{frame}{Achievements: Real-world symbolic analysis} \begin{center} \Large From theory to practice: Symbolic tools tackle real protocols \end{center} \vspace{1em} \begin{itemize} \item Two tools stand out for real-world analysis: \begin{itemize} \item \textbf{ProVerif} \item \textbf{Tamarin} \end{itemize} \item Unprecedented combination of: \begin{itemize} \item Scalability \item Expressivity \end{itemize} \item Can handle complex systems and properties \end{itemize} \end{frame} \begin{frame}{Why ProVerif and Tamarin succeed} \begin{itemize} \item \textbf{Extensive documentation} \begin{itemize} \item Detailed tutorials \item Theory explanations \end{itemize} \item \textbf{Library of case studies} \begin{itemize} \item Learn from examples \item Reusable components \end{itemize} \item \textbf{Practical usability features} \begin{itemize} \item Professional packaging \item Tamarin: Graphical user interface \item ProVerif: Attack reconstruction in HTML \end{itemize} \end{itemize} \end{frame} \begin{frame}{ProVerif: Real-world success stories} \textbf{TLS 1.0} \begin{itemize} \item Verification time: Seconds to hours \item Depends on security property \end{itemize} \vspace{0.5em} \textbf{TLS 1.3} (part of my Ph.D. thesis!) \begin{itemize} \item Modern protocol standard \item Verification time: $\sim$1 hour \end{itemize} \vspace{0.5em} \textbf{Signal Protocol} (part of my Ph.D. thesis!) \begin{itemize} \item End-to-end encrypted messaging \item Verification time: Minutes to days \item Complex properties take longer \end{itemize} \end{frame} \begin{frame}{ProVerif: Noise protocol framework} \begin{itemize} \item Framework for building secure channels \item Verification time: Seconds to days \item Varies by specific protocol variant \item (Also part of my Ph.D. thesis!) \item Super accessible and informative demo: \url{https://noiseexplorer.com} \end{itemize} \vspace{0.5em} \begin{center} \Large Key insight: More Diffie-Hellman operations = longer analysis \end{center} \vspace{0.5em} \begin{itemize} \item DH operations particularly expensive to analyze \item Signal and Noise use many DH exchanges \item Explains wide time variations \end{itemize} \end{frame} \begin{frame}{Tamarin: Tackling massive protocols} \textbf{5G Authentication Key Exchange} \begin{itemize} \item Critical infrastructure protocol \item Verification time: $\sim$5 hours \end{itemize} \vspace{0.5em} \textbf{TLS 1.3} \begin{itemize} \item Complete analysis \item Verification time: $\sim$1 week \item Resource requirement: 100GB RAM! \end{itemize} \vspace{0.5em} \textbf{DNP3 SAv5} \begin{itemize} \item Power grid security protocol \item Verification time: Several minutes \end{itemize} \end{frame} \begin{frame}{Tamarin: Noise protocols} \begin{itemize} \item Same framework as ProVerif analyzed \item Verification time: Seconds to hours \item Depends on protocol complexity \end{itemize} \vspace{1em} \begin{center} \Large Tool comparisons are difficult! \end{center} \vspace{0.5em} \begin{itemize} \item Even on similar case studies \item Different modeling choices \item Different property formulations \item \textbf{Take performance numbers with a grain of salt!} \end{itemize} \end{frame} \begin{frame}{Challenge: Equivalence properties} \begin{center} \Large The frontier of symbolic analysis \end{center} \vspace{1em} \begin{itemize} \item Many security properties need equivalence \item Examples: \begin{itemize} \item Vote privacy in e-voting \item Unlinkability in anonymity protocols \item Indistinguishability of messages \end{itemize} \item But they're \textbf{inherently harder} than trace properties \end{itemize} \end{frame} \begin{frame}{Why equivalence is hard} \textbf{Trace properties:} \begin{itemize} \item Analyze single execution traces \item ``Does bad event X happen?'' \item Local reasoning \end{itemize} \vspace{0.5em} \textbf{Equivalence properties:} \begin{itemize} \item Analyze \textbf{relations between traces} \item ``Can adversary distinguish scenarios?'' \item Global reasoning across executions \end{itemize} \vspace{1em} \begin{center} Tool support is substantially less mature \end{center} \end{frame} \begin{frame}{Two approaches to equivalence} \begin{center} \Large For full automation, must make a choice: \end{center} \vspace{1em} \begin{enumerate} \item \textbf{Bounded analysis} \begin{itemize} \item Limit number of sessions \item More expressive properties \item But incomplete \end{itemize} \vspace{0.5em} \item \textbf{Unbounded with diff-equivalence} \begin{itemize} \item Analyze infinite sessions \item Very restrictive notion \item Cannot handle many desired properties \end{itemize} \end{enumerate} \end{frame} \begin{frame}{Progress in bounded equivalence} \textbf{Recent developments include:} \vspace{0.5em} \begin{itemize} \item \textbf{More equational theories} \begin{itemize} \item AKISS, DEEPSEC \end{itemize} \item \textbf{Protocols with else branches} \begin{itemize} \item APTE, AKISS, DEEPSEC \end{itemize} \item \textbf{Non-deterministic protocols} \begin{itemize} \item Actions not entirely determined by inputs \item APTE, DEEPSEC \end{itemize} \end{itemize} \end{frame} \begin{frame}{Performance improvements} \textbf{Partial order reduction} \begin{itemize} \item Implemented in: APTE, AKISS, DEEPSEC \item Avoid exploring equivalent interleavings \item Significant speedups \end{itemize} \vspace{0.5em} \textbf{Graph planning} \begin{itemize} \item Implemented in: SAT-Equiv \item Convert to planning problem \item Leverage SAT solver efficiency \end{itemize} \vspace{1em} \begin{center} Making bounded analysis more practical \end{center} \end{frame} \begin{frame}{The unbounded equivalence challenge} \begin{itemize} \item \textbf{Diff-equivalence} remains the only fully automated approach \item First introduced in ProVerif \item Later adopted by: \begin{itemize} \item Maude-NPA \item Tamarin \end{itemize} \end{itemize} \vspace{1em} \begin{center} \Large But it's too restrictive! \end{center} \vspace{0.5em} \begin{itemize} \item Trace equivalence is most natural for privacy \item Many properties cannot be expressed as diff-equivalence \item Verifying general equivalence for unbounded sessions remains an open challenge \end{itemize} \end{frame} \begin{frame}{Computational analysis tools overview} \bigimagewithcaption{verif_computational.png}{Source: Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao and Bryan Parno, SoK: Computer-Aided Cryptography, IEEE Symposium on Security and Privacy, 2021.} \end{frame} \begin{frame}{Computational analysis tools: Overview} \begin{itemize} \item Wide variety of tools for computational security \item Different strengths and focuses \item Understanding their capabilities helps choose the right tool \end{itemize} \vspace{1em} \begin{center} \Large Let's explore what distinguishes these tools \end{center} \end{frame} \begin{frame}{Reasoning focus: Automation vs. Expressivity} \begin{center} \Large Every tool makes a fundamental tradeoff \end{center} \vspace{1em} \textbf{Automation focus:} \begin{itemize} \item Produce proofs automatically \item Light interaction required \item Limited to certain proof patterns \end{itemize} \vspace{0.5em} \textbf{Expressivity focus:} \begin{itemize} \item Express arbitrary arguments \item Handle complex reasoning \item More manual effort required \end{itemize} \end{frame} \begin{frame}{Automated proof-finding} \begin{itemize} \item Some automation-focused tools go further \item Can find proofs \textbf{completely automatically} \item But only in restricted settings: \end{itemize} \vspace{0.5em} \textbf{Examples:} \begin{itemize} \item \textbf{AutoG\&P}: Pairing-based schemes \item \textbf{CryptoVerif}: Key exchange with built-in transformations \item \textbf{ZooCrypt}: Padding-based public key encryption \end{itemize} \vspace{0.5em} \begin{center} Push-button verification for specific domains \end{center} \end{frame} \begin{frame}{Composition support} \begin{center} \Large Can we break down complex systems? \end{center} \vspace{1em} \begin{itemize} \item Real cryptographic systems are built from components \item Need to reason about each piece separately \item Then combine the results \end{itemize} \vspace{0.5em} \textbf{Compositional reasoning:} \begin{itemize} \item Essential for scalability \item Not all tools support it \item Key differentiator \end{itemize} \end{frame} \begin{frame}{Concrete security bounds} \begin{itemize} \item Can the tool prove \textbf{specific numerical bounds}? \item Not just ``secure'' but ``how secure'' \end{itemize} \vspace{0.5em} \textbf{Three levels of support:} \begin{enumerate} \item \textbf{No support}: Only asymptotic security \item \textbf{Probability only}: Bounds on success probability \item \textbf{Full support}: Both probability and time bounds \end{enumerate} \vspace{0.5em} \begin{center} Concrete bounds crucial for real-world deployment \end{center} \end{frame} \begin{frame}{Linking to implementation} \begin{center} \Large Can computational guarantees reach real code? \end{center} \vspace{1em} \begin{itemize} \item Some tools can extract/generate executable code \item Links abstract specifications to implementations \item Ensures proved properties hold in practice \end{itemize} \vspace{0.5em} \textbf{Without this link:} \begin{itemize} \item Gap between proof and code \item Implementation may diverge from spec \item Security guarantees may not transfer \end{itemize} \end{frame} \begin{frame}{Trusted computing base} \begin{itemize} \item What must we trust for the proof to be valid? \item Critical consideration for high-assurance \end{itemize} \vspace{0.5em} \textbf{Three common TCB levels:} \begin{enumerate} \item \textbf{Theorem prover}: Coq, Isabelle (minimal TCB) \item \textbf{Tool implementation}: Custom logic implementation \item \textbf{SMT solvers}: Z3 and similar (for automation) \end{enumerate} \vspace{0.5em} \begin{center} Smaller TCB = Higher confidence \end{center} \end{frame} \begin{frame}{Specification languages} \textbf{How do you write your cryptographic code?} \vspace{0.5em} \begin{itemize} \item \textbf{Functional core}: Express operation semantics \begin{itemize} \item Supported by all tools \item Natural for algorithms \end{itemize} \item \textbf{Imperative language}: Write security games \begin{itemize} \item Familiar to programmers \item Direct game representation \end{itemize} \item \textbf{Process calculus}: Protocol communication \begin{itemize} \item Natural for message exchange \item Well-suited for protocols \end{itemize} \end{itemize} \end{frame} \begin{frame}{Achievements: Real-world impact} \begin{center} \Large Computational tools have analyzed major cryptographic systems \end{center} \vspace{1em} \textbf{CryptoVerif successes:} \begin{itemize} \item TLS 1.3 (part of my Ph.D. thesis!) \item Signal Protocol (part of my Ph.D. thesis!) \item WireGuard VPN \end{itemize} \vspace{0.5em} \textbf{EasyCrypt successes:} \begin{itemize} \item AWS Key Management System \item SHA-3 standard \end{itemize} \end{frame} \begin{frame}{More achievements} \textbf{F7 milestone:} \begin{itemize} \item miTLS: Reference implementation of TLS 1.2 \item Verified computational security at code level \item Pioneering work in verified implementations \end{itemize} \vspace{0.5em} \textbf{\fstar contribution:} \begin{itemize} \item Implemented and verified TLS 1.3 record layer \item Full protocol analysis beyond cryptographic core \item Discovered new attacks on real protocols \end{itemize} \end{frame} \begin{frame}{CryptoVerif: The protocol analyzer} \begin{center} \Large Best for highly automated protocol analysis \end{center} \vspace{1em} \textbf{Key strengths:} \begin{itemize} \item Both proof-finding and proof-checking \item Excellent for key exchange protocols \item Automatic or light-guided proof discovery \end{itemize} \vspace{0.5em} \textbf{Why it works well:} \begin{itemize} \item Applied π-calculus input language \item Perfect for sequential message exchange \item Carefully crafted security assumptions \item Helps automated proof discovery \end{itemize} \end{frame} \begin{frame}{CryptoVerif: Handling complexity} \begin{itemize} \item Automation crucial for large games \item Handles many different cases \item Common in protocol proofs \end{itemize} \vspace{1em} \begin{center} \Large When protocols get complex, automation saves the day \end{center} \vspace{1em} \begin{itemize} \item Manual proof management becomes infeasible \item Tool tracks all cases systematically \item Finds proof steps human might miss \end{itemize} \end{frame} \begin{frame}{\fstar: Beyond the cryptographic core} \begin{center} \Large Best for analyzing full protocols and systems \end{center} \vspace{1em} \begin{itemize} \item General-purpose verification language \item Goes beyond just cryptographic primitives \item Analyzes complete protocol implementations \end{itemize} \vspace{0.5em} \textbf{Key insight:} \begin{itemize} \item Critical issues arise in \textbf{detailed descriptions} \item Not just in cryptographic cores \item Need to verify the full system \end{itemize} \end{frame} \begin{frame}{\fstar: Types are proofs!} \begin{center} \Large The magic of dependent types \end{center} \vspace{1em} \begin{itemize} \item In \fstar, types can \textbf{depend on values} \item A well-typed program is a \textbf{proof of its specification} \item Type checking = Proof checking! \end{itemize} \vspace{0.5em} \textbf{Example: Array bounds} \begin{itemize} \item Type: \texttt{array int \{n:nat | n < len\}} \item Accessing with this type \textbf{proves} no buffer overflow \item Compiler rejects code that might overflow \end{itemize} \vspace{0.5em} \begin{center} \textit{Your program literally cannot go wrong if it type-checks!} \end{center} \end{frame} \begin{frame}{\fstar: Z3 does the heavy lifting!} \begin{center} \Large SMT solving during type checking! \end{center} \vspace{0.5em} \begin{itemize} \item \fstar doesn't just check types, it \textbf{proves theorems} \item Every type check = Verification condition sent to Z3 \item Z3 proves your code satisfies its specification \item If Z3 says ``yes'', your code is mathematically correct! \end{itemize} \vspace{0.5em} \textbf{Example: Point on elliptic curve} \begin{itemize} \item Type: \texttt{point : \{(x,y) : int * int | y*y = x*x*x + a*x + b\}} \item This type \textbf{only} accepts valid curve points! \item Try to create invalid point? \textbf{Type error!} \item Function accepting this type? \textbf{Guaranteed} valid input! \end{itemize} \vspace{0.1em} \begin{center} \textit{Your elliptic curve code literally cannot process invalid points} \end{center} \end{frame} \begin{frame}{\fstar: the approach} \textbf{How \fstar handles computational proofs:} \begin{enumerate} \item Start with detailed protocol description \item Transform into ideal program \item Use ideal functionalities for crypto primitives \item Validate transformation manually \item Verify final program automatically \end{enumerate} \vspace{0.5em} \textbf{Success stories:} \begin{itemize} \item Discovered new attacks on TLS \item Verified concrete designs and implementations \item Bridges theory-practice gap \end{itemize} \end{frame} \begin{frame}{hax: From Rust to verified models} \begin{center} \Large Extract verification models directly from Rust code \end{center} \vspace{1em} \begin{itemize} \item Toolchain for verifying cryptographic implementations in Rust \item Two verification flavors: \begin{itemize} \item \textbf{Correctness}: Extract to \fstar (e.g., ML-KEM/Kyber) \item \textbf{Security}: Extract to ProVerif protocol models \end{itemize} \item Revolutionary approach: One codebase, multiple verification targets \end{itemize} \vspace{0.5em} \begin{center} \textit{No more manual modeling – extract from real implementations!} \end{center} \end{frame} \begin{frame}{hax-ProVerif: Protocol analysis from code} \begin{center} \Large Traditional way: Model protocols by hand \vspace{0.5em} \textbf{hax way: Extract models from implementation} \end{center} \vspace{1em} \textbf{How it works:} \begin{itemize} \item Rust structs/enums \rightarrow\ ProVerif types with constructors \item Rust functions \rightarrow\ ProVerif process macros \item Run: \texttt{cargo hax into proverif} \end{itemize} \vspace{0.5em} \textbf{Success story: TLS 1.3} \begin{itemize} \item Extracted model from Bertie (minimal TLS 1.3 implementation) \item 900 lines Rust \rightarrow\ 4500 lines ProVerif model \item Proved server authentication and session key confidentiality \end{itemize} \end{frame} \begin{frame}{hax playground: Verification in your browser!} \begin{center} \Large Try hax without installing anything! \vspace{0.5em} \url{https://hax-playground.cryspen.com} \end{center} \vspace{1em} \textbf{What you can do:} \begin{itemize} \item Run hax on Rust code \rightarrow\ See \fstar, Coq, or ProVerif output \item Run \fstar typechecker to verify generated code \item Inspect Rust ASTs (THIR/MIR) interactively \item Share snippets with others \item Submit issues directly to GitHub \end{itemize} \vspace{0.5em} \begin{center} \textit{First glimpse of Cryspen's verification workbench!} \end{center} \end{frame} \begin{frame}{hax playground: Prove Rust code online} \textbf{Example: Proving overflow safety} \begin{itemize} \item Write a simple \texttt{incr} function for \texttt{u8} \item \fstar complains: might overflow at 255! \item Add precondition with \texttt{requires} clause \item Prove function never panics \mycheckmark \end{itemize} \vspace{0.5em} \textbf{Advanced features:} \begin{itemize} \item \textbf{Right-click any code}: Explore enriched THIR/MIR ASTs \item \textbf{Share button}: Create persistent links with exact hax commit \item \textbf{One-click export}: Open in Rust playground or file GitHub issue \end{itemize} \vspace{0.5em} \begin{center} \Large Making hax accessible to everyone! \vspace{0.5em} \normalsize \textit{From newcomers to verification experts} \end{center} \end{frame} \section{Functional Correctness and Efficiency} \begin{frame}{Building correct and fast cryptographic code} \begin{center} \Large Design-level security is not enough! \vspace{1em} We need implementations that are: \begin{itemize} \item \textbf{Functionally correct} \item \textbf{Performant} \item \textbf{Memory safe} \end{itemize} \end{center} \end{frame} \begin{frame}{The implementation challenge} \begin{itemize} \item Even perfect designs can fail in implementation \item Must accurately translate proven designs to code \item \textbf{Functional correctness}: Same input/output behavior as specification \end{itemize} \vspace{1em} \begin{center} \Large But that's not enough... \end{center} \end{frame} \begin{frame}{The efficiency imperative} \begin{center} \Large Cryptography is on the critical path! \end{center} \vspace{1em} \begin{itemize} \item Every TLS packet \item Every encrypted file operation \item Every secure communication \end{itemize} \vspace{0.5em} \begin{center} \textit{Even a few extra clock cycles matter at scale} \end{center} \end{frame} \begin{frame}{The fundamental tension} \begin{center} \Large Easy path: Use reference implementation \vspace{0.5em} \normalsize \mycheckmark Straightforward correctness \\ \times Terrible performance \end{center} \vspace{1em} \begin{center} \Large Hard path: Optimize aggressively \vspace{0.5em} \normalsize \mycheckmark Blazing fast \\ \times Correctness becomes a nightmare \end{center} \end{frame} \begin{frame}{How far will developers go for speed?} \textbf{OpenSSL's approach:} \begin{enumerate} \item Write Perl code... \item ...that generates strings of text... \item ...that other Perl scripts interpret... \item ...to produce C preprocessor input... \item ...which generates platform-specific assembly! \end{enumerate} \vspace{1em} \begin{center} \Large This is one of the \textit{fastest} crypto libraries \vspace{0.5em} \normalsize But imagine verifying \textit{that} \end{center} \end{frame} \begin{frame}{The language dilemma} \begin{center} \Large High-level languages? Too slow. \end{center} \vspace{1em} \textbf{Reality of high-performance crypto:} \begin{itemize} \item C for ``portable'' performance \item Assembly for ultimate speed \item Platform-specific optimizations everywhere \end{itemize} \vspace{0.5em} \textbf{The cost:} \begin{itemize} \item Memory safety becomes critical concern \item Bugs can leak secrets (remember Heartbleed?) \item Verification becomes much harder \end{itemize} \end{frame} \begin{frame}{Beyond compiler optimizations} \begin{center} \Large Why not let compilers handle optimization? \end{center} \vspace{1em} \textbf{The harsh truth:} \begin{itemize} \item Best-in-class crypto needs manual optimization \item Compilers can't match expert assembly \item Platform-specific tricks matter \item Compilers can be problematic (more on this later...) \end{itemize} \vspace{0.5em} \begin{center} \textit{These optimizations are painstakingly repeated for each architecture} \end{center} \end{frame} \begin{frame}{Current approach: Trust the experts} \begin{center} \Large A handful of experts write all high-speed crypto \end{center} \vspace{1em} \textbf{But even experts make mistakes:} \begin{itemize} \item OpenSSL AES-GCM optimization \rightarrow\ message forgeries \item OpenSSL arithmetic bug \rightarrow\ full key recovery \item 24 vulnerabilities in libcrypto (2016-2019) \end{itemize} \vspace{0.5em} \begin{center} Despite widespread usage and scrutiny! \end{center} \end{frame} \begin{frame}{Traditional quality assurance} \textbf{Current solutions:} \vspace{0.5em} \begin{enumerate} \item \textbf{Auditing} (my full-time job when not teaching this course!) \begin{itemize} \item Expensive in time and expertise \item Can miss subtle bugs \item Not scalable \end{itemize} \vspace{0.5em} \item \textbf{Testing} \begin{itemize} \item Cannot cover all inputs \item Cryptographic input space is huge \item Edge cases matter \end{itemize} \end{enumerate} \vspace{1em} \begin{center} \Large Clearly inadequate for high-assurance crypto! \end{center} \end{frame} \begin{frame}{Enter program verification} \begin{center} \Large Cryptographic code is an \textbf{ideal target} for verification \end{center} \vspace{1em} \textbf{Why?} \begin{itemize} \item Critically important to get right \item Relatively small codebase \item Well-defined specifications \item Clear correctness criteria \end{itemize} \vspace{0.5em} \begin{center} \textit{Heavy-weight formal methods are justified here} \end{center} \end{frame} \begin{frame}{The promise of verification} \begin{center} \Large We can have our cake and eat it too! \end{center} \vspace{1em} \textbf{Program verification enables:} \begin{itemize} \item Complex optimizations \item Guaranteed correctness \item Memory safety proofs \item Platform-specific code \end{itemize} \vspace{0.5em} \begin{center} All within reach of existing tools and reasonable effort \end{center} \end{frame} \begin{frame}{The fine print: Implicit assumptions} \begin{center} \Large What are we \textit{actually} trusting? \end{center} \vspace{1em} \textbf{Common implicit assumptions:} \begin{itemize} \item Hardware behaves as modeled \item Verification done on ``friendly'' code representation \item External libraries are correct \item Verification tools have no bugs \end{itemize} \vspace{0.5em} \begin{center} \textit{Important to understand what guarantees you're getting} \end{center} \end{frame} \begin{frame}{Two approaches to correctness} \begin{center} \Large How do we prove code is correct? \end{center} \vspace{1em} \begin{enumerate} \item \textbf{Equivalence to reference} \begin{itemize} \item Compare to trusted implementation \item Same outputs for same inputs \item Natural for optimizations \end{itemize} \vspace{0.5em} \item \textbf{Functional specification} \begin{itemize} \item Pre-conditions on inputs \item Post-conditions on outputs \item More flexible approach \end{itemize} \end{enumerate} \end{frame} \begin{frame}{The mathematical challenge} \begin{center} \Large Crypto proofs need non-trivial mathematics \end{center} \vspace{1em} \begin{itemize} \item Modular arithmetic properties \item Field operations \item Group theory \item Number-theoretic facts \end{itemize} \vspace{0.5em} \textbf{The balance:} \begin{itemize} \item Too much automation \rightarrow\ can't handle the math \item Too manual \rightarrow\ overwhelming effort \item SMT solvers help find the sweet spot \end{itemize} \end{frame} \begin{frame}{From source to machine code} \begin{center} \Large The compiler gap \end{center} \vspace{1em} \begin{itemize} \item Most verification happens at source level \item But we execute machine code! \item Regular compilers can introduce bugs \end{itemize} \vspace{0.5em} \textbf{Solution: Verified compilers} \begin{itemize} \item CompCert: Formally verified C compiler \item Guarantees preservation of properties \item Trade-off: Fewer optimizations, fewer platforms \end{itemize} \end{frame} \begin{frame}{Program verification tools landscape} \begin{center} \Large A rich ecosystem of verification tools \end{center} \vspace{1em} \textbf{Key dimensions to consider:} \begin{itemize} \item Memory safety guarantees \item Level of automation \item Parametric verification support \item Input languages \item Analysis targets \item Trust requirements \end{itemize} \end{frame} \begin{frame}{Memory safety: Table stakes} \begin{center} \Large Can the tool prove absence of memory errors? \end{center} \vspace{1em} \textbf{Critical for crypto code:} \begin{itemize} \item Buffer overflows can leak secrets \item Use-after-free exposes sensitive data \item Null pointer dereferences crash systems \end{itemize} \vspace{0.5em} \begin{center} \textit{Most modern verification tools provide this as baseline} \end{center} \end{frame} \begin{frame}{Input languages: Many flavors} \textbf{Verification-oriented languages:} \begin{itemize} \item \textbf{Dafny}: High-level imperative \item \textbf{\fstar}: Functional with effects \item \textbf{Gallina} (Coq): Pure functional \item \textbf{WhyML} (Why3): Functional core \end{itemize} \vspace{0.5em} \textbf{Assembly-like languages:} \begin{itemize} \item \textbf{CryptoLine}: Low-level verification \item \textbf{Jasmin}: Assembly with high-level features \item \textbf{Vale}: Structured assembly \end{itemize} \vspace{0.5em} \textbf{Existing languages:} \begin{itemize} \item Some tools verify C, Java directly \end{itemize} \end{frame} \begin{frame}{Analysis targets: Source vs. Assembly} \begin{center} \Large Where does verification happen? \end{center} \vspace{1em} \textbf{Source-level analysis:} \begin{itemize} \item Easier to verify \item Need verified compiler for guarantees \item Performance penalty from compiler limitations \end{itemize} \vspace{0.5em} \textbf{Assembly-level analysis:} \begin{itemize} \item Harder to verify \item Direct machine-code guarantees \item No compiler performance penalty \end{itemize} \end{frame} \begin{frame}{The trust question} \begin{center} \Large What's in the trusted computing base? \end{center} \vspace{1em} \textbf{Common trust dependencies:} \begin{itemize} \item SMT solvers (Z3, CVC4, etc.) \item Theorem provers (Coq, Isabelle) \item Tool implementations themselves \item Interoperability glue code \item Specifications of external libraries \end{itemize} \vspace{0.5em} \begin{center} \textit{``Who verifies the verifiers?''} \end{center} \end{frame} \begin{frame}{Real deployment success stories} \begin{center} \Large Verified crypto is no longer just academic! \end{center} \vspace{1em} \textbf{Major deployments:} \begin{itemize} \item \textbf{\haclstar}: Used in Mozilla Firefox's NSS \item \textbf{Fiat Cryptography}: Powers Google's BoringSSL \end{itemize} \vspace{0.5em} \begin{center} \textit{Billions of users rely on verified crypto every day} \end{center} \end{frame} \begin{frame}{What made these deployments succeed?} \begin{center} \Large Three critical success factors \end{center} \vspace{1em} \begin{enumerate} \item \textbf{Performance parity} \begin{itemize} \item As fast or faster than existing code \item No performance penalty for verification \end{itemize} \vspace{0.5em} \item \textbf{API compatibility} \begin{itemize} \item Drop-in replacement \item Fits existing infrastructure \end{itemize} \vspace{0.5em} \item \textbf{Industry collaboration} \begin{itemize} \item Team members worked with companies \item Understood real-world needs \end{itemize} \end{enumerate} \end{frame} \begin{frame}{The \haclstar approach} \begin{center} \Large Going beyond just verification \end{center} \vspace{1em} \textbf{What \haclstar did right:} \begin{itemize} \item Replaced entire ciphersuite \item Not just individual primitives \item Comprehensive testing infrastructure \item Professional packaging \end{itemize} \vspace{1em} \begin{center} \textit{Willing to do the ``boring'' work that matters for adoption} \end{center} \end{frame} \begin{frame}{A paradigm shift in verification} \begin{center} \Large Old wisdom: Verified code = Slow code \vspace{1em} \textbf{New reality: Verified code matches or beats unverified!} \end{center} \vspace{1em} \begin{itemize} \item Decades of skepticism overcome \item Proof burden no longer prohibitive \item Performance penalty eliminated \end{itemize} \vspace{0.5em} \begin{center} \textit{No conceptual barrier to verifying the fastest implementations} \end{center} \end{frame} \begin{frame}{Case study: Curve25519 performance} \begin{center} \Large Let's look at real numbers \end{center} \vspace{1em} \textbf{Curve25519:} \begin{itemize} \item Widely used elliptic curve \item Speed competition among implementers \item Verification community joined the race \end{itemize} \vspace{0.5em} \textbf{The benchmark:} \begin{itemize} \item Scalar multiplication operation \item Measured in CPU cycles \item Intel i7-8565U @ 1.8 GHz \item Compared against donna64 (fast unverified C) \end{itemize} \end{frame} \begin{frame}{Curve25519: The results} \begin{center} \Large Verified implementations win! \end{center} \vspace{1em} \textbf{C implementations:} \begin{itemize} \item \textbf{hacl} (verified) \rightarrow\ Beats donna64 \item \textbf{fiat} (verified) \rightarrow\ Beats donna64 \item Multiple verified implementations faster than best unverified C \end{itemize} \vspace{0.5em} \textbf{Assembly implementations:} \begin{itemize} \item \textbf{evercrypt} (verified) \rightarrow\ Matches fastest unverified \item \textbf{precomp} (unverified) \rightarrow\ The target to beat \end{itemize} \vspace{0.5em} \begin{center} \textit{Verification no longer means compromise on speed} \end{center} \end{frame} \begin{frame}{The verification effort spectrum} \begin{center} \Large Higher performance = Higher verification effort \end{center} \vspace{1em} \begin{center} \begin{tikzpicture}[scale=0.8] \draw[->] (0,0) -- (10,0) node[right] {Performance}; \draw[->] (0,0) -- (0,4) node[above] {Verification Effort}; \node[circle,fill=blue!30] at (2,1) {High-level}; \node[circle,fill=orange!30] at (5,2) {C code}; \node[circle,fill=red!30] at (8,3.5) {Assembly}; \draw[dashed,gray] (2,0) -- (2,1); \draw[dashed,gray] (5,0) -- (5,2); \draw[dashed,gray] (8,0) -- (8,3.5); \end{tikzpicture} \end{center} \end{frame} \begin{frame}{Looking ahead} \begin{center} \Large Verified crypto is becoming the new normal \end{center} \vspace{0.5em} \textbf{What we've achieved:} \begin{itemize} \item Performance parity with unverified code \item Real-world deployment at scale \item Growing ecosystem of tools \end{itemize} \vspace{0.5em} \textbf{What's next:} \begin{itemize} \item Better automation \item Shared infrastructure \item More platforms \item Broader adoption \end{itemize} \end{frame} \section{Implementation-Level Security} \begin{frame}{The gap between theory and practice} \begin{center} \Large Design-level security is not enough! \end{center} \vspace{1em} \textbf{What we assume at design level:} \begin{itemize} \item Attackers choose inputs \item Attackers observe outputs \item That's it! \end{itemize} \vspace{0.5em} \textbf{Reality:} \begin{itemize} \item Attackers see much more \item Implementation details leak information \item Side-channels everywhere \end{itemize} \end{frame} \begin{frame}{Side channels: The hidden attack surface} \begin{center} \Large What are side channels? \end{center} \vspace{1em} \textbf{Information leaks through:} \begin{itemize} \item \textbf{Timing}: How long operations take \item \textbf{Memory access}: Which addresses are accessed \item \textbf{Power consumption}: How much energy is used \item \textbf{Electromagnetic radiation}: EM emissions \item \textbf{Acoustic}: Sound of computation \end{itemize} \vspace{0.5em} \begin{center} \textit{These are side-effects of computation, not intended outputs} \end{center} \end{frame} \begin{frame}{The devastating impact} \begin{center} \Large Side channels aren't just theoretical! \end{center} \vspace{1em} \textbf{Real attacks on real systems:} \begin{itemize} \item \textbf{RSA key recovery}: Full private keys extracted \item \textbf{AES key recovery}: Secret keys leaked \item \textbf{TLS attacks}: Lucky 13, Lucky Microseconds \item \textbf{Cloud attacks}: Cross-VM key extraction \end{itemize} \vspace{1em} \begin{center} \textit{Even ``secure'' algorithms become vulnerable in practice} \end{center} \end{frame} \begin{frame}{The constant-time solution} \begin{center} \Large Make execution independent of secrets \end{center} \vspace{1em} \textbf{Constant-time coding guidelines:} \begin{itemize} \item No secret-dependent branches \item No secret-dependent memory access \item No variable-time operations on secrets \item Same number of operations regardless of secret values \end{itemize} \vspace{0.5em} \begin{center} \textit{Note: ``Constant-time'' is about logical flow, not wall-clock time!} \end{center} \end{frame} \begin{frame}{Why constant-time is hard} \begin{center} \Large Natural code patterns become forbidden \end{center} \begin{columns}[t] \begin{column}{0.5\textwidth} \textbf{You can't write:} \begin{enumerate} \item \texttt{if (secret\_bit) \{ ... \}} \item \texttt{array[secret\_index]} \item Return early \texttt{if secret == 0} \item Use division only when \texttt{secret != 0}\footnote{\url{https://kyberslash.cr.yp.to}} \end{enumerate} \end{column} \begin{column}{0.5\textwidth} \textbf{Instead, you must:} \begin{itemize} \item Use bit manipulation tricks \item Process all data uniformly \item Avoid natural optimizations \end{itemize} \end{column} \end{columns} \end{frame} \begin{frame}{Example: Constant-time selection} \textbf{Insecure (natural) code:} \begin{flushleft} \texttt{if (secret\_bit) \{}\\ \texttt{~~~~result = a;}\\ \texttt{\} else \{}\\ \texttt{~~~~result = b;}\\ \texttt{\}} \end{flushleft} \vspace{0.5em} \textbf{Secure (constant-time) code:} \begin{flushleft} \texttt{mask = -secret\_bit;~~// 0x00...0 or 0xFF...F}\\ \texttt{result = (a \& mask) | (b \& \textasciitilde mask);} \end{flushleft} \vspace{0.5em} \begin{center} \textit{Same result, no branches, harder to understand!} \end{center} \end{frame} \begin{frame}{The compiler: Friend or foe?} \begin{center} \Large Your carefully written constant-time code... \vspace{0.5em} ...may not survive compilation! \end{center} \vspace{1em} \textbf{Compiler ``optimizations'' can:} \begin{itemize} \item Reintroduce branches \item Use lookup tables \item Short-circuit operations \item Use variable-time instructions \end{itemize} \vspace{0.5em} \begin{center} \textit{The compiler doesn't know about your security requirements} \end{center} \end{frame} \begin{frame}{Hardware betrays you too} \begin{center} \Large Even perfect assembly isn't safe \end{center} \vspace{1em} \textbf{Modern CPUs ``optimize'' behind your back:} \begin{itemize} \item Branch prediction \item Speculative execution \item Cache hierarchies \item Variable-latency instructions \end{itemize} \vspace{0.5em} \textbf{Result:} \begin{itemize} \item Timing variations you can't control \item Spectre/Meltdown-style attacks \item Cache timing attacks \end{itemize} \end{frame} \begin{frame}{Current practice: Hope and prayer} \begin{center} \Large How do we check constant-time today? \end{center} \vspace{1em} \textbf{1. Manual auditing} \begin{itemize} \item Expensive \item Time-consuming \item Error-prone \item Doesn't scale \end{itemize} \vspace{0.5em} \textbf{2. Testing wall-clock time} \begin{itemize} \item Fundamentally flawed approach \item Misunderstands constant-time \item Can't test all inputs \item Misses subtle leaks \end{itemize} \end{frame} \begin{frame}{A history of patches creating vulnerabilities} \begin{center} \Large Even experts get it wrong \end{center} \vspace{1em} \textbf{The vicious cycle in TLS:} \begin{enumerate} \item Original TLS timing vulnerability discovered \item Developers create a patch to fix it \item The patch itself is flawed \item This creates the Lucky 13 vulnerability \item Lucky 13 gets patched \item The Lucky 13 patch introduces a new timing vulnerability! \end{enumerate} \vspace{1em} \begin{center} \textit{Each ``fix'' introduced new vulnerabilities!} \end{center} \end{frame} \begin{frame}{The assembly escape hatch} \begin{center} \Large Can't trust the compiler? Skip it! \end{center} \vspace{1em} \textbf{Current practice:} \begin{itemize} \item Write critical code in assembly \item Implement constant-time directly \item Control every instruction \end{itemize} \vspace{0.5em} \textbf{The cost:} \begin{itemize} \item Platform-specific implementations \item Harder to audit \item More error-prone \item Maintenance nightmare \end{itemize} \end{frame} \begin{frame}{Enter computer-aided cryptography} \begin{center} \Large What if we could \textbf{prove} constant-time? \end{center} \vspace{1em} \textbf{CAC tools can:} \begin{itemize} \item Automatically check constant-time compliance \item Find subtle violations \item Even repair non-compliant code! \item Provide formal guarantees \end{itemize} \vspace{0.5em} \begin{center} \textit{Turn informal best practices into verified properties} \end{center} \end{frame} \begin{frame}{Formal leakage models} \begin{center} \Large What exactly does the attacker see? \end{center} \vspace{1em} \textbf{We must formally model leakage:} \begin{itemize} \item Define what operations leak \item Specify what information is revealed \item Abstract real-world observations \end{itemize} \vspace{0.5em} \textbf{Key insight:} \begin{center} \textit{Security = Leakage independent of secrets} \end{center} \vspace{0.5em} This is \textbf{observational non-interference} \end{frame} \begin{frame}{Hierarchy of leakage models} \begin{center} \Large Different models for different threats \end{center} \vspace{1em} \textbf{1. Program counter (PC) model} \begin{itemize} \item Leaks: Control flow only \item Protects against: Simple timing attacks \end{itemize} \vspace{0.5em} \textbf{2. Constant-time model} \begin{itemize} \item Leaks: PC + memory addresses \item Protects against: Cache attacks, timing attacks \item Most common in practice \end{itemize} \vspace{0.5em} \textbf{3. Size-respecting model} \begin{itemize} \item Leaks: PC + memory + operand sizes \item Protects against: Variable-time operations \end{itemize} \end{frame} \begin{frame}{Program counter leakage} \begin{center} \Large The simplest model: Control flow leaks \end{center} \vspace{1em} \textbf{What leaks:} \begin{itemize} \item Which branch was taken \item How many loop iterations \item Which functions were called \end{itemize} \vspace{0.5em} \textbf{Example violation:} \begin{flushleft} \texttt{if (password[i] != input[i]) \{}\\ \texttt{~~~~return FAIL;~~// Early exit leaks position}\\ \texttt{\}} \end{flushleft} \vspace{0.5em} \begin{center} \textit{Timing reveals where passwords differ!} \end{center} \end{frame} \begin{frame}{Constant-time leakage} \begin{center} \Large The standard model: PC + memory access \end{center} \vspace{1em} \textbf{Additionally leaks:} \begin{itemize} \item Which memory addresses are accessed \item Not the values, just the addresses! \end{itemize} \vspace{0.5em} \textbf{Example violation:} \texttt{result = lookup\_table[secret\_index]} \vspace{0.5em} \begin{center} \textit{Cache attacks can recover \texttt{secret\_index}} \end{center} \end{frame} \begin{frame}{The verification promise} \begin{center} \Large Prove once, secure forever \end{center} \vspace{1em} \textbf{Verification tools can prove:} \begin{itemize} \item Code follows constant-time discipline \item For all possible secret values \item Through all execution paths \item Despite complex control flow \end{itemize} \vspace{0.5em} \begin{center} \textit{No more hoping your tests caught everything} \end{center} \end{frame} \begin{frame}{The fine print} \begin{center} \Large What are we actually proving? \end{center} \vspace{1em} \textbf{Important caveats:} \begin{itemize} \item Proofs are relative to the leakage model \item Hardware may leak more than modeled \item New attacks may require new models \item Speculative execution is particularly tricky \end{itemize} \vspace{0.5em} \begin{center} \textit{We prove security in our model, not absolute security} \end{center} \end{frame} \begin{frame}{The gap remains} \begin{center} \Large From verified code to secure execution \end{center} \vspace{1em} \textbf{Remaining challenges:} \begin{itemize} \item Compiler may still break guarantees \item Hardware may not respect assumptions \item Micro-architectural attacks (Spectre/Meltdown) \item Physical side channels \end{itemize} \vspace{0.5em} \textbf{Partial solutions:} \begin{itemize} \item Verify at assembly level \item Use verified compilers \item Hardware/software co-design \end{itemize} \end{frame} \begin{frame}{Looking forward} \begin{center} \Large Implementation security is an arms race \end{center} \vspace{1em} \textbf{The cycle continues:} \begin{enumerate} \item New side channels discovered \item Update leakage models \item Develop countermeasures \item Verify implementations \item Repeat... \end{enumerate} \vspace{0.5em} \begin{center} \textit{CAC tools help us stay ahead in this race} \end{center} \end{frame} \begin{frame}{Computational analysis tools overview} \bigimagewithcaption{verif_implementations.png}{Source: Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao and Bryan Parno, SoK: Computer-Aided Cryptography, IEEE Symposium on Security and Privacy, 2021.} \end{frame} \section{Case Study: Lessons Learned from TLS} \begin{frame}{Case Study: Transport Layer Security (TLS)} \begin{center} \Large One of the most important real-world deployments of cryptography \end{center} \vspace{1em} \begin{itemize} \item Powers HTTPS everywhere \item Secures email, VPNs, messaging \item Protects billions of connections daily \end{itemize} \vspace{1em} \begin{center} \textit{But the road to secure TLS was long and painful...} \end{center} \end{frame} \begin{frame}{The dark ages: TLS before 1.3} \begin{center} \Large A reactive cycle of attacks and patches \end{center} \vspace{1em} \textbf{The endless loop:} \begin{enumerate} \item \textbf{Attack found} -- Security researchers discover vulnerability \item \textbf{Quick patch} -- Rushed fix deployed to stop bleeding \item \textbf{Long-term fix} -- More thoughtful solution developed \item \textbf{Next version} -- Protocol updated with fixes \item \textbf{Back to step 1} -- New attacks emerge on ``fixed'' version \end{enumerate} \vspace{0.5em} \begin{center} \textit{No substantial academic analysis during design} \end{center} \end{frame} \begin{frame}{Early academic analysis: Too simple} \begin{center} \Large Academics studied ``toy'' versions of TLS \end{center} \vspace{1em} \textbf{Why oversimplified models?} \begin{itemize} \item Full protocol too complex \item Analysis tools couldn't handle it \item Focused on cryptographic core only \end{itemize} \vspace{0.5em} \textbf{The consequence:} \begin{itemize} \item Missed many real attacks \item False sense of security \item Gap between theory and practice \end{itemize} \end{frame} \begin{frame}{The complexity explosion} \begin{center} \Large When academics looked at \textit{real} TLS... \end{center} \vspace{1em} \begin{center} \textbf{Many new attacks discovered!} \end{center} \vspace{0.5em} \begin{itemize} \item BEAST \item CRIME \item Lucky 13 \item POODLE \item Logjam \item And many more, as discussed in our TLS session! \end{itemize} \vspace{0.5em} \begin{center} \textit{The devil was in the details we'd been ignoring} \end{center} \end{frame} \begin{frame}{TLS 1.3: A paradigm shift} \begin{center} \Large From reactive patching to proactive design \end{center} \vspace{1em} \textbf{Revolutionary changes:} \begin{itemize} \item Academic community consulted \textbf{during} design \item Multiple drafts analyzed formally \item 28 drafts over 4+ years! \item Unprecedented collaboration \end{itemize} \vspace{0.5em} \begin{center} \textit{First major protocol designed with formal analysis in mind} \end{center} \end{frame} \begin{frame}{Computer-aided cryptography joins the party} \begin{center} \Large Multiple tools, multiple approaches \end{center} \vspace{1em} \textbf{Verified implementations:} \begin{itemize} \item Implementations with cryptographic proofs \end{itemize} \vspace{0.5em} \textbf{Symbolic analysis:} \begin{itemize} \item ProVerif models \item Tamarin models \end{itemize} \vspace{0.5em} \textbf{Computational analysis:} \begin{itemize} \item CryptoVerif proofs \end{itemize} \vspace{0.5em} \begin{center} \textit{A comprehensive assault on insecurity!} \end{center} \end{frame} \begin{frame}{Lesson 1: Formal methods find real flaws} \begin{center} \Large The process of formally specifying reveals bugs \end{center} \vspace{1em} \textbf{Just trying to write formal specs uncovers issues:} \begin{itemize} \item Ambiguities in the standard \item Implicit assumptions \item Corner cases \item Unclear security goals \end{itemize} \vspace{0.5em} \begin{center} \textit{If you can't specify it clearly, it's probably broken} \end{center} \end{frame} \begin{frame}{Real attacks found by formal analysis} \begin{center} \Large These aren't theoretical problems! \end{center} \vspace{1em} \textbf{TLS 1.2 analysis (Bhargavan et al.):} \begin{itemize} \item Alert fragmentation attacks \item Fingerprinting attacks \item Led to Triple Handshake attack discovery \end{itemize} \vspace{0.5em} \textbf{TLS 1.3 draft 10 (Cremers et al.):} \begin{itemize} \item Client impersonation in PSK-resumption \item Fixed in draft 11 \end{itemize} \end{frame} \begin{frame}{More attacks from formal analysis} \textbf{TLS 1.3 draft 13 (Bhargavan et al.):} \begin{itemize} \item New attack on 0-RTT client authentication \item ProVerif found what humans missed \end{itemize} \vspace{0.5em} \textbf{TLS 1.3 draft 21 (Cremers et al.):} \begin{itemize} \item Unexpected behavior affecting authentication \item Tamarin revealed subtle issues \end{itemize} \vspace{1em} \begin{center} \Large Nearly all discoveries led to protocol improvements! \end{center} \end{frame} \begin{frame}{Lesson 2: Protocols are moving targets} \begin{center} \Large 28 drafts = 28 different protocols! \end{center} \vspace{1em} \textbf{The challenge:} \begin{itemize} \item Significant changes between drafts \item Previous analyses quickly outdated \item Manual proofs become stale \item Months of work invalidated \end{itemize} \vspace{0.5em} \begin{center} \textit{How do you hit a moving target?} \end{center} \end{frame} \begin{frame}{Machine-checked proofs to the rescue} \begin{center} \Large Automated tools can evolve with the protocol \end{center} \vspace{1em} \textbf{Key advantages:} \begin{itemize} \item Update models incrementally \item Re-run verification automatically \item Catch regressions immediately \item Ensure fixes don't break other properties \end{itemize} \vspace{0.5em} \textbf{Manual proofs can't compete:} \begin{itemize} \item Too slow to update \item Error-prone modifications \item Can't keep pace with drafts \end{itemize} \end{frame} \begin{frame}{Lesson 3: Design for verifiability} \begin{center} \Large Small changes can dramatically simplify analysis \end{center} \vspace{1em} \textbf{TLS 1.3 embraced verification-friendly changes:} \begin{itemize} \item Better key separation in key schedule \item Consistent message tagging \item More transcript information in exchanges \item Cleaner state machine \end{itemize} \vspace{0.5em} \begin{center} \textit{Negligible performance impact, huge verification benefit} \end{center} \end{frame} \begin{frame}{Examples of verification-friendly changes} \textbf{Key separation:} \begin{itemize} \item Different keys for different purposes \item Enables modular security proofs \item Prevents cross-protocol attacks \end{itemize} \vspace{0.5em} \textbf{Consistent tagging:} \begin{itemize} \item Every message type clearly labeled \item No ambiguity in parsing \item Simplifies formal models \end{itemize} \vspace{0.5em} \textbf{Transcript inclusion:} \begin{itemize} \item Include history in handshake messages \item Makes consistency proofs easier \item Prevents replay attacks \end{itemize} \end{frame} \begin{frame}{The impact: A new standard for standards} \begin{center} \Large TLS 1.3 changed how protocols should be designed \end{center} \vspace{1em} \textbf{The new playbook:} \begin{enumerate} \item Involve formal methods experts early \item Design with verification in mind \item Use tools throughout development \item Update proofs with each draft \item Fix issues before standardization \end{enumerate} \vspace{0.5em} \begin{center} \textit{From ``ship and patch'' to ``verify and ship''} \end{center} \end{frame} \begin{frame}{Why this matters beyond TLS} \begin{center} \Large TLS 1.3 proved formal methods can scale \end{center} \vspace{1em} \textbf{Key achievements:} \begin{itemize} \item Analyzed a \textit{real} protocol, not a toy \item Found and fixed \textit{real} vulnerabilities \item Kept pace with \textit{real} development \item Influenced \textit{real} design decisions \end{itemize} \vspace{0.5em} \begin{center} \textit{This is the future of secure protocol design} \end{center} \end{frame} \begin{frame}[plain] \titlepage \end{frame} \end{document}