Arduino Vehicle Security

Vehicle Software Updates⋆

Martin Slind Hagena, Emil Lundqvista, Alex Phua, Yenan Wanga,

Abstract

With the rise of software-defined vehicles (SDVs), where software governs most vehicle functions alongside enhanced connectivity, the need for secure software up- dates has become increasingly critical. Software vulnerabilities can severely impact safety, the economy, and society. In response to this challenge, Strandberg et al. [es- car Europe, 2021] introduced the Unified Software Update Framework (UniSUF), designed to provide a secure update framework that integrates seamlessly with existing vehicular infrastructures.

Although UniSUF has previously been evaluated regarding cybersecurity, these as- sessments have not employed formal verification methods. To bridge this gap, we perform a formal security analysis of UniSUF. We model UniSUF’s architecture and assumptions to reflect real-world automotive systems and develop a ProVerif- based framework that formally verifies UniSUF’s compliance with essential security requirements — confidentiality, integrity, authenticity, freshness, order, and live- ness —demonstrating their satisfiability through symbolic execution. Our results demonstrate that UniSUF adheres to the specified security guarantees, ensuring the correctness and reliability of its security framework.

Keywords:

Provable Security, Vehicular Systems, Secure Software Updates ⋆Preprint accepted for publication in Computers & Security 2025 (Hagen et al., 2025).

1. Introduction

Connected cars are quickly becoming the norm, with 96% of manufactured cars in 2030 expected to have connectivity features (Council, 2020). These connected cars feature a multitude of electronic control units (ECUs), with more than 100 ECUs per vehicle (Narisawa et al., 2022). Maintaining and regularly updating these ECUs is critical to prevent security vulnerabilities.

The massive scale of the automotive industry, with over 70 million cars sold worldwide annually (Scotiabank, 2024), makes it a prime target for malicious actors. If an attacker compromises the software update process, the result can be malware installation, sensitive data leakage, and even vehicle hijacking, leading to devastating financial, social, and potentially fatal consequences.

Despite the importance of secure updates, ensuring the confidentiality, in- tegrity, and correct execution of the software update process for connected vehicles remains a highly challenging task.

In Particular, Attackers Could

exploit weaknesses in the update process to install malicious software, eaves- drop on sensitive information, or revert vehicle software to an obsolete version containing vulnerabilities. Moreover, the sheer number of vehicles and ECUs in each car presents a scalability challenge, complicating the implementation of robust security measures across the entire fleet.

1.1. Existing Solutions And Their Shortcomings

Frameworks have been proposed to address these challenges, including the Unified Software Update Framework (UniSUF) (Strandberg et al., 2021a). UniSUF proposes a reference architecture intended to serve as input to stan- dards for secure software updates. UniSUF’s specifications were driven by the following development goals (Strandberg et al., 2023).

Confidentiality: To hinder eavesdropping. G1: Ensure software confidentiality during the software update process. G2: UniSUF session keys can only be viewed in decrypted format by au- thorized software components.

Integrity and Authenticity: To hinder spoofing and tampering. G3: The software is authentic against a certificate and remains unchanged during the update process.

G4: Only authentic resources are processed.

2

Freshness: To hinder replay attacks. G5: An adversary should be unable to revert a vehicle’s software to a previously installed version.

G6: The system creates unique software distribution files per software update. Each such file can only be used for a designated vehicle. Order: To hinder vulnerabilities that take advantage of running the process in an unintended order.

G7: The software update process should follow the correct order. Liveness: Hinder DoS attacks. G8: The software update process should eventually terminate, regardless of success or error.

Figure 1 provides a high-level overview of the UniSUF architecture, illus- trating the main entities involved in the update process: the Producer, the Consumer, Software Suppliers, the Software Repository, and Electronic Con- trol Units (ECUs). Software update packages, referred to as VUUPs, are generated by the Producer based on the latest software versions provided by the Software Suppliers, which have also passed internal testing. The Pro- ducer delivers the VUUPs to the Consumer and uploads the software to the Software Repository. Upon receiving a VUUP, the Consumer processes it and installs the updates on the respective ECUs according to the instruc- tions specified in the VUUP. Section 4 presents detailed architectures and protocol steps.

UniSUF’s prior evaluations focus primarily on practical deployments and lack formal verification of its security guarantees. This leaves the potential for subtle vulnerabilities that attackers could exploit, notably by exposing cryptographic keys or violating the sequence of operations during the update process.

Several scientific challenges are associated with the formal verification of sys- tems like UniSUF. These include [1: Confidentiality] ensuring that the software update process maintains the confidentiality of secret information throughout execution; [2: Integrity and Authenticity] verifying that no unauthorized modifications occur during the update process; and [3: Or- der and Liveness] guaranteeing that the update process follows the correct

3

Figure 1: High-level overview of the UniSUF architecture showing the main entities and update flow. Section 5 details the architecture components, see Figures 15 to 31.

sequence of actions and terminates appropriately. These challenges are com- pounded by the complexity of modeling such systems in formal verification tools such as ProVerif (Blanchet, 2016; Blanchet et al., 2018), which requires a precise representation of the security assumptions and the adversary model.

The challenges associated with the formal security of UniSUF raise the fol- lowing research questions. RQ1: UniSUF has certain secrets, essential for its operation, for example, cryptographic keys and disseminated software. The question is whether UniSUF’s operation might expose any of its secrets.

RQ2: How can we guarantee that the software that UniSUF disseminates is obtained from an authentic source and not manipulated? RQ3: How can we guarantee that in UniSUF, it is impossible to perform a

Software Update With Obsolete Software Versions?

RQ4: Appropriate software updates require a specified order of actions. How can we guarantee that UniSUF’s update operation proceeds orderly? RQ5: How do we know that the software update process always ends?

1.2. Our Contribution

We address the above challenges and research questions by conducting a formal security analysis using symbolic execution in ProVerif. Our key con- tributions to advancing the state of the art are as follows: • We model UniSUF’s architecture (Section 4) and assumptions (Section 3) to reflect real-world automotive systems.

This Model Is Represented In

ProVerif (Section 5) to show the formal satisfiability of essential security properties, including confidentiality, integrity, authenticity, freshness, or- der, and liveness.

• We introduce novel techniques (Section 6) to simulate UniSUF in a sym- bolic execution environment within ProVerif, allowing us to formally ana- lyze critical aspects, such as software authenticity and the correct sequence of operations.

• Through formal proofs and experimental results, we ensure that UniSUF’s update process terminates and follows the correct procedural order. The primary outcomes of our results are as follows.

• A rigorous formulation of UniSUF’s security requirements, emphasizing confidentiality, integrity, authenticity, freshness, order, and liveness in the software update process.

• An open-source ProVerif-based framework to formally verify UniSUF’s compliance with these security guarantees. • Through ProVerif’s symbolic execution environment, we demonstrate that UniSUF can satisfy the proposed security requirements under realistic ad- versary models while considering a system architecture that represents real-world deployment.

Our results show that UniSUF’s architecture effectively prevents attacks, such as secret exposure and replay attacks while ensuring that software updates proceed in the correct sequence and terminate as expected. This demonstrates that UniSUF’s architecture, assumptions, and security require- ments can be formally satisfied, providing strong assurances for its security in real-world deployments (Section 7).

An important clarification concerns the notion of computational cost and scalability. The effort reported in this paper concerns the formal specifica-

5

tion and verification of requirements, rather than the execution of update protocols in deployed vehicles. Consequently, any computational overhead arises exclusively at design time, when symbolic verification tools such as ProVerif analyze the model and proof obligations. These costs depend on model size and tool runtime, but are incurred only once during the verifi- cation process. They do not translate into runtime overhead for the vehicle platform or its backend infrastructure. Moreover, symbolic verification tech- niques, including ProVerif, are conceptually scalable in the sense that they reason over unbounded sessions and adversaries. Our approach, therefore, provides strong security assurances without introducing performance or scal- ability penalties in production systems.

To ensure the reproducibility of our results and to encourage further devel- opment, we pledge to release our solution as open-source upon acceptance of the paper, as detailed in Appendix A.

2. Related Work

Analyzing the security of a complex system requires consideration of po- tential threats. Strandberg et al. (2021b) proposes a security and resilience framework, i.e., Resilient Shield, utilizing a security enhancement methodol- ogy (Strandberg et al., 2018) along with mitigation mechanisms from (Rosen- statter et al., 2020) in light of an analysis of attacks targeting vehicles. Based on the identified attacks, the authors establish security goals and specify the directives required to achieve them. (2023) details specifica- tions for meeting security goals with an emphasis on vehicle software updates.

The authors provide a detailed threat analysis of UniSUF for different threat scenarios, aligned with security goals (Strandberg et al., 2021b), and detailed requirements for the UniSUF architecture (Strandberg et al., 2021a).

2.1. Formal Verification Tools

There are formal verification tools that can either assist or automate proofs. For instance, we can express systems and their properties as logical formulas and use theorem provers such as Coq (Chlipala, 2013) and Isabelle (Wenzel et al., 2008) to either interactively or automatically prove the specified prop- erties. However, formulating the entire implementation of complex systems is tedious and error-prone. Instead, it can be more intuitive to verify a sys- tem based on a formal model using model checkers such as Spin (Holzmann,

6

1997), Uppaal (Behrmann et al., 2006), and TLA+ (Lamport, 2002). Model checkers take a formula and a model and then verify whether the formula holds within the model. The appropriate model checker can simplify the pro- cess of deriving a system model. For example, Uppaal is a model-checking environment that provides both a graphical interface and a modeling lan- guage to model real-time systems (Behrmann et al., 2006), which makes it well suited for time-critical systems.

For our purposes, we also need to model the adversary, to be explicitly de- fined in general model checkers. In contrast, cryptographic protocol verifiers, such as ProVerif (Blanchet et al., 2018), CryptoVerif (Blanchet, 2007), and Tamarin Prover (Meier et al., 2013), are designed to focus on security and im- plicitly incorporate the adversary model. For instance, these cryptographic protocol verifiers verify their models under the assumption of the Dolev-Yao adversary model (Dolev and Yao, 1983). Therefore, cryptographic protocol verifiers are more appropriate for security properties as they eliminate the need to model an adversary.

Wang (2024) provides protocols to attest that the manufacturer has approved vehicle hardware. These protocols enable the replacement of old components with new ones and the attestation of all vehicle components during start- up. Wang Wang (2024) used formal methods to prove the correctness of his protocols. He defined the system model, assumptions, and requirements and used ProVerif (Blanchet et al., 2018) to formally verify that his protocols fulfill the specified requirements given the system model and assumptions.

The work by Wang has been an inspiration for our own research in this area. Basin et al. (2018) used Tamarin Prover to find weaknesses in the Authen- tication and Key Agreement protocol used by 5G. Tamarin Prover has also been used to analyze WiFi Protected Access 2 (Cremers et al., 2020) and Transport Layer Security 1.3 (TLS 1.3) (Cremers et al., 2017). In Bhargavan et al. (2022), an analysis of TLS 1.3 was performed with ProVerif Blanchet et al. (2018), where they also looked at a privacy extension for TLS 1.3 called Encrypted Client Hello.

2.2. Formal Verification of Automotive and IoT Software Update Protocols Several formal methods have been applied to analyze the security of software update mechanisms in automotive and IoT systems. A significant body of work has focused on Uptane, which is a widely adopted framework for se-

7

cure automotive software updates, considered by many in the industry as a de facto standard. For example, Kirk et al. Kirk et al. (2023) develop a Communicating Sequential Processes (CSP) model of the Uptane proto- col together with an attacker inspired by the Dolev–Yao model (Dolev and Yao, 1983), and use the Failures–Divergences Refinement (FDR4) checker to derive exhaustive traces representing potential security violations. These symbolic traces are then translated into executable test cases and run against a reference Uptane implementation on a hardware testbed. Their analysis validated Uptane’s defenses against the modeled threats, but also demon- strated that certain attacks, such as freeze or spoof, become feasible when specific defenses (e.g., expiration checks) are omitted in practice. illustrate how CSP-based refinement and test generation can reveal both specification-level exposures and implementation-dependent weaknesses.

In a complementary study, Lorch et al. (2024) present a comprehensive au- tomated verification of Uptane by combining the Kind 2 infinite-state model checker with the Tamarin cryptographic protocol verifier in an eager com- bination. Unlike prior Uptane analyses that faced state-space explosion or termination issues, their workflow achieves termination in most instances while covering fine-grained message structures. This analysis rediscovered all five previously known vulnerabilities and identified six new ones, all of which were acknowledged by the Uptane standards body.

