Compiler Correctness: A Formal Proof for Cryptographic Security

by

Author: Denis Avetisyan

Researchers have formally verified the Jasmin compiler, establishing guarantees that cryptographic implementations remain secure even after compilation.

The paper leverages Interaction Trees and Relational Hoare Logic to demonstrate IND-CCA security preservation for Key Encapsulation Mechanisms (KEMs).

While formally verifying compilers typically focuses on functional correctness, ensuring cryptographic security—a nuanced property involving probabilistic and potentially non-terminating computations—presents unique challenges. This paper, ‘The Jasmin Compiler Preserves Cryptographic Security’, addresses this gap by providing a formal guarantee that the Jasmin compiler—a framework for developing efficient, verified cryptographic implementations—preserves cryptographic security, specifically IND-CCA for Key Encapsulation Mechanisms. Leveraging a novel Relational Hoare Logic and a denotational semantics based on interaction trees, we rigorously demonstrate this preservation. Could these techniques be extended to verify other cryptographic compilers and broaden the scope of formally verified security properties?

Foundations of Secure Digital Systems

Modern secure communication fundamentally depends on cryptographic primitives, and among these, the Key Encapsulation Mechanism (KEM) plays a crucial role. A KEM allows two parties to establish a shared secret key over a public channel, even in the presence of an eavesdropper. This process involves one party generating a public key and a corresponding secret key. The public key is then used to encapsulate a random secret, creating a ciphertext. This ciphertext, along with the encapsulated secret, is sent to the other party. Using its own secret key, the receiving party decapsulates the ciphertext, recovering the original secret. This shared secret can then be used for symmetric encryption, enabling confidential communication. The beauty of KEMs lies in their resistance to attacks even if the encryption algorithm itself were to be compromised, offering a forward-secure foundation for numerous digital security protocols, from secure web browsing ($https$) to encrypted messaging.

While cryptographic primitives like key encapsulation mechanisms (KEMs) provide a theoretical foundation for secure communication, their practical security is critically dependent on correct implementation. Subtle flaws in software or hardware – such as timing attacks, side-channel leakage, or buffer overflows – can compromise even the most robust algorithms. These vulnerabilities arise from the translation of mathematical specifications into executable code, introducing opportunities for attackers to exploit weaknesses beyond the algorithm’s inherent design. Consequently, rigorous testing, formal verification, and constant vigilance against implementation-level attacks are essential to ensure that cryptographic systems deliver on their promise of confidentiality and integrity; a perfectly secure algorithm remains vulnerable if its deployment is careless or flawed.

Defining Program Meaning for Rigorous Verification

Formal program verification relies on a rigorous definition of program semantics, which specifies the precise relationship between program state and expected behavior. This definition moves beyond intuitive understanding and establishes a mathematical basis for determining correctness. Specifically, program semantics must clearly delineate the valid states a program can occupy, the transitions between those states, and the resulting output for given inputs. Without a formal semantic definition, it is impossible to objectively determine if a program meets its intended specification or to prove the absence of runtime errors. This precision is essential for automated verification tools and techniques, enabling them to analyze code and confirm its adherence to defined properties.

Big-step semantics defines program behavior by specifying the result of executing a program or a portion of a program in a single step, moving the program state directly from an initial configuration to a final one. This approach is well-suited for reasoning about program equivalence and termination, as it focuses on the overall transformation. Conversely, coinductive semantics describes program behavior as the limit of an infinite sequence of states, defining what holds true at all possible stages of computation. This is particularly effective for modeling potentially infinite computations and defining the meaning of recursive programs, where the behavior is defined by the potentially unending unfolding of recursion. Both frameworks utilize mathematical relations to define valid program steps, but differ in how they represent the progression of computation and the types of programs for which they provide the most natural and expressive definitions.

A simulation relation, formally defined as a relation $R$ between states of a source and target program, is fundamental to establishing program equivalence during compilation. This relation must satisfy the condition that if the source program is in state $s$ and transitions to state $s’$, then the target program, starting from the corresponding state in $R$ with $s$, must be able to transition to a state $t$ that is also in $R$ with $s’$. Demonstrating the existence of such a relation proves that any behavior observable in the source program is also reproducible in the target program, thereby validating the correctness of the compilation process. The precision of the simulation relation directly impacts the strength of the equivalence proof; a stronger relation implies a more robust guarantee of behavioral preservation.

Jasmin: A Compiler Architected for Assurance

Jasmin is a compiler framework developed with a primary focus on cryptographic applications demanding high assurance and performance. Unlike general-purpose compilers, Jasmin is specifically engineered to facilitate formal verification of generated code, prioritizing correctness and security over raw speed. This design allows developers to mathematically prove properties of their cryptographic implementations, such as resistance to specific attacks, directly from the source code. The framework supports the development of high-speed cryptographic primitives while enabling rigorous analysis to ensure the absence of vulnerabilities, which is crucial for sensitive applications like key management, secure communication protocols, and data encryption.

