Symbolic Parallel Composition for Multi-language Protocol Verification

TL;DR

The paper tackles the challenge of verifying security protocols implemented with components in multiple languages by introducing Symbolic Parallel Composition, which treats different languages as symbolic LTSs connected through a shared symbol space. Central to the approach is symbolic execution semantics for each component and a combined deduction relation that enables cross-language reasoning about messages without translating base types like bitstrings into DY terms. The authors formalize the framework in HOL4, prove correctness and refinement theorems, and instantiate the method with SBIR and Sapic^+ representations, culminating in end-to-end correctness results for ARMv8 binaries via the BIR intermediate representation. The TinySSH and WireGuard case studies demonstrate the practicality of end-to-end verification, showing mutual authentication and forward secrecy preserved across multi-language implementations. Overall, the framework offers a scalable, language-agnostic path to secure interactions in complex, multi-language environments, with potential extensions to probabilistic and multi-party settings.

Abstract

The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics. This facilitates the (parallel) composition of labeled transition systems, improving the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev-Yao (DY) model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and DY terms. Our technique provides a foundation for securing interactions in multi-language environments, enhancing program verification and system analysis in complex, interconnected systems.

Figures (12)

• Figure 1: The DY attacker's deduction rules. Top-left to bottom-right: the attacker knows the messages it received and can apply function symbols. If a name is public, the attacker knows this name, and equivalent names to fresh names are also fresh. Equivalence modulo $E$ translates into an equivalence judgment, and if a term is known, any equivalent terms are also known. Any terms that correspond to a given symbol are known if the symbol itself is known.
• Figure 2: The transition relation rules for Dolev-Yao attacker model.
• Figure 3: The transition relation rules for Dolev-Yao library model.
• Figure 4: A DY attacker removing bit-level masking using $\vdash_{\mathbf{{\color{RoyalBlue}{1}}} \mathsf{{\color{RedOrange}{2}}}}^\mathsf{bit}$ in \ref{['ex:BS-manipulation']}
• Figure 5: A fragment of the $\mathbf{{\color{RoyalBlue}{BIR}}}$ syntax

Theorems & Definitions (21)

• Example 1: Bitstring manipulation
• Definition 1: Symbolic LTS
• Definition 2: Symbolic Parallel Composition
• Example 2: DY communicates with crypto library
• Example 3: Logical truth
• Example 4: Masked encryption key
• Example 5: Transferable equalities
• Theorem 1: Symbolic Composition Correctness
• proof
• Lemma 1: confSymbolic Compositional Trace Inclusion fullSymbolic Compositional Trace Inclusion revisionSymbolic Compositional Trace Inclusion