Their Work Il-

lustrates how combining model checking with cryptographic reasoning can provide both scalability and coverage under diverse adversary capabilities, including multiple key-compromise scenarios.

Another formal analysis of Uptane is provided by Boureanu (2023), who used the Tamarin prover to model version 2.0 of the protocol. Building on the threat model in the Uptane 2.0 standard, this work introduced a hierarchical set of attacker tiers, including compromise of primary or secondary ECUs and of individual repositories. The authors validated a set of security and pri- vacy requirements that go beyond those specified in the standard, including properties such as agreement and temporal correctness. They identified sev- eral flaws that were responsibly disclosed to the Uptane Alliance. While the verification required substantial computational resources, the study demon- strated that symbolic analysis of Uptane 2.0 at scale is feasible and can directly inform improvements to the evolving standard.

Earlier, Mahmood et al. (2020) introduced the first model-based security

8

testing approach for automotive over-the-air (OTA) updates, targeting the Uptane reference implementation. Their framework combined attack trees for threat modeling with an automated tool that generates and executes cor- responding test cases. In a proof-of-concept demonstration, they showed a simulated attack compromising Uptane repositories with malicious firmware.

While this approach provides systematic coverage of known threats, its re- liance on attack trees limits its ability to capture zero-day or composite attacks, motivating later exhaustive analyses based on formal models.

Not all formal verification studies target Uptane; some address other software update protocols or different aspects of the OTA software update process. Ponsard and Darquennes (2021), for instance, apply the Tamarin prover to an IoT-oriented firmware update scheme called UpKit. Their work focuses on proving selected properties, most notably firmware integrity and the freshness of update requests, under a Dolev-Yao adversary. By modeling the crypto- graphic operations and message flows in Tamarin’s rewrite-rule framework, they verify that UpKit meets its targeted requirements, though the analysis does not cover the full range of software update properties.

Other researchers have looked at implementation-level assurance. Mukher- jee et al. (2021) propose an Uptane-based OTA update solution deployed entirely inside a Trusted Execution Environment (TEE) on commercial off- the-shelf embedded hardware (ARM TrustZone). Using SAW, the Software Analysis Workbench, they verify code-level security properties of the Uptane client within OP-TEE and demonstrate the approach on a Raspberry Pi 3B.

Their threat model assumes that the normal-world OS and network may be compromised, while the TEE and server remain trusted. This work high- lights how hardware-enforced isolation can be combined with formal software analysis to strengthen OTA software update implementations.

An earlier foundational effort by Pedroza et al. (2011) introduced a holistic formal methodology for secure OTA updates in vehicles. Their approach ex- tended the AVATAR SysML-based framework to incorporate both security and safety requirements, and integrated formal verification into a model- based development flow. Specifically, AVATAR models of OTA update pro- tocols were translated to ProVerif for symbolic analysis under a Dolev-Yao adversary, while safety aspects were verified using UPPAAL. This allowed properties such as secure authentication, confidentiality, and data integrity of updates to be formally checked already at the design stage. The emphasis

9

was on combining early requirements engineering with formal security and safety verification, thereby demonstrating as early as 2011 the feasibility of security-by-design for vehicular update systems.

Our work on UniSUF diverges from these studies in both goal and approach. Rather than assessing an existing protocol for hidden flaws, we focus on formally specifying a new multi-ECU update framework and verifying that it satisfies a comprehensive set of security requirements by design. We en- code UniSUF’s update procedures in ProVerif and prove, under a standard Dolev–Yao adversary model, that critical properties such as authenticity of the update source, integrity of firmware payloads, confidentiality of sensitive data, and freshness of update commands hold. Ordering is ensured through replay-protection and monotonicity checks, while liveness is argued at the design level rather than mechanically proved. Our verification approach is requirement-driven: each high-level requirement is formalized as a ProVerif query, and the framework is decomposed into interrelated sub-protocols to mirror the modular structure of the UniSUF framework. This decomposi- tion facilitates scalability and clarity. In positioning, UniSUF extends the requirements-oriented perspective already seen in early frameworks such as AVATAR, while differing from vulnerability-focused analyses of Uptane and its implementations (e.g., attack-tree testing, CSP/FDR model-based test- ing, or hybrid model checking with cryptographic reasoning). Taken together with Boureanu’s symbolic proof of Uptane 2.0 and Mahmood’s attack-tree- based framework, these efforts trace the evolution of formal verification for software update protocols, from semi-formal test generation, through sym- bolic and hybrid analyses, to requirements-driven verification by design for new multi-ECU frameworks.

3. Preliminaries

We provide our definitions, assumptions, and requirements.

3.1. System Settings

The system consists of computing entities that interact through communica- tion channels. We assume the system is synchronous and that all entities can access universal time. Every entity has a state, including its variables and all messages in its incoming communication channels. The entities update their states by taking atomic steps. Each step performs an internal computation

10

that takes one time unit. These steps can also receive or send messages. An unbounded sequence of atomic steps, X, denotes an execution. For a given entity E, an execution of E is a subsequence of X from which all steps not taken by E are omitted. Each of our studied problems is solved by a dis- tributed algorithm. The system entities collectively execute an algorithm by individually running a sequence of tasks. Each problem is divided into the sub-problems we analyse in Section 5. The last task in each sequence is the halt task.

3.2. Threat Model

Based on the Dolev-Yao model (Dolev and Yao, 1983), the adversary has com- plete control over the communication between entities. In addition, message interception, injection, and modification are also possible. The adversary may also delay the delivery of the message by a bounded time η; therefore, communication channels are assumed to be reliable but without guarantees of FIFO ordering. This is derived from Wang (2024).

3.3. Cryptographic Primitives, Notations, and Assumptions We assume access to the standard cryptographic primitives in Table 1. We emphasize the requirement for an authenticated symmetric encryption scheme, such as AES-GCM, which ensures that the encrypted data remain confiden- tial and are authenticated to verify the sender (McGrew and Igoe, 2015, Sec.

1). This is necessary because some secrets must be authenticated, such as inputs to the Trusted Execution Environment (Strandberg et al., 2023, Tab. 1)). To simplify our model, we define a certificate as valid if it is signed by the root certificate. For simplicity, we omit the explicit notation of these sig- natures in our cryptographic descriptions, assuming that all valid certificates are implicitly signed. UniSUF operates under the assumption of a trusted root certificate (Strandberg et al., 2021a, 2023). Consequently, we assume that this root certificate is securely pre-installed in the vehicle.

UniSUF assumes secure and reliable communication between entities. This can be achieved, for example, by using SSH (Lonvick and Ylonen, 2006) or mutual TLS (Rescorla, 2018; Campbell et al., 2020). Therefore, adversaries cannot eavesdrop, tamper, or replay messages, with the exception of one link (see Section 5.3.5) for which UniSUF uses reliable non-FIFO commu- nication without security guarantees. UniSUF uses cryptographic materials (see Section 4.1), such as symmetric keys and cryptographic signatures.

11

Table 1: Notations used in the communication schemes. Inspired by Wang (2024, Table 1).

Objkey

Symmetric key of type Obj.

Entity E’S Certificate Is An Asymmet-

ric key pair.

Ecert Is Included In A Data Structure

or message.

Eprivatekey

The private key belonging to ECert.

Epublickey

The public key belonging to ECert.

Message With Epublickey, Thereby

creating CipherText. AsymDec(CipherText, EPrivateKey) Asymmetrically decrypts the given

Recovering

Message.

Message With The Symmetric Key

Key, thereby creating CipherText.

Recovering

Message.

Ing Changed, And Validates If The

ObjKey is used to encrypt Message.

12

Table 1: Notations used in the communication schemes. Inspired by Wang

(2024, Table 1). (Continued)

AuthSymDec(CipherText, ObjKey) Decrypts the CipherText, similar to

Obj′

Key̸ = ObjKey will be detected.

That Message Cannot Be Retrieved

from H.

S With Epublickey Returns H, I.E.,

AsymDec(S, EPublicKey) = H.

Represents Data That Is Signed By

EPrivateKey.

Message || Sign(Hash(Message),

EPrivateKey).

Details May Vary With Different Val-

ues of Obj and args.

The Various Requests Sent Between En-

tities in UniSUF (see Section 5).

Creates A Flag Stating That Item Of

type Obj was successfully initiated.

Model Success Statuses Sent Between

entities in UniSUF (see Section 5).

Ter I. Note That An Item Can Be Any

data.

Items I1 And Up To Ii Are Extracted

from the set of items I.

Tional Dots At The End Signify That

more items left in I are ignored.

3.4. Update Rounds

Where applicable, cryptographic materials are assigned to individual vehicle identification numbers (VIN), vid, and must be distributed within a specified deadline, te (expiration time) (Strandberg et al., 2023; Strandberg, 2024).

The mapping is secured by appending the vid and te to the cryptographic material and signing the resulting data. We use the pair (vid, te) to refer to the software update rounds in UniSUF. We choose the term rounds, rather than sessions, to avoid confusion with the term sessions used, e.g., for SSH (Gasser et al., 2014, Sec. 2). When no vid can be specified, we omit the VIN from our update round notation and use only te.

For a given problem and its algorithm, an execution of an algorithm is de- noted as an update round execution. We assume that message transmissions include an update round identifier. Therefore, entities can learn about new

14

update rounds and associate each execution of their task sequences with an update round. We denote this execution as an entity’s execution of an up- date round, which is a subsequence of the update round execution. We also assume that all entities have a persistent log of all received messages. Each message is identified by the tuple (r, d), where r is the update round identi- fier and d is the cryptographic material in the message. All entities drop any message that is already in the persistent log.

3.5. Problem Definition

We present our requirements for UniSUF, using the goals derived in Sec- tion 1.1. System-level Requirements 3.5.1 to 3.5.6 specify UniSUF at the system level.

The System-level Requirements 3.5.1 to 3.5.3 and 3.5.5 depend on require- ments specified for each UniSUF sub-problem. These requirements are pre- sented in Section 5. Namely, one derives the specifications of UniSUF sub- problems by specifying the sub-problems’ set of secrets (S), the set of cryp- tographic materials (D), the set of procedures ({ℓ1, ℓ2, . . }) that handles cryptographic materials, and the ordering constraints on the procedure invo- cations, which we call the handling partial order (P(ℓ)).

System-level Requirement 3.5.1 (Confidential Secrets). Let X be an up- date round execution and S be the set of secrets in X, which we specify per sub-problem (see Section 5). There is no si ∈S such that an adversary A can obtain si during X.

System-level Requirements 3.5.2 to 3.5.4 consider a set of cryptographic ma- terials D, which we specify for each sub-problem in Section 5. Each element in D is a pair; the first element is the cryptographic material itself, and the second element is the material’s designated origin entity. As certificates are pre-existing cryptographic materials, we state that the origin entity of each certificate is the root CA.

System-level Requirement 3.5.2 requires that the adversary must not manip- ulate the cryptographic materials in D. System-level Requirement 3.5.2 (Integrity of Cryptographic Materials).

UniSUF only uses cryptographic materials created by their designated origin entity, which we specify in Section 5, and is not modified by any other entity.

15

System-level Requirement 3.5.3 considers procedures that handle crypto- graphic materials, such as material production, sending, receiving, validation, and software installation. To safeguard the vehicle during the most critical part of the update process, the vehicle enters offline mode (Strandberg et al., 2021a, 2023; Strandberg, 2024). Additionally, the ECUs are normally locked for security reasons, but must be unlocked to install new software. There- fore, we also classify ECU unlocking and vehicle offline mode activation as handling events.

Let X be an execution of update round r, d (documents) a subset of cryp- tographic materials, and ℓa name of a procedure that handles d in event e(r, d, ℓ) ∈X. In Section 5, we list these procedures per task. We state that e(r, d, ℓ) is a handling event in X. Note that d ⊆D.

System-level Requirement 3.5.3 specifies that cryptographic materials cou- pled with their handling procedures and associated with a specific update round are processed only during that update round; i.e., replays of round unique cryptographic materials between update rounds are not allowed.

System-level Requirement 3.5.3 (Inter-Round Uniqueness). Let e(r, d, ℓ) and e(r′, d′, ℓ′) be handling events during update round executions X and X′, respectively. Suppose (d, ℓ) = (d′, ℓ′). It holds that r = r′.

System-level Requirement 3.5.4 specifies that cryptographic materials cou- pled to a specific update round are only processed once per procedure during that update round. In other words, replays of materials in an update round are not allowed.