The Jasmin Front-End constitutes the first stage of the compilation process, responsible for converting source code, typically written in a high-level language, into a formally defined intermediate representation (IR). This IR is specifically designed to facilitate formal verification; its structure is relatively simple and abstract, removing complexities introduced by target-specific optimizations or low-level details. The resulting IR is not machine code, but rather a set of instructions suitable for analysis and proof, enabling rigorous examination of the program’s semantics before subsequent compilation stages. This separation of concerns – ensuring semantic correctness at the IR level – is a key design principle of Jasmin, supporting the ultimate goal of a formally verified compiler.

A core objective of the Jasmin compiler project is to provide a formal correctness proof, mathematically establishing that the compilation process accurately preserves the intended behavior of the source code. This paper details such a proof, specifically demonstrating Indistinguishability under Chosen-Ciphertext Attack (IND-CCA) security. IND-CCA security guarantees that an attacker cannot distinguish between encryptions of different messages, even with the ability to request the decryption of chosen ciphertexts. The provided proof rigorously shows that Jasmin’s compilation process does not introduce vulnerabilities that would compromise this security property, ensuring the compiled code maintains the same level of cryptographic protection as the original, formally verified source.

Formalizing Compiler Correctness with Advanced Techniques

The formal verification of the Jasmin compiler relies on a combined methodology utilizing Relational Hoare Logic (RHL) and Interaction Trees (ITrees). RHL provides a formal system for reasoning about the relationship between program states before and after execution, specifically addressing the challenges presented by mutable state and aliasing. ITrees, a graphical formalism, represent the possible interactions between a program and its environment, enabling a structured approach to verifying program behavior against specified contracts. This integration allows for the rigorous demonstration of compiler correctness by formally relating the source and target code semantics, ensuring that the compilation process preserves program meaning and does not introduce unintended behavior. The combination facilitates both the specification of desired properties and the automated or interactive proof of those properties within the compiler.

Traditional Hoare Logic relies on proving preconditions and postconditions for program transformations, requiring a fixed program structure. However, compilation frequently involves structural changes – such as the introduction or removal of nodes in an Abstract Syntax Tree (AST) – that invalidate these fixed-point assumptions. One-Sided Rules within Relational Hoare Logic (RHL) address this by allowing verification to proceed even when the program’s structure is not statically known. These rules define relationships between program states based on how the structure changes, rather than requiring a complete structural equivalence. This is achieved by reasoning about relations between sets of states before and after a transformation, focusing on the validity of logical properties rather than strict structural isomorphism, which is essential for verifying compilers that perform complex AST manipulations.

Static analysis techniques are integrated into the formal verification process to mitigate computational overhead. These techniques pre-process the Jasmin compiler’s front-end code, identifying and simplifying logical relationships before formal proof construction begins. This proactive simplification demonstrably reduces the size of the resulting proofs; specifically, the current implementation achieves approximately a 10% reduction in proof size when compared to previous verification efforts that did not incorporate this level of static analysis. The reduction in proof size directly translates to decreased verification time and resource consumption.

The verification of the Jasmin compiler, as detailed in the study, underscores a principle of systemic integrity. Every component, every transformation within the compiler, impacts the overarching security guarantees. This resonates with John McCarthy’s observation: “The best way to predict the future is to invent it.” The paper doesn’t merely accept the potential for vulnerabilities; it proactively constructs a formally verified system. By meticulously detailing the preservation of IND-CCA security through Interaction Trees and Relational Hoare Logic, the authors demonstrate a commitment to shaping a secure computational future—inventing, rather than simply predicting, a trustworthy software ecosystem. The study highlights that every new dependency, every compiled instruction, is a hidden cost to freedom—a cost the authors address through rigorous formalization.

What Lies Ahead?

The successful verification of the Jasmin compiler, while a necessary step, reveals the field’s inherent fragility. A formally verified compiler is not an island; it is a node in a complex network of tools, libraries, and, crucially, human intention. The preservation of security ultimately rests not on the compiler’s logic alone, but on the soundness of the specification against which it is verified. Current approaches to specifying cryptographic primitives often rely on idealized models – elegant abstractions that bear only a tenuous relationship to concrete implementations. The next challenge, therefore, lies in bridging this gap, developing specification languages that capture the nuances of real-world cryptographic systems without sacrificing the rigor demanded by formal verification.

Furthermore, the Interaction Trees and Relational Hoare Logic employed here, while powerful, represent a significant investment of human effort. Automation remains a distant, though crucial, goal. The complexity of modern cryptographic protocols demands tools that can reason about security properties with minimal human intervention. The pursuit of such tools should not focus solely on scalability, but also on intelligibility. A verification result is only valuable if it can be understood and scrutinized. A black box guarantee, however robust, offers little solace in the face of evolving threats.

Ultimately, the work suggests a shift in focus. The emphasis should move from verifying individual components – compilers, libraries, protocols – to verifying the interactions between them. Security is not a property of isolated systems, but an emergent property of their collective behavior. A holistic approach, grounded in a clear understanding of system structure, is the only path towards truly resilient cryptographic infrastructure.

Original article: https://arxiv.org/pdf/2511.11292.pdf

Contact the author: https://www.linkedin.com/in/avetisyan/

See also:

2025-11-17 21:35