Analysis of the Security Design, Engineering, and Implementation of the SecureDNA System

TL;DR

This work analyzes the security design, engineering, and implementation of SecureDNA's privacy-preserving hazard screening system for DNA synthesis orders. It applies formal-methods (strand spaces and CPSA) to model the basic order-request and exemption-handling protocols, uncovering fundamental weaknesses that undermine defense-in-depth through a flawed SCEP and weak bindings. The authors demonstrate that SCEP provides only one-way authentication and that critical bindings are insufficient, proposing SCEP+ and other mitigations that are formally validated, with Version 1.1.0 implementing the fixes. The study highlights the crucial role of formal-methods analysis in protocol design and offers concrete guidance for strengthening security engineering in privacy-preserving biomedical screening with practical regulatory and safety implications.

Abstract

We analyze security aspects of the SecureDNA system regarding its system design, engineering, and implementation. This system enables DNA synthesizers to screen order requests against a database of hazards. By applying novel cryptography, the system aims to keep order requests and the database of hazards secret. Discerning the detailed operation of the system in part from source code (Version 1.0.8), our analysis examines key management, certificate infrastructure, authentication, and rate-limiting mechanisms. We also perform the first formal-methods analysis of the mutual authentication, basic request, and exemption-handling protocols. Without breaking the cryptography, our main finding is that SecureDNA's custom mutual authentication protocol SCEP achieves only one-way authentication: the hazards database and keyservers never learn with whom they communicate. This structural weakness violates the principle of defense in depth and enables an adversary to circumvent rate limits that protect the secrecy of the hazards database, if the synthesizer connects with a malicious or corrupted keyserver or hashed database. We point out an additional structural weakness that also violates the principle of defense in depth: inadequate cryptographic bindings prevent the system from detecting if responses, within a TLS channel, from the hazards database were modified. Consequently, if a synthesizer were to reconnect with the database over the same TLS session, an adversary could replay and swap responses from the database without breaking TLS. Although the SecureDNA implementation does not allow such reconnections, it would be stronger security engineering to avoid the underlying structural weakness. We identify these vulnerabilities and suggest and verify mitigations, including adding strong bindings. Software Version 1.1.0 fixes SCEP with our proposed SCEP+ protocol.

Figures (8)

• Figure 1: Architecture of the SecureDNA system showing the roles and cryptographic variables held by each role.
• Figure 2: The basic order-request protocol. Steps 2 and 5 call a custom mutual authentication protocol SCEP (see Section \ref{['ssec:custom']}).
• Figure 3: The exemption-handling protocol. ${\mathcal{C}}$'s request includes an ELT signed by ${\mathcal{B}}$ and a one-time passcode (the "Auth Device Code"). In ${\mathcal{H}}$'s response to ${\mathcal{S}}$, ${\mathcal{H}}$ sends a list of sequences that are in its database, with boolean flags indicating which sequences are also in the exemption token. ${\mathcal{H}}$ verifies that ${\mathcal{C}}$ included a valid passcode. Steps 2 and 5 call a custom mutual authentication protocol SCEP (see Section \ref{['ssec:custom']}).
• Figure 4: Ladder diagram of the custom mutual authentication (SCEP) protocol. Vertical lines correspond to communicating roles (${\mathcal{S}}$, ${\mathcal{K}}$, ${\mathcal{H}}$). Arrows between vertical lines indicate roles transmitting and receiving protocol messages. SCEP assumes an existing one-way authenticated TLS channel between the synthesizer ${\mathcal{S}}$, and the keyserver ${\mathcal{K}}$ or the keyed hash database ${\mathcal{H}}$. Some message components appear only when ${\mathcal{S}}$ communicates with ${\mathcal{K}}$; we indicate these components by surrounding them with brackets ([]). The responder nonce $N$, token $T$, and secret signing key $d$ correspond to the entity with which ${\mathcal{S}}$ communicates. Upon completing SCEP, ${\mathcal{S}}$ obtains a request cookie $\omega$, which ${\mathcal{S}}$ transmits in a subsequent request to ${\mathcal{K}}$ or ${\mathcal{H}}$.
• Figure 5: Ladder diagrams of the basic order-request and exemption-handling protocols. Because ${\mathcal{S}}$ communicates with ${\mathcal{K}}$ and ${\mathcal{H}}$ over separate, one-way authenticated TLS connections, ${\mathcal{S}}$ completes the SCEP mutual authentication protocol (see Figure \ref{['fig:auth-ladder']}) in Steps 1 and 4 to obtain request cookies $\omega_\mathcal{K}$ and $\omega_\mathcal{H}$. When completing SCEP with ${\mathcal{K}}$, ${\mathcal{S}}$ includes ${\mathcal{K}}$'s identifier $I\!D_\mathcal{K}$. In Step 2, ${\mathcal{S}}$ transmits to ${\mathcal{K}}$ the cookie $\omega_\mathcal{K}$, blinded sequences $M(s)^\beta$ and (optionally) the blinded exempt sequences $M(s_E)^\beta$. In Step 5, ${\mathcal{K}}$ transmits $\omega_\mathcal{H}$, $M(s)^k$, and an optional tuple (exemption token $T^E$, second-factor authentication code $O_A$, and exemption sequence $M(s_E)^k$), to which ${\mathcal{K}}$ receives a query response that grants or denies the synthesis request in Step 6.

Theorems & Definitions (52)

• Definition 9.1: Strand Space
• Definition 9.2: Penetrator Strands
• Definition 9.3: Public and Private Keys
• Definition 9.4: TLS Traces
• Definition 9.5: SCEP Token
• Definition 9.6: SCEP Traces
• Definition 9.7
• Definition 9.8: SCEP Strand Space
• Definition 9.9: Listener Strands
• Definition 9.10: Confidentiality