System-level Requirement 3.5.4 (Intra-Round Uniqueness). Let X be an update round execution and e(r, d, ℓ) ∈X be a handling event. No event e′(r, d, ℓ) exists in X.

System-level Requirement 3.5.5 specifies that procedures are executed in an order that follows UniSUF’s specification. System-level Requirement 3.5.5 (Integrity of Handling Events). Let X be an update round execution. The occurrences of handling events, e(r, d, ℓ) ∈ X, must follow a handling partial order P(ℓ), which depends only on ℓ, where P(ℓ) is specified per task (see Section 5).

System-level Requirement 3.5.6 prevents non-termination of update rounds, given our system assumptions. The termination is considered timely if all

16

UniSUF entities take the halt task before the update round expires; if not, it is considered late. System-level Requirement 3.5.6 (Termination). All executions of update rounds must terminate.

Using the goals specified in Section 1.1, we discuss how the requirements satisfy the goals. Firstly, G1 and G2 are covered by Confidential Secrets, as we ensure that both the software and the cryptography keys are part of the set of secrets S.

Note That G2 Is Only Partially Covered Because

ProVerif (Blanchet et al., 2018) can only prove that the adversary is unable to learn the secrets and not that each secret is only available to a certain set of entities. Secondly, G3 and G4 are fulfilled by Integrity of Cryptographic Materials because the software and other materials produced by the origin entities are never modified throughout the update process. Thirdly, Inter- Round Uniqueness and Intra-Round Uniqueness together satisfy G5 because any update round that processes the installation of software cannot be replayed to execute previous versions. G6 is fulfilled because any VUUP can only exist in a single update round, and such an update round is directly coupled to a vehicle via the VIN (see Section 3.1). Fourthly, G7 is fulfilled by Integrity of Handling Events, and lastly, G8 is achieved by Termination since this requires that all executions terminate, legitimate or illegitimately.

4. Unisuf Architecture

In this section, we detail the UniSUF architecture and its functionalities.

4.1. Cryptographic Materials

As detailed in Table 2 and previously mentioned in Section 3.3, UniSUF uses different cryptographic materials. The signing process is shown in Figure 2. Table 2: UniSUF cryptographic materials, sorted in alphabetical order.

17

Figure 2: Different cryptographic materials in UniSUF are shown, each with its respective key. Figure derived from Strandberg et al. (2021a, Fig. 3). Table 2: UniSUF cryptographic materials, sorted in alphabetical order.

(Mkm)

MKMSecurityAccess || MKMSoftware || . .

Secure Key Array (Ska)

SKASecurityAccess || SKASoftware || . .

18

Table 2: UniSUF cryptographic materials, sorted in alphabetical order.

Securityaccesskey1, Mkmsecurityaccesskey)

|| . .

Mkmsoftwarekey)

|| . .

Description

UniSUF uses Vehicle Unique Update Packages (VUUP) to install vehicle updates. A VUUP is an update package produced by UniSUF for a specific vehicle. It contains all the necessary cryptographic keys, certificates, and instructions for the software update. The internal structure of a VUUP file is shown in Figure 3. The VUUP does not contain the actual software files; instead, Download Instructions are included to specify where software files can be downloaded. The specific implementation of Download Instructions is unspecified but can be seen as URLs to the software update files. Note

19

that the Download Instructions is encrypted by a unique session key coupled to its update round. This key is retrieved from the Download Instruction Key Manifest (DKM).

As shown in Figure 4, a key manifest consists of a symmetric session key that has been asymmetrically encrypted, accompanied by a policy defining the key’s usage (see DKM, IKM, and MKM). Note that the UniSUF term session is equivalent to update rounds (see Section 3.4). In Table 2, none of the key manifests are signed, to remain consistent with the notation used by Strandberg et al. (2021a). However, when the key manifests are trans- mitted during tasks (see Section 5), all key manifests are signed with the certificates according to Figure 2.

Additionally, a VUUP includes Installation Instructions encrypted by the session key from the Installation Instruction Key Manifest (IKM). The In- stallation Instructions contains the diagnostic instructions for installing soft- ware, the Master Key Manifest (MKM), and the Secure Key Array (SKA), as shown in Table 2. To guide task-specific requirements of Confidential Secrets (see System-level Requirement 3.5.1), we define the notations MKMKey and SKAKey to refer to all keys in MKM and SKA respectively.

Thus, the DKM and IKM session keys are packaged into key manifests (i.e., a master key plus a policy). In contrast, the MKM can contain multiple master keys, whereas the DKM and IKM each contain only one.

Strandberg (2024) defines encased software as software that undergoes a multi-layered protection process.

Initially, The Software Is Signed By The

software supplier to ensure its integrity and authenticity. Next, as part of UniSUF, it is encrypted to ensure confidentiality.

Finally, The Encrypted

software is secured with an additional signature, ensuring that the encrypted package can be validated to avoid initiating the decryption process in case of validation failure. The word encased should not be mixed up with the term encapsulated used by Strandberg et al. (2021a) to represent materials contained in the VUUP file.

UniSUF uses the term category to classify master keys based on purpose, such as decrypting software files, or unlocking ECUs to enable update capabilities. The Vehicle Signed Order (VSO) is a readout per vehicle that contains de- tailed information about the vehicle, such as the onboard software versions.

UniSUF uses this information and the latest available software versions to

20

Figure 3: Internal structure of a VUUP file.

The Blue Items Are Used In The

download process, while the green ones are used for the installation process. Note that the VUUP content has been signed by V CMCert. The figure is derived from Strandberg et al. (2021a, Fig. 3).

construct a software list containing the software files and configurations for a specific and vehicle unique software update. Download Instructions and Installation Instructions are then created based on the software list.

The software itself is located in external sources and not present in the ac- tual VUUP file. The software files are signed by the software suppliers and associated with version numbers to prevent installations of older software ver- sions (Strandberg, 2024). UniSUF validates the supplier signature, further encrypts the software, and appends another signature. Finally, the signed encrypted software is uploaded to the software repository.

4.2. System Entities

As shown in Figure 5, UniSUF consists of three entities: Producer, Con- sumer, and the Software Repository (Strandberg et al., 2023, Sec. 4). Addi- tionally, UniSUF interacts with external entities, such as Software Suppliers and ECUs (Strandberg, 2024). UniSUF uses redundant entities and interacts with multiple Software Suppliers and vehicles with multiple ECUs (Strand- berg et al., 2021a, 2023). However, for our proof, we consider a simplified system in which each vehicle has exactly one Consumer and one ECU. Ad- ditionally, all vehicles communicate with exactly one Producer and one Soft- ware Repository, and there exists only one Software Supplier.

4.2.1. Software Repository

The UniSUF Software Repository is an entity that represents multiple dis- tributed repositories (Strandberg et al., 2021a), mainly responsible for soft-

21

Figure 4: Different cryptographic materials in UniSUF and how they are encrypted. Figure derived from Strandberg et al. (2021a, Fig. 2). ware storage, where each software file is associated with a specific download URL. However, in offline cases, the software can also be stored on Network- Attached Storage (NAS) or a USB stick Strandberg (2024).

4.2.2. Producer

Strandberg et al. (2021a) define the Producer as a collection of different sub-entities responsible for producing and securing software update pack- ages. The Producer is also responsible for disseminating software to different storage repositories. As shown in Figure 6, UniSUF has the following 12 producer entities (cf. (2021a), Table 1).

• Producer Local Secure Storage – Stores software files received from software suppliers. • Version Control Manager (VCM) – Coordinates the producer entities and finalizes the creation of the VUUP file for a specific vehicle.

• Producer Signing Service (PSS) – Produces signatures on behalf of other entities. • Cryptographic Material Storage (CMS) – Securely stores crypto- graphic materials, such as keys for decrypting software or unlocking ECUs,

22

Figure 5: Diagram of all the entities and their communication in UniSUF. Dotted arrows denote communication channels between entities from different modules. The black arrows denote secure communications, while the sole red arrow denotes an insecure communication link.

as well as certificates. • Producer Security Agent (PSA) – Generates session keys and retrieves additional keys from the CMS, such as keys for unlocking ECUs, perform- ing privileged diagnostic requests, and decrypting software. These addi- tional keys are further encrypted with session keys, which are, in turn, encrypted using a vehicle-specific public certificate.

• Database – Store URLs to software files located in software repositories. • Order Cloud Service – Stores the Vehicle Signed Order (VSO) in a queue and URLs to VUUP files.

• Order Agent (OA) – Verifies the validity of incoming VSOs and starts the updating process by forwarding the request to the Version Control Manager (VCM).

• Producer Download Agent (PDA) – Creates download instructions from the software list received from VCM. Later in the process, the down- load instructions are encrypted, signed, and sent to VCM.

• Producer Installation Agent (PIA) – Creates installation instructions from the software list received from VCM. The installation instructions are bundled with cryptographic material, encrypted, signed, and sent to VCM.

23

Figure 6: The communication flow between the Producer entities. Dotted arrows denote communication channels between a Producer entity and a non-Producer entity.

• VIN Database (VD) – Stores data about unique vehicles and software versions. • Vehicle Cloud Service – Stores the VUUP files and VCM certificates that can be downloaded by the Consumer via a VUUP URL.

4.2.3. Consumer

The Consumer is the Producer’s counterpart and is responsible for decap- sulating the VUUP and the processing of the download and installation in- structions (Strandberg et al., 2021a, Sec. 4.2). UniSUF has the following four Consumer entities as shown in Figure 7.

• Consumer Local Storage – Stores signed VUUP, and signed and en- crypted software files. • Consumer Download Agent (CDA) – Executes the download instruc- tions and retrieves software from software repositories.

• Consumer Security Agent (CSA) – Provides a trusted execution envi- ronment where, e.g., decryption can occur in an isolated and secure space. • Consumer Installation Agent (CIA) – Executes the installation in- structions and then streams the decrypted software to the unlocked ECUs with the help of CSA.

24

Figure 7: The communication flow between the Consumer entities is denoted by the solid arrows. Dotted arrows denote communication between a Consumer and a non-Consumer entity. The red arrow denotes an insecure communication channel.

All other channels are secure.

4.2.4. Software Suppliers

Software suppliers create and deliver software to the Producer for the instal- lation in different vehicles (Strandberg et al., 2021a, Sec. 3.3). The software suppliers also sign their software to provide authenticity. We assume a sim- plified model that considers a single software supplier supplying software to a single ECU (see Section 4.2.5).

4.2.5. The Electronic Control Unit

An Electronic Control Unit (ECU) is a vehicle computer responsible for var- ious tasks, from simple signal processing to more advanced functionality, for instance, an infotainment system running various applications. For our sim- plified model, we assume a system with only one ECU. The ECU is first unlocked and put in programming mode by using security access and a se- cret key (Strandberg et al., 2021a, Sec. 4.2), to allow the ECU to receive and install software with Unified Diagnostic Services (UDS) (Strandberg, 2024;

4.2.6. Adversary

As shown in Figure 8, the adversary is based on the Dolev-Yao model, as- suming an adversary with access to the communication channels.

25

The adversary is actively present on all communication links in the system. However, most of these links, except the one depicted in red, are secure and reliable communication channels; that is, the adversary cannot interfere, according to Dolev-Yao. The one exception is the link between the Consumer and the ECUs, which is a reliable but not a secure communication channel, where the adversary can potentially read, modify, delete, or insert messages.

Figure 8: The illustration depicts the presence of adversaries on the high-level UniSUF architecture shown in Fig. 1, where the adversaries are represented by the red devils.

4.3. Modelling Unisuf

This section explains the modeling of entities and their respective executions in UniSUF.

4.3.1. Execution Of System Entities

Each system entity runs a sequence of tasks for a given problem. The entity running the initial user-invoked task is called the initiator; illustrated in Figure 9. All other entities are listeners (see Figure 10) since their first task is the listening task.

This task listens for an initiation message specified for each listener. The listening task invokes the next task in sequence and a new listening task, enabling concurrent executions of the task sequence.

We divide listeners into two categories: a passive listener that will wait for an initiation message and an active listener that will request an initiation message.

26

Figure 9: The initial user-invoked task begins an execution of the initiator entity’s tasks. The initiation tasks are marked with the symbol of a hand pressing a button. Figure 10: The listening task invokes a copy of itself to continue listening on a new execution. It also begins an execution of the listening entity’s tasks. The listening tasks are marked with a symbol of an ear.

4.3.2. Lifecycle Of Update Rounds

An update round execution begins when the round identifier is created during the initiation task. Throughout this round, listener entities start executing once their listening task receives a message containing the round identifier.

As shown in Figures 11 and 12, an entity maintains a context for each up- date round. This context contains the update round identifier and the cryp- tographic materials (see Section 4.1) used throughout the execution of the round. The context is passed along the task sequence and can be updated by each task.

Each update round identifier encodes its expiration time and when such expiration occurs, all entities halt their local execution of the update round, by removing the context associated with the round and ignoring any further messages related to that round. The update round is terminated once all

27

Figure 11: The figure illustrates an example of executing an initiator entity’s task sequence. For each task, we also show what the context can contain. Figure 12: The figure illustrates an example of an execution of a listening entity’s task sequence.

entities have halted their execution of the update round. 4.3.3. Passing Contexts Across Segments of Task Sequences We divide the main problems into sub-problems, where each sub-problem uses a subset of the system entities. In Figure 13, sub-problem 1 uses the initiator and listener entity 1. Figure 13 shows that an entity’s task sequence can be segmented so that each segment belongs to a single sub-problem. For example, listener entity 1’s task 3 and halt task form a segment that belongs to sub-problem 2.

When an entity starts working on a sub-problem for an update round, it possibly already has an update round context. For instance, if the entity has previously participated in other sub-problems for the same update round,

28

Figure 13: The execution of an example problem. This problem considers three entities, whereas one is the initiator entity. The problem is divided into three sub- problems.

i.e., it has previously run either the initiation task or listening task for the same update round. Figure 14 shows that listening entity 2 has a context at the start of the sub- problem since it starts on task 2, i.e., it has previously run the listening task.

The other listener, listener entity 1, does not start with any context, since it first needs to run its listening task at the start of the sub-problem. Once a segment’s execution finishes, the last context of this segment is passed to the next segment as the starting context. Therefore, we identify which entities have previously executed task segments in the same update round for a given sub-problem. For these entities, we specify the cryptographic materials present in their starting contexts (see Section 5).

4.3.4. Well-Known Addresses Of Unisuf Entities

We assume that all consumer entities, as defined in Section 4.2.3, are aware of the specific Vehicle Identification Number (VIN) of the vehicle they occupy. Each vehicle has a pre-stored public vehicle certificate containing metadata, including VIN-related information Strandberg (2024).

29

Figure 14: Example of two entities solving a sub-problem together. The figure also shows how each task in the entities is connected to a context. Additionally, we assume that all entities in UniSUF know each other’s ad- dresses, e.g., through existing protocols, such as DNSSEC, enabling entities to securely obtain IP addresses from domain names Van Adrichem et al.

(2014).

5. Sub-Problems

From the UniSUF specifications (Strandberg et al., 2021a), we analyse two problems: the software preparation and the software update. The software preparation process (cf. Section 5.1) involves safeguarding software received from suppliers, ensuring the software’s confidentiality and authenticity for it to be securely incorporated into future vehicle updates. Additionally, the software update is further divided into the encapsulation and the decapsu- lation stages (cf. Sections 5.2 and 5.3) emphasizing securely updating ve- hicular software and configurations. Strandberg et al. (2021a) specifies an additional stage after decapsulation: the post-state. The post-state encom- passes installation reports and logs, potentially affecting upcoming software updates. However, we do not consider the post-state in our simplified model.

Consequently, the main tasks in UniSUF are dissected into sub-problems, based on the steps provided by Strandberg et al. (2021a), where each sub-

30

problem, has a description, a diagram depicting its algorithm, a communica- tion scheme, and assumptions and requirements.

5.1. Preparation

An overview of the entities involved in the preparation stage and their com- munication links can be seen in Figure 15. In the preparation stage, software supplier files are processed before being used for software updates Strandberg et al. (2021a). We have divided this stage into two sub-problems: the Secure Software Files and the Upload Soft- ware Files. The focus of the first sub-problem is the encrypting and signing of the software, whereas the second sub-problem handles the software upload and the creation of software URLs.

The preparation stage manages both software files applicable to multiple vehicles and unique files for specific vehicles Strandberg (2024). In our model, we assume the case when software is being prepared for multiple vehicles and we additionally assume that the update round is solely identified by the expiration time te (see Section 3.4).

Figure 15: An overview derived from (Strandberg et al., 2021a, Sec.

3.3) For

the communication between all entities involved in the preparation stage further divided into two sub-problems.

5.1.1. Step 1–4: Secure Software Files

The initial phase of the update process focuses on securing software files (see Figure 16 and Table 3). The software supplier signs the software files before sending them to local storage on the producer side. VCM validates the signature and encrypts the software using a symmetric key obtained from PSA; this key is referred to as SoftwareKey. The encrypted software is then signed with the VCM certificate to finalize the SoftwareEncapsualted assembly.

31

Figure 16: Diagram of the sub-problem Secure Software Files. S ={Software, SoftwareKey, SupplierPrivateKey, V CMPrivateKey} D ={(Software, Supplier), (SoftwareKey, PSA), (SoftwareHash, V CM),

(Signedsoftwarehash, Pss)}

To derive the specific sub-problem requirements from the system require- ments (see Section 3.5), we define S, D and the partial order P(ℓ) = ℓi < ℓi+1

For 1 ≤I ≤4 With The Following Labels:

ℓ1: The software suppliers upload the software to Producer Local Storage. ℓ2: PSA generates the software key. ℓ3: VCM generates a hash of the software.

ℓ4: PSS generates a signature for the software. ℓ5: VCM assembles SoftwareEncased.

5.1.2. Step 5–6: Upload Software Files

Once the software file has been encased, it is uploaded into a software reposi- tory. The repository then generates a URL to the uploaded encased software

V Cmprivatekey)

Table 3: Communication scheme for the sub-problem Secure Software Files. The dashed line represents parallel processes. and returns this URL to VCM (see steps 5.1 and 5.2 in Figure 17 and Ta- ble 4). Finally, the VCM stores the software URL in the VIN database and stores the SoftwareKey in CMS; used for the encryption of software files.

Note that VCM has a starting context because its initiation task is in a previous sub-problem (see Section 5.1.1). VCM’s starting context contains SoftwareEncased and SoftwareKey.

Success(Softwarekey)

Table 4: Communication scheme for the sub-problem Upload Software Files.

33

Figure 17: Diagram of the sub-problem Upload Software Files. S ={Software, SoftwareKey, SupplierPrivateKey, V CMPrivateKey}

For 1 ≤I ≤3 With The Following Labels:

ℓ1: Software Repository receives the SoftwareEncased. ℓ2: VIN Database stores the SoftwareURL. ℓ3: CMS stores the Softwarekey.

ℓ4: VCM receives status of Softwarekey being stored in CMS.

5.2. Encapsulation

The encapsulation stage starts when the Order Agent has received an or- der request from CDA, whereafter producer entities work collaboratively to produce a VUUP (Strandberg et al., 2021a, Sec. 4.1). Figure 18 shows a high-level flow diagram of the different sub-problems involved in the encap- sulation stage. In steps 1–2, the encapsulation stage starts by producing a VSO, which is later processed to a Software List in step 3. Furthermore, in steps 4–7, the Software List is sent to PDA, PIA, and PSA to gener- ate necessary materials, for instance, download and installation instructions.

Instructions and other materials are included in a VUUP file (step 8), where- after the encapsulation stage finalizes by notifying the consumer that updates are available (cf. steps 9–11).

Figure 18: Overview of communications between all entities that are involved in the encapsulation stage.

5.2.1. Step 1–2: Order Initiation

The encapsulation process begins when the CDA requests an update by send- ing a signed order (denoted as VSO) to the Order Cloud Service (see steps

35

1.1–1.3 in Figure 19). In step 1.4, Order Cloud Service stores the order in a queue, whereafter the Order Agent attempts to fetch an order from this queue. If an order is available, Order Cloud Service sends a VSO to Order Agent, which verifies the signature and initiates VCM using the VSO (steps 2.1–2.4).

Figure 19: Diagram of the sub-problem Order Initiation.

[V So]Consumer

Table 5: Communication scheme for the sub-problem Order Initiation. To derive the specific sub-problem requirements from the system re-

=

{(V SO, CDA)}, and the partial order P(ℓ) = ℓi < ℓi+1 for 1 ≤i ≤4

36

ℓ1: CDA generates a signed VSO. ℓ2: Order Cloud Service stores the signed VSO in its queue. ℓ3: Order Agent pulls signed VSO from Order Cloud Service.

ℓ4: Order Agent initiates VCM with the signed VCM. ℓ5: VCM sends status on initialisation.

5.2.2. Step 3: Create Software List

Given a VSO, the VCM will produce a software list (see step 3.1–3.5 in Figure 20). The software list contains the software to be installed in the vehicle. After creating the software list, it is transmitted to the PIA, PSA, and PDA for further processing (step 3.6).

The Software List Is Used To

generate the download and installation instructions. The entity VCM has a starting context because its listening task has been included in the previous sub-problem Order Initiation (see Section 5.2.1).

The starting context of VCM contains the signed VSO. Figure 20: Diagram of the sub-problem Create Software List.

V Indata ∥Softwarev Ersions)

Table 6: Communication scheme for the sub-problem Create Software List.

S ={Cdaprivatekey, V Cmprivatekey}

D ={(V SO, CDA), (SoftwareList, V CM), (V INData, V INDatabase),

(Softwarev Ersions, V Indatabase)}

To derive the specific sub-problem requirements from the system require- ments (see Section 3.5), we define S and D as seen above, and the partial order P(ℓ) = {ℓ1 < ℓ2, ℓ2 < ℓ3, ℓ2 < ℓ4, ℓ2 < ℓ5, ℓ3 < ℓ6, ℓ4 < ℓ6, ℓ5 < ℓ6}.

In other words, ℓ1 happens before ℓ2 happens, which then precedes ℓ3, ℓ4, and ℓ5 occurring in parallel, and finally ℓ6 happens last. ℓ1: VCM obtains the most up-to-date software versions and vehicle data from VIN Database.

ℓ2: VCM creates a signed Software List. ℓ3: VCM sends the signed Software List to PDA. ℓ4: VCM sends the signed Software List to PIA.

ℓ5: VCM sends the signed Software List to PSA. ℓ6: VCM receives status of Software List being sent to PDA, PIA and PSA.

5.2.3. Step 4: Create Download Instructions

Based on the Software List received from the VCM in the previous sub- problem Create Software List (see Section 5.2.2), PDA creates the Download

38

Instructions (see steps 4.1–4.2).

The Download Instructions Is Encrypted

using a generated session key. The session key is then used to produce the key manifest DKM (steps 4.3–4.10). This sub-problem finishes by signing the Download Instructions and DKM (steps 4.12–4.16).

The entities PDA and PSA have starting contexts because their listening tasks have been included in a previous sub-problem (see sub-problem Create Software List). The starting context of PDA contains the signed Software List and V CMCert.

Figure 21: Diagram of the sub-problem Create Download Instructions. S ={SoftwareList, DownloadInstructions, DKMKey, RootPrivateKey,

Pdaprivatekey, V Cmprivatekey}

D ={(SoftwareList, V CM), (DownloadInstructions, PDA), (DKMKey, PSA), (V ehicleCert, Root), (PDACert, Root),

(Dkm, Pda)}

To derive the specific sub-problem requirements from the system require- ments (see Section 3.5), we define the sets S and D as seen above, and the partial order P(ℓ) = ℓi < ℓi+1 for 1 ≤i ≤10 with the following labels:

Sign(Hash(Dkm), Pdaprivatekey)

Table 7: Communication scheme for the sub-problem Create Download Instruc- tions.

ℓ6: Pda Generates Dkm

ℓ7: PSS generates a signature for the Download Instructions ℓ8: PSS sends the signed encrypted Download Instructions to PDA

5.2.4. Step 6: Generate Installation Materials

In parallel to the creation of Download Instructions and Installation Instruc- tions (see Sections 5.2.3 and 5.2.5), the PSA generates and secures cryp- tographic materials necessary for the installation of software updates, e.g.,

40

SKA and MKM. For instance, ECU keys for the unlocking of ECUs, to gain extended privileges. The entities PSA, PSS, and CMS have starting contexts because their listen- ing tasks have been included in previous sub-problems (see sub-problem Cre- ate Download Instructions). PSA’s starting context contains the signed Soft- ware List and V CMCert and CMS’s starting context contains the V ehicleCert.

Figure 22: Diagram of the sub-problem Generate Installation Materials.

Sign(Hash(Mkm), Psaprivatekey)

Table 8: Communication scheme for the sub-problem Generate Installation Mate- rials.

V Cmprivatekey}

D ={(SoftwareList, V CM), (V ehicleCert, Root), (PSACert, Root),

(Mkm, Psa), (Ska, Psa)}

To derive the specific sub-problem requirements from the system require- ments (see Section 3.5), we define the sets S and D as seen above, and the partial order P(ℓ) = ℓi < ℓi+1 for 1 ≤i ≤9 with the following labels:

ℓ9: Pss Sends The Signed Mkm To Psa

5.2.5. Step 5 and 7: Create Installation Instructions The PIA receives Software List from VCM and creates Installation Instruc- tions based on the Software List (see steps 5.1–5.2 in Figure 23). Similarly to sub-problem Create Download Installation, the Installation Instructions are encrypted with a generated session key, which gives rise to the IKM (steps 7.1–7.11). The Installation Instructions is also appended with the materials generated in the sub-problem Generate Installation Materials (steps 7.1–7.3).

The entities PIA, PSA, PSS, and CMS have starting contexts because their listening tasks are included in previous sub-problems (see sub-problems Cre- ate Software List and Create Download Instructions). PIA’s starting context contains the signed Software List and V CMCert, PSA’s starting context con- tains the signed SKA and signed MKM, and CMS’s starting context contains the V ehicleCert.

42

Figure 23: Diagram of the sub-problem Create Installation Instructions. S ={SoftwareList, InstallationInstructions, IKMKey, RootPrivateKey,

Piaprivatekey, V Cmprivatekey}

D ={(SoftwareList, V CM), (InstallationInstructions, PIA), (IKMKey, PSA), (V ehicleCert, Root), (PIACert, Root),

(Mkm, Psa), (Ska, Psa)}

To derive the specific sub-problem requirements from the system require- ments (see Section 3.5), we define the sets S and D as seen above, and the partial order P(ℓ) = ℓi < ℓi+1 for 1 ≤i ≤11 with the following labels:

ℓ7: Pia Generates Ikm

ℓ8: PSS generates signature for the Installation Instructions

Sign(Hash(Ikm), Piaprivatekey)

Table 9: Communication scheme for the sub-problem Create Installation Instruc- tions. ℓ9: PSS sends the signed encrypted Installation Instructions to PIA

5.2.6. Step 8: Package The Instructions

Once the required materials for software update have been created, the ma- terials need to be inserted into the VUUP file. The procedure starts with PDA and PIA sending data to VCM (see steps 8.1–8.2 in Figure 24). Be- fore data is packaged into VUUP content, signatures are validated to ensure authenticity (steps 8.3–8.8). The VUUP file is signed by the PSS and later uploaded to the cloud (steps 8.9–8.14).

The entities PDA, PIA, VCM, CMS, and PSS have a starting context because their listening tasks are included in previous sub-problems Order Initiation (see Sections 5.2.2 to 5.2.5). PDA’s starting context contains the encrypted

44

and signed Download Instructions and the signed DKM, and PIA’s starting context contains the encrypted and signed Installation Instructions and the signed IKM.

Figure 24: Diagram of the sub-problem Package the Instructions. Steps marked with * can occur in parallel. S ={V ehiclePrivateKey, RootPrivateKey, PDAPrivateKey, PIAPrivateKey,

Psaprivatekey, V Cmprivatekey, Dkmkey, Ikmkey}

D ={(V UUPURL, V ehicleCloudService), (V UUP, V CM), (DownloadInstructions, PDA), (InstallationInstructions, PIA), (PDACert, Root), (PIACert, Root), (V CMCert, Root)} For any execution of this sub-problem, the entities PDA, PIA, VCM, CMS, and PSS are aware of which update round it belongs to since these entities have been in the same update round in sub-problems Order Initiation and

Authors:

Peder EZ Larson 1, 2,* , Jenna ML Bernard1, James A Bankson 3, Nikolaj Bøgh 4, Robert A Bok1, Albert P. Chen 5, Charles H Cunningham 6,7, Jeremy Gordon1, Jan-Bernd Hövener 8, Christoffer Laustsen 4, Dirk Mayer 9,10, Mary A McLean11 12, Franz Schilling13, James Slater1, Jean-Luc Vanderheyden5, 14, Cornelius von Morze 15, Daniel B Vigneron1, 2, Duan Xu1, 2, and the HP 13C

94143, Usa.

Denmark. 5 GE Healthcare, Menlo Park, California, USA. 6 Physical Sciences, Sunnybrook Research Institute, Toronto, Ontario, Canada.

8 Section Biomedical Imaging, Molecular Imaging North Competence Center (MOIN CC), Medicine, Baltimore, MD, USA. Cambridge, United Kingdom.

14Jlvmi Consulting Llc, Dousman, Wi, Usa

#See Acknowledgements for a list of all HP 13C MRI Consensus Group Members This work was supported by the ISMRM Hyperpolarized Media MR Study Group, the ISMRM Hyperpolarization Methods & Equipment Study Group, and the Hyperpolarized MRI Technology Resource Center (NIH/NIBIB grant P41EB013598).

Abstract

MRI with hyperpolarized (HP) 13C agents, also known as HP 13C MRI, can measure processes such as localized metabolism that is altered in numerous cancers, liver, heart, kidney diseases, and more. It has been translated into human studies during the past 10 years, with recent rapid growth in studies largely based on increasing availability of hyperpolarized agent preparation methods suitable for use in humans. This paper aims to capture the current successful practices for HP MRI human studies with [1-13C]pyruvate - by far the most commonly used agent, which sits at a key metabolic junction in glycolysis. The paper is divided into four major topic areas: (1) HP 13C-pyruvate preparation, (2) MRI system setup and calibrations, (3) data acquisition and image reconstruction, and (4) data analysis and quantification. In each area, we identified the key components for a successful study, summarized both published studies and current practices, and discuss evidence gaps, strengths, and limitations. This paper is the output of the “HP 13C MRI Consensus Group” as well as the ISMRM Hyperpolarized Media MR and Hyperpolarized Methods & Equipment study groups. It further aims to provide a comprehensive reference for future consensus building as the field continues to advance human studies with this metabolic imaging modality.

Keywords: Hyperpolarized MRI, metabolic imaging, carbon-13, pyruvate, dissolution dynamic

Introduction

MRI with hyperpolarized 13C agents, also known as hyperpolarized (HP) 13C MRI, has shown great potential as a novel imaging modality, particularly for its ability to probe metabolic processes in real time. The first human studies with HP [1-13C]pyruvate were performed in 2011 in prostate cancer patients (1).

Since then, there have been over 60 papers published with imaging results of human subjects from 13 different sites, with applications including prostate cancer, brain tumors, breast cancer, kidney cancer, pancreatic cancer, metastatic disease, liver disease, ischemic heart disease, diabetes and cardiomyopathies. The vast majority of these studies used [1-13C]pyruvate (1–63), where [2-13C]pyruvate (64) and 13C-urea (56) have been demonstrated too.

As clinical HP 13C MRI advances, there is a growing need to build consensus for best practices, which are critical for comparing data across sites, performing multi-site trials,deploying methods to new sites, partnering with vendors, and potentially for obtaining broader regulatory approvals.

In March 2022, we initiated an effort to build consensus within the HP 13C MRI community with this opportunity in mind, and it was greeted with strong enthusiasm. The “HP 13C MRI Consensus Group”, containing over 55 members from 27 sites, identified the area of greatest need and opportunity for consensus building to be HP [1-13C]pyruvate human

●

Pyruvate is the most mature and widely used HP agent and has the most significant translational evidence emphasizing the potential clinical impact.

●

Clinical trials, particularly multi-site trials, have the strongest need for consensus methods to ensure that data can be combined across sites. This work is a Position Paper for which the goal is to describe current successful practices and study methods for HP [1-13C]pyruvate human studies along with justification to support those practices. This is divided into four major topic areas: (1) HP 13C-pyruvate preparation, (2) MRI system setup and calibrations, (3) data acquisition and image reconstruction, and (4) data analysis and quantification (Fig. 1). The current successful practices and study methods include a literature review of published peer-reviewed journal papers showing human HP [1-13C]pyruvate study data, up to September 2022 (1–63), as well as new unpublished information from surveys of HP 13C study sites. Based on this information, we also highlight the evidence gaps, strengths, and limitations of current practices which are summarized at the end of each section.

Figure 1: Illustration of the HP 13C MRI human study process, including the 4 major areas covered in this paper: Hyperpolarized 13C-pyruvate preparation, MRI system setup and calibration, Acquisition and Reconstruction, and Data Analysis and Quantification.

Figure 2: Anatomical targets of HP [1-13C]pyruvate MRI human studies published up to September 2022.

Hyperpolarized 13C-Pyruvate Preparation

This section covers the processes for creating the HP agent, 13C pyruvate, and will include many aspects and considerations that are needed to safely and effectively prepare doses for metabolic imaging studies in human subjects. These include material, personnel, equipment and facility, fluid path preparation, quality control, and release.

It is helpful to understand that the specifications of a dose of 13C pyruvate suitable for in vivo MR HP metabolic imaging were shaped in part by early preclinical studies performed by GE HealthCare summarized in Ref. (65). In short, the safety of the two novel drug components, 13C pyruvate and the electron paramagnetic agent (EPA) AH111501, were demonstrated in those studies. The more precise formulation of the dose suitable for human use was then determined from clinical studies (66) that included two Phase 1 clinical trials in young and elderly healthy volunteers without hyperpolarization of the 13C nuclei and another Phase 1/2a dose escalation and imaging feasibility study with HP 13C pyruvate in 31 prostate cancer patients at the With the exception of the first HP 13C imaging clinical trial, which utilized a prototype device in a cleanroom (1), all HP 13C studies performed in humans to date have utilized the SPINlab polarizer (manufactured by GE HealthCare). Consequently all doses of the HP 13C pyruvate delivered by SPINlab have been produced using the “SPINlab Pharmacy Kit” that serves as the container-closure system for the various drug components (13C pyruvic acid and EPA mixture, dissolution medium, and neutralization and dilution medium) during sample polarization, dissolution and quality control (QC) processes. Thus many aspects of the HP sample preparation considerations discussed below are related to the SPINlab instrument and the consumables designed to be used with it (67).

General Considerations

While more than 860 patients or healthy subjects having been injected with HP 13C pyruvate as of January 2022 without reports of any serious adverse events (68), HP 13C pyruvate injection remains an investigational MR contrast agent and can only be administered by those with Investigational New Drug (IND) exemption from the Food and Drug Administration (FDA) in the USA, a Clinical Trial Application (CTA) in Canada, approval from National Research Ethics Committee Services in the UK, or approval from the relevant local regulatory body. Thus, methods and processes involved to produce a dose should have patient safety as the first priority. Since utilizing dissolution dynamic nuclear polarization (dissolution-DNP) for human use is still a relatively new development, there are no existing published regulatory guidelines specifically for this method.

There are two major production styles that determine how various sites approach the agent preparation. In the US, the most common approach is to rely on a sterilizing filter (“Terminal Sterilization”) to ensure sterility of the final product, akin to PET tracer production, where a starting molecule with a radioisotope is processed using various other ingredients to make the final, desired and injectable contrast agent within a necessarily short amount of time (69). For these sites, sterilization of the components and accessories upstream of this filter are not required, although many of them were manufactured and tested following Good Manufacturing Practice (GMP) or Good Laboratory Practice (GLP) requirements. The filling process is usually performed under an ISO 5 laminar flow hood, but a clean room or an isolator is not required.

This approach is typically accompanied by testing the integrity of the sterilizing filter prior to release of the dose for injection. Typically, post release endotoxin and sterility tests are performed using an aliquot reserved from each released dose.

In the UK and EU, the most common approach is to more-closely follow sterile pharmaceutical compounding guidelines (70), where all components and ingredients are required to be sterile or manufactured under GMP guidelines and are assembled and filled within a clean room environment or an isolator system (“Sterile Preparation”). Typically a batch of Pharmacy Kits for HP 13C pyruvate injection are prepared together. The sterility of the final dose is also ensured by batch validation testing, in addition to the sterility of the ingredients and the sterile compounding process. The endotoxin and sterility testing are performed for the process validation but are not performed for each injected dose.

Some institutions fill and assemble the Pharmacy Kit required for a specific study on the same day or the day prior to polarization, dissolution, and patient administration, but others have also demonstrated the feasibility of preparing a batch of kits, keeping them in a -20ºC freezer and using them over a period of a few months.

Beyond the obvious requirements that the process and the facility has to ultimately produce a dose that is safe to inject into a human, regulatory authorities will also focus on the question “Are you in control of your processes?”. To be in control of your process requires an in-depth and broad understanding of all processes involved in pre, post, and during the production process.

Personnel

It is typical and may be required to have licensed personnel involved in the production process depending on local regulations.Typically a pharmacist, radiopharmacist or other similarly qualified person (QP), in charge of the facility where the Pharmacy Kit filling and preparation is taking place, is responsible for the overall process and the release of the injectable dose.

Qualified cleanroom technicians are often involved in the Pharmacy Kit filling under the supervision of the pharmacist or QP. As is required for pharmaceutical compounding or PET tracer production, training requirements and training records for all personnel need to be maintained and available for audit by the FDA or equivalent.

Equipment And Facility

The facility and all equipment need to have standard operating procedures (SOPs) that describe how equipment is used, maintained, and calibrated to comply with relevant legislation. Currently, almost all the filling of the Pharmacy Kit takes place within a compounding laminar flow hood or isolator (typically ISO 5). At some sites, the filling is conducted within a cleanroom, while at others, it is conducted in a dedicated non-cleanroom space, reflecting differences in cleanroom approach and specifications between regulators worldwide (71). Some equipment or facilities, such as the compounding hood or cleanroom, may require external certified laboratories for testing.

Material Handling

Material handling guidelines (69,70) require SOPs detailing a system to track all of the materials involved in the HP production process for a particular patient dose, similar to current good manufacturing practice (cGMP) requirements for material handling for drug compounding. This includes acceptance standards, storage conditions, amount used in the patient dose for each ingredient and materials used in the assembly of the fluid path and Pharmacy Kit. Currently some users choose to open and inspect and sometimes modify the Pharmacy Kits upon arrival, but some users keep them in the sealed packaging until they are required for dose preparation.

Pharmacy Kit Filling And Assembling

As required by an IND or its equivalent, the preparation of the doses of HP 13C agent are detailed in the Chemistry, Manufacturing, and Control (CMC) section of an applicable regulatory submission; an example of this has been made available (72). It describes the processes of filling the Pharmacy Kit with the different components that make up the final drug product, and of assembling the final kit for either storage or immediate use in the polarizer. Special attention should be given to the laser welding process in order to satisfy installation qualification (IQ) and operational qualification (OQ). Typically, the final developed process is validated by process qualification (PQ) runs, during which 3 or more Pharmacy Kits are filled and used and the final HP 13C products are tested for endotoxin and sterility and to confirm that they meet the dose specifications for injections (usually including pyruvate concentration, residual EPA concentration, pH, liquid state polarization level and dose temperature). The data from 3 consecutive PQ runs are submitted as part of the IND submission (or its equivalent), and are often also reviewed by the Institutional Review Board (IRB) where the studies are conducted.

Quality Control And Dose Release

The quality control (QC) and dose release can be separated into two aspects: one is the QC and release of the filled Pharmacy Kit, and second is the QC and release of the HP 13C agent for injection, after polarization and dissolution. For institutions filling a batch of kits and storing them to use over a period of time, typically the batch can be released based on initial validation, environmental monitoring data from the day of kit production, and if filters are used during preparation of any of the components, filter integrity testing. But in some cases one or more kits are used for validation before the batch of kits are released for future use. For institutions that fill only the kits required for specific studies shortly before the experiment, the filled kits often do not go through separate release tests before they are used.

The quality control of the HP 13C pyruvate solution post dissolution is primarily performed to ensure that the agent meets the dose specifications (Table 1) before it is administered to the subject. These specifications target both safety (pH, residual EPA, temperature) and efficacy (pyruvate concentration, polarization, volume). Typically, the pyruvate concentration, residual EPA concentration, pH, dose temperature, dose volume, and liquid state polarization are measured by the QC accessory associated with the SPINlab polarizer. Some users perform a secondary measurement for one of the parameters, such as pH, using a different instrument or pH paper. For sites that do not go through a separate release testing process for batch filled kits, the integrity of the sterilization assurance filter, a part of the Pharmacy Kit, is typically tested as a part of the dose release. It is also common for these users to preserve an aliquot of the final HP 13C pyruvate solution for post-release endotoxin and sterility testing. This testing cannot be completed fast enough to test an individual dose prior to injection, but this is why other processes such as PQ runs and validation testing are done to minimize the chance a subject could be injected with a contaminated dose.

The Final Dose Release And Injection

should be done under the supervision of a licensed professional, based on local regulations.

Some Key Challenges

Many of the challenges associated with HP 13C pyruvate preparation can be attributed to the conditions required for the dissolution-DNP method of high magnetic field (~3-7 T) and very low temperature (~1 K) during polarization, with pressurized and superheated water necessary for the rapid dissolution event. These extreme conditions are quite challenging for the design of the container-closure and fluid path system. In particular, the cryogenic temperature in the polarizer requires special attention to any moisture or ambient (moist) air introduced into that portion of the fluid path, which can form an ice block at ~1 K. This ice can lead to flow restriction during the dissolution event and reduce the strength of the laser welded bond between the cryovial and its cap. This can ultimately produce failures in the dissolution step, including variations in final pyruvate concentration and pH that may fail to meet QC release criteria as well as fluid path ruptures that provide no available dose and result in polarizer down-time.

The polarization of the HP 13C pyruvate sample decays quickly over the span of a few minutes after dissolution, and thus the process of dissolution, QC for release, and injection should be completed as fast as possible to preserve the high polarization level achieved. Any delays in the preparation process, such as transportation time or equipment malfunction, can significantly reduce the final polarization and result in lower quality imaging data.

Current Practices

A summary of data collected from all sites performing clinical trials with HP 13C-pyruvate is shown in Fig. 3 and Table 1, including the specification of the final dose and how the quality control and release of the final dose are performed. There is a split in the Production Style, described in the General Considerations section above, with 8/13 sites using Sterile Preparation versus 5/13 using Terminal Sterilization. While many of the dose specifications show notable differences in acceptable ranges, all of these variations listed in tables have been successfully and safely been used to perform HP 13C pyruvate studies in humans. Their differences depend on the institutions’ preferences, resources and their particular regulatory situation. There is high similarity in pyruvate ranges, temperature ranges, EPA limits, and volume limits. There is modest variability in pH ranges and large variability in the endotoxin test limit. There is a 3-fold difference in acceptable polarization levels, which are measured to ensure a futile dose is not injected since the polarization is directly proportional to SNR. This reflects the decision by several sites to believe that useful data can be still be obtained with suboptimal polarizations.

Figure 3: Hyperpolarized agent preparation methods reported by sites currently performing HP

In House

Table 1: HP 13C-pyruvate preparation parameters, methods, and dose specifications used for quality control testing and release as well as validation. These were obtained from a survey of all sites performing clinical trials with HP [1-13C]pyruvate. The parameters used for product release are noted in bold text, otherwise these parameters are measured for batch validation or other QC measurements. The endotoxin and sterility testing are performed during process validation of the batch and/or post-injection, and largely depends on the agent production approach.

Summary

The overall safety record of HP 13C-pyruvate has been very strong, and the SPINlab hyperpolarizer has proven to provide high polarizations at human sized doses while meeting numerous QC and release criteria. A weakness remains the failure modes of the SPINlab Phamacy Kits (e.g. ice blocks, path ruptures), which are placed under extreme requirements particularly during dissolution. The preparation process still requires a high degree of expertise.

Therefore, there is a significant need to improve the reliability, robustness, and ease of operation for generating HP 13C-pyruvate doses for human studies. Furthermore, there is a divide between manufacturing and sterile compounding style preparation as well as other site-specific practices, resulting in variations in SOPs and justification required to relevant regulatory bodies. There have also been no comparisons between these approaches. It is also unclear what release criteria and QC parameters are truly required to ensure patient safety.

However, all of the reported methods are acceptable and approved by the appropriate regulatory authorities, and have led to the rapid expansion of successful human studies in recent years.

Mri System Setup And Calibrations

This section covers the MRI system setup, including the imaging system, RF coils, phantoms, and prescan calibration methods.

Imaging System

The main prerequisite for a given MRI scanner to be capable of supporting studies with HP 13C is its “broadband” capability to transmit and receive radiofrequency (RF) signal at the frequency of 13C, which is around 4 times lower than 1H. This does not come as a default on clinical MR devices. The transmit power of the broadband amplifier should also be sufficient to support the intended flip angle and RF pulse shape with the employed transmission RF coil(s) for 13C. Most studies to date use relatively low flip angles (< 90 degrees) for HP 13C in order to preserve polarization for time-resolved imaging. The capability to receive 13C signal on multiple channels is also desirable to increase SNR, as discussed further in the “RF coils” section.

The choice of magnetic field strength is primarily dependent on the metabolites’ frequency separation due to chemical shift dispersion and 1H imaging. High field strengths do not enhance hyperpolarized 13C signal as they do for 1H because the signal strength in a HP experiment relies on manipulating the population of quantum energy states outside of the MRI scanner.

However, the injected HP 13C-pyruvate and its metabolic products have greater frequency separation at higher fields, and it may thus be easier to separate and quantify these resonances at higher fields. This comes at the cost of a reduction in the achievable T2* and often reduced T1. As the initial polarization is independent of the imaging field strength it has been proposed that the increased T2* at 1.5T can potentially be exploited to increase SNR by adapting the acquisition bandwidth or reduce off-resonance imaging effects in cases when the decay of the transverse magnetization is dominated by T2* (73). In practice, 3T has been used in all published human 13C-pyruvate studies surveyed (Supporting Table S1), and comprises the majority of scanners currently in use for human studies (Table 3). A field strength of 3T is well-suited for 1H MRI anatomical reference and correlative imaging.

Stronger and more rapidly slewing magnetic field gradients support more rapid spatial encoding, particularly for metabolite-specific single-shot imaging using echo-planar imaging (EPI) or spiral imaging (See “Acquisition and Reconstruction”). Although the spatial resolution acquired for HP 13C imaging is typically much coarser than for 1H MRI, the factor of ~4 in gyromagnetic ratio leads to the same reduction factor in performance of the gradient system, so 13C experiments are potentially more limited by gradient hardware performance. To date, all human studies have used the commercially-available integrated gradient systems provided in clinical MRI scanners.

Optimization of scanner design has understandably focused on minimization of artifacts in 1H MRI, where devices such as room lights, the gradient amplifiers, and the motors driving the patient bed are checked to ensure that they do not produce RF interference at the 1H frequency, but artifacts may arise at other frequencies. Eddy current compensation is also not always appropriately adjusted for nuclei at other frequencies (74). In order to optimize for 13C, many sites have performed checks on phantoms for RF interference, gradient artifacts, and eddy currents (74), including the use of post-hoc gradient impulse response function characterisation and correction, and some vendors have fixed these issues as well.

Rf Coils

For HP 13C imaging studies in humans, RF coils for both 1H and 13C nuclei are needed, with 1H MRI providing an anatomical reference for registration and optional additional multiparametric MRI readouts. At the Larmor frequency of 13C nuclei, the relative contributions from coil noise compared to sample noise increase compared to 1H (73,75), although sample noise still is likely the dominant contributor for human-sized coils at 32.1MHz - the resonance frequency of 13C nuclei at 3T.

The key requirement for human 13C-pyruvate RF coils are that the coil geometry and sensitive volume must cover the volume of interest in the subject. Table 2 and Figure 4 shows coil configurations that have been used and optimized for applications in different anatomic regions.

Volume resonators are most commonly used for transmit, as they surround the subject to

Provide B1 Transmit Across The Fov (B1

+). While 1H relies on a large birdcage (“body”) coil built into the scanner, 13C transmit coils must be placed inside the bore. This takes up valuable space within the magnet, and also has led to the use of designs with relatively inhomogeneous

B1

+. Many human studies have used Helmholz pair resonators for transmit, including the “clamshell coil”, which has a notably inhomogeneous B1

+ Profile But Has Been Used Because Of

relatively easy integration into the scanner bore. B1

+ Variation Results In Variations In The Flip

angles that control the use of the hyperpolarized magnetization and creates errors in common HP metrics (9,76). The exception are head coils, where birdcage designs with highly

Homogeneous B1

+ can be placed around the head while easily fitting inside the bore. As with 1H MRI, higher SNR can typically be achieved by smaller receive coil elements, such as surface coils or phased arrays, and the majority of 13C receive coils used have layouts similar to 1H phased arrays.

RF coil quality control is important to ensure proper functioning of the coils to provide consistent imaging quality, especially with limited natural abundance 13C signal in vivo. It typically involves 1) a physical integrity check of the coil cables and connectors and 2) phantom SNR tests to check the coil’s performance and to monitor it over time (see Phantoms below). An useful reference for RF coil quality control is outlined in the MRI accreditation program of the American College of Radiology (77) and can be adapted for 13C coils.

Notably, configurations for brain and prostate studies used dual-tuned 1H/13C coil designs, which greatly simplify workflow and registration of 1H and 13C images, as no switching of coils is needed.

(1)

Table 2: RF coil configurations reported for human HP [1-13C]pyruvate studies.

Tx = Transmit

coil, RX = receive coil. The commonly used “clamshell” TX coil is a Helmholz pair design. For 1H RF configurations, all used the Body coil for TX unless otherwise noted, and “repositioned” indicates the 13C coil was removed for 1H imaging. One representative reference is listed for each configuration. The RF coil configurations reported in the reviewed papers are shown in Supporting Table S1.

Figure 4: Examples of RF coil configurations used for human HP [1-13C]pyruvate brain studies. (A,B) 13C Clamshell TX (Helmholz pair) and 2× 4-channel paddle RX arrays. (C) 13C Birdcage volume TX and 32-channel RX array (RX array slides into TX coil). (D) 13C Birdcage volume TX and 24-channel RX array, combined with a 1H 8-channel RX array. Image reproduced with permission from Ref (16).

Phantoms

Since hyperpolarized magnetization is non-renewable, phantoms containing 13C nuclei are important to: 1) test the multi-nuclear capabilities of the imaging system, including all parts of the signal excitation and receive chain; 2) perform calibration measurements before a scan with hyperpolarized nuclei; and 3) perform necessary pre-scan adjustments (see “Prescan Calibration” section). The phantoms currently in use are listed in Table 3. Their composition must provide sufficient 13C signal, with additional considerations of conductivity, stability, chemical shift(s) present, potential for dynamic imaging, and cost. The phantom geometries are typically either compact, in order to be used alongside the subject during a HP scan, or large enough to mimic the inner volume of a RF coil for system testing.

One popular compact design contains enriched 13C-urea at high concentration, typically 8 M, which provides a single resonance, placed inside a small container ~1 mL. The most common recipe mixes 13C-urea in a 90% water/10% glycerol solution, with glycerol used to increase the urea solubility and doping with a Gd-based contrast agent to shorten T1 which increases the potential SNR per unit time. For example, when Dotarem is added at a 3:1000 volume ratio the 13C-urea T1 is around 500 ms and T2 is around 100 ms. However, when testing pulse sequences influenced by T1 and T2, doping should be used carefully. This phantom is suitable for frequency calibration, transmit gain calibration, sequence testing, and as a fiducial marker when placed next to a patient. However, enriched 13C-urea has a relatively high cost compared to natural abundance compounds.

For larger volumes (>100 ml), the phantoms most often used contain undiluted ethylene glycol, glycerol, or dimethyl silicone. These compounds have sufficiently high carbon concentrations to provide sufficient 13C signal even with the 1.1% natural abundance of 13C. These larger phantoms matching the inner volume of an RF coil are useful for coil testing, including transmit

+) And Receive (B1

-) coil profile mapping, as well as to mimic acquisitions using in vivo FOV requirements. In this case, size and conductivity should match the expected subject size in order to mimic coil loading and get a realistic estimation of B1+. Large-volume natural abundance urea phantoms have also been used by some sites, but suffer from higher conductivity compared to biological tissues. Typically, it is easier to increase the conductivity and hence coil loading of the non-conductive phantom by adding NaCl to match physiological loading (16,78).

Dynamic phantoms that aim to mimic metabolite kinetics have also been developed (79–81), and have the potential to more closely mimic the HP experiment, but so far these are not widely used.

Prescan Calibration

Prior to performing an MRI acquisition, the so-called prescan procedure is used to set the shim parameters to maximize B0 homogeneity over the field of view (FOV) or a specific region of interest (ROI), the scanner center frequency (CF), the RF transmit gain, and the receiver gain.

While this calibration procedure is usually automated for 1H, the lack of sufficient natural abundance 13C signal prevents use of automated methods. (Although natural abundance 13C lipid signal has been detected, there are so far no reports on using this signal for prescan.) Table 3 shows current practices across sites.

Maximizing B0 homogeneity is independent of the nucleus and is therefore performed prior to 13C imaging using the 1H water signal and existing shimming tools, such as by a standard automated process (“Auto Shimming”) or using high order shimming routines. Similarly, the 13C CF can be calculated from the 1H CF using a predetermined scaling factor that depends on the target chemical shift (82). Another common approach used is to have a small, high-concentration 13C phantom, e.g. 8M 13C-urea, integrated in the RF coil or placed next to the scan subject (1). The reference frequency can also be based on real-time measurements after the HP injection but prior to imaging (83). Both the CF and B0 shimming are critical when using spectrally-selective RF pulses, as inmetabolite-specific imaging methods, where the desired excitation bandwidths are typically very narrow and frequency offsets can lead to a failure mode that is only apparent after injection.

The calibration of the RF transmit power is typically performed on a small, high-concentration 13C phantom placed near the region of interest during the scan or on a large 13C phantom of similar size and coil loading as the subject, prior to the subject scan. Reference power is often done by sweeping the power in a pulse-acquire sequence (53,62), or the Bloch-Siegert method (52,84). When using a small phantom, the location of the phantom, B1

+ Inhomogeneity As Well

as any shielding effects, e.g., when the phantom is integrated into a coil (1), may degrade the accuracy. Other methods include real-time Bloch-Siegert method measurements after the HP injection (83), and using the stronger natural abundance 23Na signal that is close enough to the 13C resonance frequency to be detected by 13C coils (82).

The receiver gain is predetermined, either systematically based on independent phantom measurements and assuming the dose and polarization of the HP compound is known prior to injection, or based on past HP imaging studies.

Power [Kw]

Phantom(s) - during study Phantom(s) - before study 13C Frequency

8

13C-bicarbonate doped with dimethyl silicone, various

Maximum Values

Table 3: Summary of the imaging systems, phantoms, and prescan procedures used at sites currently performing HP 13C-pyruvate human studies. These were obtained from a survey of all sites performing clinical trials with HP [1-13C]pyruvate. *Previously performed studies with a Siemens 3T Tim Trio. The imaging systems, phantoms, and prescan procedures reported in the reviewed papers are shown in Supporting Table S1.

Summary

Commercially available 3T MRI systems are by far the most commonly used for human HP 13C-pyruvate studies, although a systematic investigation of the impact of B0 has only recently been investigated (73). The multi-nuclear RF transmit and receive chain has proven sufficient for current acquisition strategies, although many sites have observed artifacts due to RF interference, gradient interference, and residual eddy currents when operating at the 13C frequency. A variety of 13C RF coils, tailored for numerous anatomical targets, have been successfully demonstrated, with the main limitation that most transmit coils take up a lot of additional space inside the bore and provide relatively inhomogeneous B1

+ Profiles. The

phantoms used have converged into generally 2 categories - small phantoms containing 13C-enriched compounds that can be used during the study and human-sized phantoms containing compounds with high carbon concentrations but without 13C enrichment that are used to test and calibrate the coils. There are no standardized compositions or geometry, and dynamic phantoms that recapitulate in vivo kinetics would be desirable but are still an emerging area. Prescan calibration procedures were not well defined in most publications, so we surveyed individual sites to determine current practices. Calibration procedures for the B0 field (13C CF and shimming) for most sites take advantage of 1H signal and methods, while methods

For Calibration Of B1

+ is more variable across sites, likely a reflection of remaining challenges in how to perform this calibration. Standardization of both phantoms and calibration procedures would synergistically improve the robustness and reproducibility of HP 13C studies.

Acquisition And Reconstruction

Data acquisition strategies in human HP [1-13C]pyruvate MRI studies must account for multiple chemical shifts, efficiently utilize the non-renewable HP magnetization, and acquire data quickly relative to metabolism and relaxation decay processes. These studies require spectral encoding to separate metabolites, necessitating pulse sequences that efficiently encode up to 5D data (3 spatial + 1 spectral + 1 temporal dimension). RF pulses must efficiently sample without immediately saturating the non-renewable HP magnetization, and sequences must acquire data quickly and be robust to both experimental and physiologic variation (e.g. B1

+ Inhomogeneity,

variation in perfusion) to ensure reproducibility and minimize scan-to-scan variability. This section covers current successful practices for data acquisition in human [1-13C]pyruvate studies, and accompanying 1H imaging, from different anatomic regions, including scan parameters and image reconstruction.

Acquisition And Reconstruction Methods

The acquisition methods used in human [1-13C]pyruvate studies can be classified into 3 categories: 1) MR spectroscopy or MR spectroscopic imaging (“MRS/I”), 2) chemical shift encoding methods, and 3) metabolite-specific imaging (Fig. 5).

Mrs/I Methods Specifically

resolve a spectrum that can be analyzed to extract expected as well as unexpected resonances, making this approach very robust. It was used in many initial studies (1).

Chemical Shift

encoding methods, most commonly the Iterative Decomposition of water and fat with Echo Asymmetry and Least-squares estimation (IDEAL) method, use imaging sequences acquired with multiple TEs and rely on a model-based separation of expected chemical shifts (85).

Metabolite-specific imaging methods use specialized RF pulses that are spatially and spectrally selective to excite individual metabolites which are then typically imaged with fast k-space trajectories such as echo planar imaging (EPI) or spirals (86).

Their Application To Different

organ systems is described below. The image reconstruction methods used in human [1-13C]pyruvate studies have typically been conventional methods (e.g. FFT, non-uniform FFT, or equivalent). The incorporation of accelerated imaging and advanced reconstruction methods including parallel imaging (4,57,87) and compressed sensing (7) has also been applied in human studies for improved spatial resolution, temporal resolution and coverage, but have the potential for additional artifacts as well as SNR losses due to ill-conditioning of the reconstruction (e.g. g-factor).

The Majority Of

published studies do not use accelerated imaging indicating the resolution and coverage achievable without acceleration is currently adequate for successful data collection. Performing coil combination, even with fully sampled data has also been shown to have specific challenges for HP human images: using naive sum-of-squares methods suffer from high noise amplification in the relatively low SNR regime of HP [1-13C]pyruvate (compared to 1H), motivating several HP 13C-specific methods that include data-driven coil sensitivity estimation which have shown obvious improvements over sum-of-squares (11).

More recently denoising techniques have been applied as post-processing of human HP data(41,42,44). The techniques applied are based on spatial-temporal singular value decomposition for unsupervised estimation of signal and noise components. They have shown improvements in apparent SNR in the brain and liver, while care must be taken to choose parameters such as the rank threshold to avoid oversmoothing and overfitting to the estimated signal components.

Prostate Studies

Prostate cancer was the first human application of HP [1-13C]pyruvate (1), and data was acquired with MRS/I methods: 1D dynamic MRS, single-slice 2D dynamic echo-planar spectroscopic imaging (EPSI), and single time point 3D EPSI. Advances in imaging strategies led to the development and application of new acquisition schemes, including undersampled 3D EPSI with compressed-sensing (7), model-based chemical shift encoding methods that use a priori information (47,59), and metabolite-specific EPI (10), all of which can provide volumetric whole-organ coverage and dynamic acquisitions.

The pyruvate bolus arrival in the prostate can vary by ± 10 s between patients, necessitating dynamic imaging to reliably and consistently capture the pyruvate bolus (18). For this reason, all currently ongoing studies acquire dynamic data. While MRS/I, chemical shift encoding, and metabolite-specific imaging can all achieve dynamic imaging, chemical shift encoding and metabolite-specific imaging provide greater dynamic and volumetric coverage (85). For scan prescriptions, the FOV is designed to provide full prostate coverage and typically to match the orientation of the anatomic imaging used for registration. Flip angles used in current studies are constant through time, as quantification with a variable-through-time flip scheme is highly sensitive to bolus timing (8) and errors in the RF transmit (B1 +) field (76).

Heart Studies

Data acquisition methods for 13C imaging in the heart must be designed to meet the demands of significant cardiac motion and blood flow. To cope with the periodic cardiac motion, most human heart studies to date used gating to the diastolic window, the longest cardiac cycle interval, which has reduced motion (2,22,28,30,35,36,38,45,52). The duration of the diastolic window limits the available data sampling time, making cardiac acquisitions the most time-constrained of the HP 13C MRI applications. The most common acquisition approach is metabolite-specific imaging with spiral k-space trajectories (2). Their single-shot imaging capability makes these methods particularly robust to motion effects. Furthermore, spiral k-space trajectories provide rapid k-space coverage and relatively benign flow and motion artifacts. The majority of studies have used 2D multi-slice acquisitions, but 3D encoding has also been used successfully (35).

Brain Studies

For HP 13C MRI of the human brain, the majority of studies have also used 2D (slice selective) acquisitions (10–12,14,16,28,33,40,41,44,51,53,60), with a trend toward volumetric coverage using 2D multi-slice metabolite-specific imaging. 3D metabolite-specific imaging of the whole brain, with phase encoding of the slice direction (34,57), has been shown to provide similar SNR efficiency (88) compared with multislice imaging. A number of studies have employed MRS/I (5,6,29,31–33,50,55) resulting in a spectrum from each voxel, which has the advantage of not requiring a priori information about which peaks to encode. This was important in early brain studies when it was not known which peaks would be detectable. Chemical shift encoding, using a set of images with different echo times and an iterative reconstruction of the individual resonances (i.e. the IDEAL approach (85)), has also been used (12,49,54), with the drawback that coverage in the slice direction was limited due to the time required to acquire multiple echo time images.

Abdomen And Breast Studies

The fundamental approaches to data acquisition and reconstruction in the abdomen and breast are largely similar to the aforementioned applications, but demand attention to particular challenges associated with these anatomic regions, especially relating to respiratory motion.

Although it has been shown that a basic 2D MRSI approach based on phase encoding and FID readout can be successfully applied for HP 13C imaging in breast (15) and kidney (13), major advantages in terms of spatiotemporal resolution and coverage have been realized using tailored approaches based on metabolite-specific imaging (43,62) and chemical shift encoding (43), which have facilitated multi-slice or 3D dynamic acquisitions over large FOVs in the abdomen (4,37,46).

The significant respiratory motion encountered in these regions can directly blur 13C images, and has further favored these rapid acquisition strategies. Motion also degrades B0 homogeneity, which can shift frequency-selective excitation profiles and introduce artifacts into rapid imaging readouts. This makes accurate determination of the acquisition center frequency and shimming essential in these regions which often cover large FOVs. (See “Prescan Calibration” section for more information). In some studies, breath-holding was used to minimize motion effects and enforce frame-to-frame data consistency (42). A pragmatic and reasonably effective approach for dealing with respiratory motion during 13C data acquisition is an initial breath-hold (as long as can be tolerated), followed by free-breathing (46,62).

1H Imaging

Collection of 1H imaging data is essential both for prescribing the 13C acquisition and for interpretation of the resulting 13C data. Multi-planar 1H scouts are acquired prior to 13C acquisition to enable graphical prescription of the 13C imaging region. All human HP 13C-pyruvate imaging studies acquire conventional MRI scans (e.g. T1- and T2-weighted volumes) for anatomic reference, aiming to cover at least the full 13C FOV. Acquiring these anatomic scans as close as possible to the time of 13C imaging (immediately before or after) minimizes potential misregistration between the data sets. Depending on the application, other advanced 1H sequences are also acquired (e.g. diffusion-weighted imaging for cancer imaging).

When contrast-enhanced data is acquired, it is done after 13C imaging, as paramagnetic contrast agents will accelerate 13C relaxation.

Reported Study Parameters

Figures 5 and 6, and Supporting Table S2 shows the reported acquisition study parameters for human HP [1-13C]pyruvate studies published as of September 2022. Figure 5 shows a mixture of MRS/I, metabolite-specific imaging, and chemical shift encoding methods have been successfully used, where spectroscopy-based methods have become less prevalent in recent studies. Figure 6 shows the acquisition timing, including the important start time and interval/temporal resolution, is quite variable across studies.

Figure 5: Acquisition methods used in published HP [1-13C]pyruvate human studies published up to September 2022, classified into: MR spectroscopy and spectroscopy imaging (MRS/I); chemical shift encoding methods, such as IDEAL, that use multiple TEs and model-based reconstructions; and metabolite-specific imaging methods that use spectrally-selective excitation to image a single resonance at a time.

Figure 6: Temporal acquisition characteristics reported in HP [1-13C]pyruvate human studies published up to September 2022. (a) Reported referencing of acquisition start times.

(B)

Acquisition start times reported when using dynamic imaging and when timing was reported relative to the end of the injection. (c) Temporal resolutions. “Not Applicable” indicates dynamic imaging was not used.

Summary

Three general categories of acquisition strategies have been used successfully for human HP 13C-pyruvate studies: MRS/I, model-based chemical shift encoding (e.g. IDEAL) methods, and metabolite-specific imaging methods. These have enabled successful studies in the prostate, heart, brain, abdomen, and breast. Recent studies increasingly have used the imaging-based strategies of metabolite-specific imaging and chemical shift encoding which are the fastest methods, although a heads-to–head comparison between techniques has not been performed.

Metabolite-specific imaging is quite popular because of its speed and compatibility with single-shot imaging, but is sensitive to B0 field variations and thus requires careful calibrations. Nearly all studies surveyed acquired data dynamically, allowing measurement of the bolus and metabolite kinetics. The exact timings and associated flip angles vary quite widely across reported studies, with no consensus yet as to how to choose these parameters. Image reconstruction is typically done directly using Fourier Transform methods, and accelerated imaging strategies are uncommon.

Data Analysis And Quantification

This section covers the analysis of data from human HP [1-13C]pyruvate studies, including modeling and metrics, visualization, as well as considerations for how to store data and metadata. Depending on study design, the analysis may need to give quantitative or semi-quantitative output reflecting a biological process or may just reflect a contrast between different regions of interest for quantitative evaluation.

Metrics

Figure 7: HP [1-13C]pyruvate raw data (A) have typically been quantified using four categories of metrics depending on the acquisition. Data acquired as a single time point are often quantified using normalized metabolite images or metabolite ratios (B). Dynamic data can be quantified using normalized metabolite images or metabolite ratios (B), or with metabolite timings such as time-to-peak (TTP) or pharmacokinetic (PK) models (C). The latter two require the data to be time-resolved. [1-13C]alanine and 13C-bicarbonate are analyzed similarly to [1-13C]lactate but omitted here for display.

Metabolite images are commonly used as summary metrics for HP MRI data, often including some form of normalization as well as summed over time as an area under the time curve (AUC) (17). These are analogous to the visual evaluation that is most used for routine clinical work (89,90). In these metabolite images, we expect that the [1-13C]pyruvate AUC signal is predominantly weighted towards perfusion and uptake, while [1-13C]lactate, [1-13C]alanine and 13C-bicarbonate AUCs represent metabolic conversion. The strength of this approach lies in its simplicity and relatively few underlying assumptions. Limitations to the use of single-metabolite images or AUCs include sensitivity to inhomogeneous coil profiles (57,87,91), the acquisition strategy and acquisition parameters, pyruvate polarization and concentration level, and signal relaxation rates (92). Further, the reader must be careful to interpret all the images in conjunction to better understand the underlying biology; for example, increased [1-13C]lactate in the presence of decreased [1-13C]pyruvate delivery can have a very different meaning compared to increased [1-13C]lactate with increased [1-13C]pyruvate delivery.

In an attempt to address variations in coil sensitivity, polarization level, and pyruvate delivery, AUC images are often computed by normalizing to a specified parameter, such as the maximum pyruvate or average lactate signals, or presented as a ratio such as lactate/pyruvate or divided by “total Carbon” - the sum total of HP 13C signal observed across all metabolites. The AUC ratios between metabolites and pyruvate are proportional to the corresponding forward kinetic rates (81,93), but are not directly comparable to rate constants when magnetization loss rates (e.g. relaxation and losses due to signal excitation) differ between studies. Similarly, the ratios between the produced metabolites (e.g. bicarbonate/lactate) can reflect the balance between downstream metabolic pathways (12,55). Care must be taken to consider how AUC images are calculated and normalized before comparing values between studies.

To further quantify the interpretation, pharmacokinetic (PK) modeling approaches were developed to compute the apparent kinetics of pyruvate-to-metabolite exchange (92,94–99). These yield semi-quantitative to quantitative apparent rate constants, given in s-1. Some models require a vascular input function, while others avoid this requirement (95). PK models can explicitly account for acquisition-specific details such as excitation angle and repetition time, and thus may reduce the effects of these details on quantification. An input-less model, provided in the Hyperpolarized-MRI-Toolbox (https://github.com/LarsonLab/hyperpolarized-mri-toolbox) (100) and thus frequently employed for human data, has been shown to fit well and robustly to prostate and brain data (8,20). PK models are quantitative in nature, arguably provide more relevant biological information (8,20), and appear to be reproducible across sites (51). However, rate constants derived from PK models are still apparent rates, and likely do not reflect a single biological characteristic.

Some additional considerations include whether complex or magnitude data is used, as the noise behaviors will impact the analysis differently. Additionally, cut-off thresholds or other criteria may be used to identify and avoid voxels with insufficient SNR before analysis to improve robustness (20,41).

Regardless of the analysis approach, the underlying biology is not always clearly represented by the data; instead, the metrics may be influenced by perfusion, barrier permeability, intercellular shuttles, enzyme activities, co-substrate concentrations, or combinations thereof, depending on the organ and disease of interest (19,43,94,101–103). This may be addressed by incorporating complementary information. As an example, HP 13C pyruvate data is influenced by perfusion, and thus addition of perfusion MRI could be important for interpretation (98,104,105).

All the methods outlined above have been explored in clinical studies, described in Supporting Table 3 and summarized in Figure 8. As of September 2022, approximately 52% of studies involving human subjects report rate constants derived from a PK model with a few different models reported. A nearly equal fraction (51%) of the studies report AUC ratio values.

Approximately 66% of these studies report metabolite-specific images or AUC values. About 40% report SNR values; this metric is particularly frequent in manuscripts that describe technical developments for clinical HP MRI. Approximately 16% of these studies summarize model-free metrics, and 10% report measurements from a single timepoint. Most studies report a combination of quantities.

Figure 8: Reported metrics used for analysis in HP [1-13C]pyruvate human studies published up to September 2022.

Visualization

A wide variety of approaches have been used for visualizing data from human HP 13C-MRI studies. The challenges and practical considerations are: 1) choosing the appropriate metrics to display, 2) how to encode the parameters (e.g. the colormap), and 3) choosing how to provide anatomical context and other multi-parametric data. The choice of visualization also depends on the goal which could be for diagnostic interpretation, but also quality control, reproducibility among readers and publication.

Metrics

The choice of HP 13C metrics is described in detail above. At this stage in HP 13C development where there is no standardized metric, often a combination of metabolite images and ratios or PK model parameters are shown.

Parameter Encoding

The mapping function chosen should provide an adequate, often quantitative, impression of the parameter mapped. There is a consensus in the visualization field that perceptually uniform maps are best suited to visualize continuous parameters, like the greyscale typically used by radiologists as well as other monochrome (black to blue) and color ranges (fire-type, rainbow-type) (106,107). Multi-color heatmaps have been the most frequently employed method for HP 13C data, while greyscale has infrequently been used but it ensures there is no coloring-based bias as well as facilitating later reuse (Fig. 9a). Among the color schemes employed in the clinical HP 13C literature, fire-type scheme seems to be the most common [similar to “Plasma” or “Inferno” in matplotlib.org]. Next most commonly employed is the rainbow-type scheme [similar to “Rainbow” in matplotlib.org].

Anatomical Context

HP MRI faces the challenge that it does not necessarily depict the anatomical features, similar to PET, and thus requires an anatomical reference. Most often, a grayscale anatomical image is overlaid with a HP colormap (Fig. 9c,d). This approach is very intuitive, but can skew perception as the grey-scale anatomical reference may affect the brightness of the HP data (e.g. signal in the skull). This bias does not occur when showing adjacent maps (Fig. 9a, b). Here, anatomical outlines may help to provide reference (Fig. 9b).

Related Journal Articles & DOI Links

Selected peer-reviewed publications relevant to 12 Lead ECG Acquisition. Click the DOI to access the full paper (may require institutional access).

Why Choose Us?

Bangalore guidance for robotics, Spectre and autonomous systems projects.