Trail of Bits

Fermat famously claimed to have a “truly marvelous proof” of his Last Theorem, but he never wrote it down, insisting the margin of his page was too narrow to contain it. A few centuries later, Anthropic announced a complete formalization of Fermat’s Last Theorem using 13 million lines of Lean code (clearly not what Fermat intended). Luckily, we found a wonderfully cursed Lean bug, shown below, that suggests the proof may have fit the margin after all. The issue affects all stable versions of Lean up to 4.33.1, and the patch is incorporated in v4.34.0-rc1. A “checked” proof of Fermat’s Last Theorem using Lean 4.33.1 The blue checkmarks in the screenshot above would suggest that Lean considers this proof correct. This seems odd given the amount of work Sir Andrew Wiles put into this problem and the vast size of Claude’s proof. So what is going on? The “proof” clearly doesn’t make any sense and exploits an issue in Lean. We found the issue while using GPT-5.6 to experiment with a new skill for code review. We want to clarify up front that the issue is not a kernel soundness issue, but it happens to nicely fit any discussion of strings, lengths, and substrings. The issue affects String.Pos.Raw.extract, Lean’s low-level string-slicing function. When asked to extract a one-byte slice at an astronomically large position, Lean’s logical definition returns the empty string. But the compiled native code returns the entire original string. That disagreement is enough to manufacture a contradiction. Lean’s ordinary evaluator “proves” that the tiny slice was empty, while native evaluation “proves” that the very same slice contained “a truly marvelous proof.” Put those together, and Lean concludes that the empty string equals a non-empty string. And once you have a contradiction, you can prove anything, including Fermat’s Last Theorem. On the bright side, the Lean team was considerably faster than mathematical history. About 90 minutes after we reported the issue, hargoniX opened a fix for the memory-safety problem, and it was merged roughly three hours after filing. The remaining semantic mismatch was fixed by Rob23oba five days after the report, closing the issue. We’d like to give a huge shoutout to hargoniX, Rob23oba, and the Lean team for the fast turnaround. As a reminder, when dealing with external proofs, follow Lean’s guidance for validating a Lean proof. In our proof-of-concept code above, #print axioms flt shows ‘flt’ depends on axioms: [propext, Classical.choice, Quot.sound, flt._native.native_decide.ax_1_1]. The extra axiom native_decide adds the compiler to the trusted boundary, and therefore needs to be used with care. Machine-checked proofs will increasingly enable an unprecedented level of trust in mathematical results and critical software. However, more work is needed (e.g., lean4lean and alternative kernel implementations) to ensure that proofs aren’t deemed correct through exploitation of issues in theorem provers. Fermat’s theorem took 350+ years to prove. If you don’t want to wait that long for your code to be audited, contact us.

As part of Patch the Planet, we received preview access to GPT 5.6-Cyber with a simple task: evaluate its cyber capabilities. Recent events inspired me to give it a challenge to work through: escape the VM I’d normally use for sandboxing. The target was a QEMU/KVM VM on my Linux dev machine (Debian Linux 12, AMD Zen3). It escaped the VM three different times. First, it used recently disclosed bugs in my host kernel. When I fully updated, it used disclosed bugs that had not yet reached package maintainers or were not classified as security bugs. When I rebuilt QEMU and dependencies from the latest upstream source, it found several 0-days. It operated autonomously for hours, backtracked from approaches that didn’t work, pulled code and research papers, wrote oracles, made its own minimal examples, and aimed for a reusable, reliable exploit, all with minimal handholding and prompting. My main job was to physically reboot the machine when it hardlocked the host kernel. If it wasn’t clear before, I will state it plainly: you can no longer assume a mere VM will contain a sufficiently advanced AI agent. To use a 2010s term of art, you should treat such agents as an advanced persistent threat. Advancing cybersecurity capabilities Let’s imagine a common situation: you want to run an AI agent, but need its full capabilities, including the ability to download, build and debug software; do research; sift through dependencies; set up fuzzers; triage vulnerabilities; and stand up services under different configurations. The generally accepted solution is to set up a VM that serves as a safety perimeter and isolated prison for the agent: this virtual environment contains nothing of value, is separate from the host, and can be immediately deactivated or snapshotted for later investigation. This setup allows the agent to roam free, while isolating your computer from its consequences. There is, of course, a tiny wrinkle. To be useful, the virtual environment must share resources with your host machine and provide a way to interact with the agent: you want to be able to see its screen, get files in and out, etc. You also almost certainly want the agent to have (some) network access. Are these shared software, state, and communications pathways enough for the agent to escape containment? For a long time the answer was “no, absolutely not.” More recently, I’d have thought “maybe, after a while.” It turns out the real answer was “yes, and quickly.” I gave the agent a simple task: It was in a CTF; to win, it had to break out of the VM and successfully read the flag file. The agent was started outside the VM, given SSH access into the VM environment, and permitted to do anything inside the VM. It was to keep a research log of findings. Why start outside the target environment, even though it could lead to cheating? I was operating under the (correct) assumption that escape attempts may lock/crash the VM during operation. The risk of starting the agent from the host was acceptable: there was nothing of particular importance on the dev machine, and any final exploit could be audited for cheating its objectives. Escape 1: Januscape (CVE-2026-53359) About an hour after letting the agent run, the host machine was hardlocked. Luckily, I had a logged-in session where I could read scrollback: the agent found my host machine kernel was vulnerable to Januscape (which was disclosed a few weeks earlier). There is no public exploit, but the agent had built one, and had enough confidence to test it—except that it didn’t land cleanly. I have no doubt that after some more revision it would have. One point for GPT 5.6-Cyber. I updated my kernel to the latest offered for Debian 12. Escape 2: libslirp I am old and I like stability and consistency. That is why I run Debian 12, the current oldstable. Oldstable works, changes slowly, and gets security updates—exactly the known quantity I want from my software. Unfortunately, it seems that some security updates do not quite make it into the distribution. In this case, Debian 12 still ships libslirp 4.7.0, which is vulnerable to CVE-2026-9539. The agent also discovered that a bug fix commit in libslirp with no CVE assigned could be combined with CVE-2026-9539 to craft an arbitrary memory read/write in the host. After that, escape is trivial. Two points for GPT 5.6-Cyber. For those curious, libslirp is a library that enables VMs to have networking, which you almost always want. I did not even know what libslirp was, or that the version I was running had both known and fixed-but-unmarked vulnerabilities. The AI agent deduced it quickly and was able to combine the two vulnerabilities to escape. To make escape more challenging, I manually fetched the latest upstream libslirp and QEMU, and rebuilt a minimal QEMU with only the features I needed. Persisting across long time horizons One of the most impressive features of GPT 5.6-Cyber and Codex with goal mode is effective persistence over long (here, approximately 12-hour) time horizons across multiple compactions and innumerable subagent invocations. I did not do anything special to elicit this behavior; while my prompt included directions for the agent to keep a ledger of its findings, this was mostly for me, not for the agent. The agent searched diligently and backtracked from multiple paths that led to failure. First it tried identifying what was accessible via the network on the host; it found a CUPS server (with a known CVE that had not made it to oldstable packages), but was not able to complete exploitation due to AppArmor. It then detected I run my host kernel with mitigations=off and attempted to use hardware bugs to get a read oracle of host memory (the primitive was too unreliable). Eventually it went on a bug-hunting analysis of the host kernel source, QEMU, and associated libraries. It slowly chained together multiple vulnerabilities, including several 0-day bugs, until it could craft a reliable VM escape. Escape 3: 0-days This is what the agent used for the final exploit chain: three 0-days (at time of discovery) and one patched vulnerability that didn’t make it to my distribution kernel (because it was not recognized as a security issue): Component Patched? Description Capability QEMU No; bug has been reported. VAPIC’s unchecked ROM alias could overlap locked SMRAM. Exposed SMRAM and enabled attacker-controlled SMM execution. Linux KVM Patched in upstream Bug details pending stable kernel patches Left an attacker-modified shadow page unsynchronized and reusable. Linux KVM Yes in upstream, not in distribution kernel paging64_invlpg() reused a stale level-2 role after the guest entry changed to a 4 KiB mapping. Created a writable 2 MiB host-physical mapping, enabling QEMU heap modification. libslirp No; bug has been reported. Mixed fragment IHLs caused ICMP reflection to copy data beyond the reassembled packet. Produced thousands of recognizable, live NetPacket objects for locating and hijacking a callback. Here are the vulnerabilities the agent found but did not use in the final chain: Component Patched? Description Capability Why it went unused libslirp No; bug has been reported IPv6 retained bytes beyond the declared payload length. Host-stream data injection Less reliable and required a suitable host service; the KVM chain provided a stronger primitive. CUPS Yes in upstream, no for distribution Slirp loopback forwarding exposed CUPS’s reusable root Local certificate. Persistent root file overwrite through a file:// printer AppArmor blocked the sensitive host paths needed to retrieve the flag. QEMU Yes, now, but not when found A mode transition left a 96-byte panning buffer for a 1,024-byte render. Controlled QEMU heap overflow The target used -display none, so no display listener reached the renderer. QEMU No; bug has been reported Queue reset left requests alive, causing inuse underflow and completion reentrancy. QEMU denial of service and bounded queue-state corruption No unbounded memory-write or host-execution primitive was demonstrated. Challenging current software security assumptions My suspicion was that GPT 5.6-Cyber would succeed, but the frequency and manner of its success removed all doubt. We have to reassess sandboxing quality for capable AI agents, and in general the software stack with which they interact. An off-the-shelf VM is not enough to contain a modern, cyber-capable AI agent. There is simply too much attack surface. Even innocuous features (like running with a display) add extra, exploitable attack surface. A distribution with rapid updates is now a requirement. I love older, stable software, but the cycle of backporting patches is simply too long. An older distribution (like Debian 12, my old standby) that isn’t getting immediate upstream updates should be assumed vulnerable. A competent agent will discover these bugs quickly and synthesize target-specific exploits. What can we do? A start is using a virtualization technology that was purposely built with a minimal attack surface and a focus on security, like Firecracker. I had the AI agent run against Firecracker. It was able to hardlock the machine due to more Linux kernel flaws (all patched in upstream), but could not successfully escape. It may have, given even more time, but Firecracker is obviously a substantially harder target. In general, we have to become much more attentive to security fundamentals: least privilege (regarding network access, credentials, available features, etc.), logging, and active monitoring. Further, we can limit the time agents have to operate and ensure a pristine environment for each use.

We found and reported a bug in Provenance Blockchain, a public proof-of-stake chain built on Cosmos SDK, that lets any user grant themselves admin control over marker accounts without holding a single token. Provenance covers a range of financial services, including on-chain tokenized loans, private equity tokens, bridged assets, and asset registries. Our bug affected 82 markers representing live financial assets on mainnet. We found the bug, which affects versions before 1.28.0, in March 2026, and reported it to Provenance on April 1. It was mitigated in PR #2627 (commit c81fd65), which shipped in v1.28.0 on May 1, 2026, and fixed in PR #2734, which shipped in v1.29.0 on June 8, 2026. What is a marker? The marker module is Provenance’s core primitive for fungible tokens. Chain participants can issue a new asset on Provenance by submitting a MsgAddMarkerRequest transaction; the chain creates a dedicated account for that asset, called a marker. Each marker is a special account type that controls: A denomination (e.g., uusd.trading, cusd.deposit, cguaranteedrateomni) An access control list governing who can mint, burn, withdraw, deposit, or administer the token A supply field recording the canonical token count An escrow balance (the marker account can hold any asset, not just its own denomination) Markers are either supply_fixed (the supply field is enforced as a hard cap) or non-fixed (the bank module is the source of truth; the supply field is informational). This distinction is central to the bug. The bug: An access check anyone can pass AddAccess is the Cosmos SDK message handler that processes requests to modify a marker’s access control list. It checks whether the caller is authorized using three conditions, any one of which is sufficient: The caller is the marker’s designated manager and the marker is in Finalized state. The caller already holds ACCESS_ADMIN on the marker. The caller controls 100% of the marker’s circulating supply. case types.StatusFinalized, types.StatusActive: if !(caller.Equals(m.GetManager()) && m.GetStatus() == types.StatusFinalized) && !m.AddressHasAccess(caller, types.Access_Admin) && !k.accountControlsAllSupply(ctx, caller, m) { return fmt.Errorf(“%s is not authorized to make access list changes against finalized/active %s marker”, caller, m.GetDenom()) } Figure 1: Authorization check in keeper.AddAccess (x/marker/keeper/marker.go#L94–L100) Condition 3 is implemented by accountControlsAllSupply: func (k Keeper) accountControlsAllSupply( ctx sdk.Context, caller sdk.AccAddress, m types.MarkerAccountI, ) bool { balance := k.bankKeeper.GetBalance(ctx, caller, m.GetDenom()) supply := m.GetSupply() // ← bug return supply.Equal(sdk.NewCoin(m.GetDenom(), balance.Amount)) } Figure 2: The vulnerable accountControlsAllSupply function (x/marker/keeper/marker.go#L866–L875) The m.GetSupply function reads the supply field stored directly on the marker struct. For non-fixed supply markers that were activated with zero supply, that field always stays zero. The live circulating count lives in the bank module, and non-fixed markers never write back to the marker struct after minting. So for any non-fixed supply marker, the authorization check reduces to the following: supply = Coin{denom, 0} // stored marker field, always 0 balance = Coin{denom, 0} // attacker holds no tokens 0 == 0 → true Figure 3: Authorization check result for a non-fixed supply marker when the caller holds no tokens The check intended to restrict access to 100%-of-supply holders becomes unconditionally true for any caller with zero balance. Exploitation: Two transactions to mint or drain An attacker sends a single MsgAddAccessRequest transaction: { “denom”: “uusd.trading”, “administrator”: “<attacker_address>”, “access”: [ { “address”: “<attacker_address>”, “permissions”: [“ACCESS_ADMIN”, “ACCESS_MINT”, “ACCESS_WITHDRAW”] } ] } Figure 4: MsgAddAccessRequest granting the attacker admin, mint, and withdraw permissions on a target marker No existing tokens are needed for exploitation. The authorization check passes immediately via the broken condition 3. From there, the attacker has two paths: MsgMintRequest: to mint new tokens of the marker’s denom and send them to any address MsgWithdrawRequest: to drain any assets held in the marker’s escrow balance The whole attack is two transactions: one to gain permissions, and one more to act on them. Impact: What was at risk At the time of discovery, 82 active markers on Provenance mainnet had a stored supply of 0 while carrying real circulating supply or escrowed assets, every one of them exploitable. These markers span multiple independent parties on the chain, not a single application. Escrow withdrawal was the most direct path. Among the affected markers, those holding nhash (Provenance’s base token) in escrow accounted for roughly 30 × 1015 nhash, or around $500,000 at HASH prices at the time of discovery. The three largest markers are shown below: Marker Owner Escrowed nhash grant0051 Provenance Foundation grant program 19,230,770,000,000,000 provenance.validator.incentive.program Chain validator incentive fund 8,561,225,000,000,000 grant0077 Provenance Foundation grant program 2,486,556,736,909,250 The three markers shown above are all chain governance programs operated by the Provenance Foundation: one holds validator rewards, and two hold community grant funds. Supply inflation was a broader but more constrained vector. The 74 vulnerable markers spanned bridged stablecoins and wrapped assets (uusd.trading, uusdc.figure.se, nbtc.figure.se), consortium deposits (cusd.deposit), tokenized mortgage participations (cguaranteedrateomni, chomebridgeomni), and yield tokens (nuva.ylds, uylds.fcc). An attacker with ACCESS_MINT on any of these could issue arbitrary new tokens of that denom. The practical harm depended on the token type. For restricted tokens with KYC requirements, it was primarily a solvency and integrity threat; for non-restricted coin-type markers, it was a more direct inflation risk. We confirmed the affected markers and their balances by querying mainnet via the Provenance CLI and the public REST API. The fix: Read live supply, and guard against zero PR #2627 shipped the mitigation, which adds a check against zero supply: if supply.Amount.IsNil() || supply.Amount.IsZero() { return false } Figure 5: The fix (x/marker/keeper/marker.go in PR #2627) This blocked the attack we reported. All 82 affected markers had a stored supply of 0, and a zero-supply marker now fails the check outright. It did not fix the divergence. The comparison still read the stale field, so it still passed whenever that field was non-zero and the caller’s balance happened to match it. PR #2734 shipped the full fix, which changes one line: // Before: reads stale stored field, always 0 for non-fixed markers supply := m.GetSupply() // After: reads live circulating supply from the bank module supply := k.bankKeeper.GetSupply(ctx, m.GetDenom()) Figure 6: The one-line fix (x/marker/keeper/marker.go in PR #2734) Both sides of the comparison now come from the bank module, so there is no stale field left to diverge. Authorization must fail from the default state The root cause of this issue was state desynchronization. The marker struct and the bank module both represent the token supply, but only the bank module is kept current for non-fixed markers. The authorization check read from the wrong one. The check wasn’t just wrong; it was bypassable by default because of the zero-equality shortcut. Because the stale field was always 0, the comparison 0 == 0 was always true. An access control check that compares against a value that is always the same as the attacker’s default state is trivially bypassable. Switching to the live bank supply alone doesn’t fully close the hole. A freshly deployed marker with no tokens minted yet also has live supply of zero, so an attacker could self-grant admin by targeting it before it’s funded. The fix handles this with an explicit zero-guard: accountControlsAllSupply returns false whenever live supply is zero, regardless of balance. The broader pattern: an authorization predicate must never be satisfiable from the attacker’s default state. A check of the form balance == supply hands access to everyone when supply can be zero, whether because the state is stale or the marker is simply unfunded. Two things would have caught this before it went live. First, the access-list authorization model was never specified. Writing the rule down forces both questions that point straight at the bug: which supply, and what happens when it’s zero? Second, the property is easy to state: accountControlsAllSupply should only return true when live supply is positive and the caller holds all of it. A property-based test or fuzzer that generates random sequences of marker operations, such as minting, transferring, and creating empty markers, and checks this property after each step would find both failure modes automatically.

Every Signal chat starts the same way: the client asks the Signal server for the public key associated with your contact’s phone number. But how do you know the server gave you the right key? A compromised server could provide a false public key, allowing the client to encrypt messages to an attacker rather than the intended recipient. Until now, the only way to detect such malfeasance was to verify safety numbers with your contact in person or over a trusted channel. Signal recently launched an alternative: Automatic Key Verification, a feature that helps validate that your chats are secure without requiring direct safety number comparison. Trail of Bits built and operates one of the three auditors that make this system trustworthy. Our auditor, which is an independent implementation written from scratch, continuously checks that the Automatic Key Verification system behaves honestly. How key verification works Automatic Key Verification is a form of “key transparency” that makes mismatch attacks harder to hide by creating a globally consistent view of the set of public keys associated with each phone number. The Signal app now performs a periodic self-check to ensure that all keys stored in the global map for your account belong to your devices. If the app is unable to verify the log, or finds that not all keys are expected, the user is presented with a warning that “Automatic Key Verification is currently unavailable for your device.” Automatic Key Verification may also be unavailable for other reasons, as outlined in Signal’s documentation. What our auditor does Automatic Key Verification depends on external auditors. Trail of Bits helps this system function by providing external verification that the user ↔ public key map is globally consistent and well formed, and does not hide any entries. Each time a new entry is added, we update our local copy of the map, stored as a Merkle tree. Periodically, we sign the head of the tree using a signing key that only we know. Because we commit to only ever signing one consistent lineage of Merkle trees, clients know that they are seeing the same set of public keys as everyone else in the system. Clients currently require signatures from each of three auditors: one operated by Signal, one operated by Cloudflare, and one operated by Trail of Bits. When Automatic Key Verification is turned on, the Signal client periodically fetches Merkle tree heads from the Signal key transparency server. The client requires that each tree head belong to a lineage endorsed by all registered auditors within the last seven days. If the server does not present valid auditor signatures, the client will raise a warning and Automatic Key Verification will fail. A fully malicious server may therefore maintain a split view of the system for at most one week before client applications start to display warning messages. We chose to implement our auditor from scratch, based on the specification, to provide independent verification; the code is open source. Signal also publishes a reference implementation. We will provide updates to this blog post if we need to make substantive changes to our signing policy, such as resetting the state of our auditor or rotating our signing key. Our current public key is: 7fe5d91de235188486d8fb836a6da37e625e2b10eb6d144185b9364cc83cbbb6 How to use Automatic Key Verification You can enable Automatic Key Verification in Signal by going to “Settings > Privacy > Advanced” and enabling Automatic Key Verification. In supported chats, you can verify the public key of your counterparty by visiting the safety number verification screen and clicking “Verify Automatically.” Automatic Key Verification often does not support chats where you started the conversation by searching for a recipient’s username. See Signal’s help page for more information. If automatic verification fails, users should fall back on safety number comparison. Why we’re doing this We believe that free and private communication is a critical public good. We are not paid by Signal or any other party for this service; we operate it in the interest of users and the community broadly. Some form of public key integrity is an important component of any full end-to-end encryption system. If you would like to implement key transparency or end-to-end encryption generally, contact us.

Nitro Enclaves and Key Management Service (KMS) feel like a natural fit: since the KMS can verify attestation documents generated by the enclaves, developers can offload key management tasks from their applications to the AWS-managed service. But integrating an external service with your trusted enclaves comes with new threats, even if that service comes from the same provider. In this blog post—the third in our series on Nitro Enclaves, following our posts on attack surface and images and attestation—we catalog passive and active attack classes against the enclave-KMS communication channel, and cover the operational risks that persist even when the cryptography is correct. Intro to KMS The KMS is an AWS service that provides a unified public API for creating and managing keys backed by HSMs to the broader AWS ecosystem. There are three main key types supported by KMS that devs need to care about: Customer-managed keys (CMK) Data keys (DK, symmetric) Data key pairs (asymmetric) CMKs never leave KMS. You request KMS to perform cryptographic operations (like encryption or signing) for you. Data keys and key pairs are generated in KMS, are not stored in KMS, and are intended for programmatic uses. For symmetric keys, the KMS gives you a plaintext key and the same key encrypted to CMK. Your application performs encryptions, removes the plaintext key, and stores the key encrypted to a CMK along the ciphertexts; this pattern is called envelope encryption. For asymmetric keys, the KMS gives you a plaintext key pair and the private key encrypted to CMK. Your application creates signatures or encrypts data, deletes the private key, and keeps the public key and encrypted private key (along with signatures/ciphertexts). Both types of data keys can be used with Decrypt operation to get plaintext keys again. S t o r a g e s t { o E r _ e d ( k E , _ C d } k , C ) E n c l a v G e e { n d e k C D p r , = e l a E e c a t _ n r i e d c y n D k ( p t a = d t e t e k ( { x a n , c d t K c p m k = e ( l k } d y c a _ e ( m i i c c k n d ( m , t , d k d e E k _ k x _ , i ) t d C d } ) k ) ) ) K M S Figure 1: Basic KMS operations. cmk_id is an ID (ARN) of CMK key, cmk is the actual key used, enc/dec are any encryption/decryption algorithms, GenerateDataKey and Decrypt are KMS operations. Access to keys is subject to authorization policies, including key policies, IAM policies, and grants. Cross-account access for keys can be enabled. Keys can be identified in multiple ways: ARN, Id, Alias ARN, and Alias name. Keys are usually per-region (single-region), but multi-region keys can be created too. Enclave-KMS communication There are two mechanisms that are in play when integrating KMS with Nitro Enclaves: KMS policies restricting access to CMKs to specific enclaves (by PCR values) KMS encrypting responses to enclave’s public keys In the first mechanism, the key policy may authorize access to only requests that contain fresh and correctly signed attestation documents with the expected PCR values. Enclaves have to generate attestations and include them in requests to KMS. Note that the enclave still needs IAM credentials to access KMS in the first place. The second mechanism is about enclaves sending asymmetric public keys (inside the attestation documents) to KMS, and KMS encrypting part of the responses to the key. This mechanism is supposed to ensure that only the requesting enclave can see output from KMS. Only a few KMS operations support these two mechanisms. The operations are: GenerateDataKey, GenerateDataKeyPair Decrypt DeriveSharedSecret GenerateRandom Note the absence of the Encrypt operation: enclaves can request this operation, but without the attestation-based security mechanisms. CMKs cannot be used directly by enclaves for encryption without missing on the attestation checks. This means cryptography operations are supposed to be implemented via data keys, and not directly via CMKs. S t o r a g e s t { o E r _ e d ( k E , _ C d } k , C ) E n c l a v e G D e { e { n E E c E e _ _ d C r _ d p r a d e = y a e l a = k c e p 2 c a t e = ( n t = ( i e n e a c ( e a n D c n t ( c n t t a ( c t d m c t e t a ( e k k ( e x a t c s , _ a s t K t m t p i t t = e e k _ l d t _ d y s , p a , e p e ( t d r i E s r c c _ k i n _ t i ( m p ) v t d _ v d k u } , e k p 2 k _ b E x , u , , i , _ t a b E C d d a ) t 2 _ ) , k ) t , a a ) e d 2 t , s k ) t t ) e _ } s d p t k u _ b d p 2 k u ) b ) K M S Figure 2: Basic KMS operations with enclave attestation. Use cases KMS can be integrated with Nitro Enclaves for various reasons: for application-specific needs, to sign enclave image files (EIFs), or to increase the entropy available in the enclave. The application-specific use cases are based on KMS’ ability to verify attestation documents, which in turn enables developers to write KMS authorization policies based on PCR measurements from the attestation. A common use case is implementation of authenticated external storage for the enclaves. When access to KMS keys is restricted by PCRs 0-2, only a specific enclave version has access to the keys. Enclave image files can be signed. Any signing certificate (private key) can be used for the task, but the officially supported ways include signing with a key stored in a local file, and via KMS. The signing certificate used for the EIF is then exposed as PCR8. This PCR can be used in KMS policies. This feature lets one to restrict access to KMS keys to enclaves created by the same developer, while developer identity is protected by the KMS too. Finally, the GenerateRandom method of KMS can be used to add more entropy to the enclave. While not critically important – enclaves already have access to high quality entropy from the hypervisor – additional randomness may increase trust in the system. On the other hand, one may argue that the added complexity exceeds the benefits. No strong opinions here. Passive attack prevention Threats to the enclave-KMS communication can be divided into two categories: passive and active. Passive attackers can observe traffic and modify data that is stored outside of the enclave and is not attested (data at rest). Active attackers can additionally modify all traffic coming in and out of the enclave (traffic on the network). The exact landscape of passive attacks depends on specific system design, but KMS operations allow us to reason about them fairly well, as an attacker can control any and all of the inputs to these operations. This tl;dr checklist helps avoid passive attacks: Requests to KMS always contain the Recipient parameter. Encryption context is used for supported operations. Context is decided by enclaves, and is not fully attacker-controlled. Encrypt and GenDataKey operations are authorized properly. Data encrypted with data keys has context. Key commitment is considered. Correct CMK is used. CMK ARN is hardcoded. keyId from response is checked. Decrypt requests always specify key ID. IAM role is attested. Full ARNs are used, key aliases are not used. Freshness/replay attacks are mitigated. Side-channel attacks are considered. Key types and cryptographic algorithms are validated. The Recipient parameter includes attestation, which allows KMS to validate PCRs. If key policies are correctly configured, requests without this param fail, so it is rather hard to miss. A single CMK key can be used to generate multiple data keys and shared secrets. Since the encrypted data keys are stored outside of the enclave, an attacker can swap them. It is therefore important to cryptographically distinguish the ciphertexts, and the encryption context is one of the ways to achieve that. Importantly, this solution works only if the attacker does not have full control over the encryption context; if they do, they can swap the ciphertext blob while also making the enclave use the wrong context. Below are diagrams for simple “data swap” attacks that encryption contexts can prevent. Attack A t t a c k e s r s t ( ( t o E E o r , 2 i r e C , n e ( ) C s ( E 2 t E 2 D ) e , , a a C C t d = 2 a e = o n e s f c n w ( c a ( d ( p E k d , , k a C P 2 t ) ) , t E ) P a n 2 c c ) k l ) a v e G G { D D e { e E e e n E n 2 c c e = e = r d r d r e r e y e y e a n a n p c p c t c t c t ( t { ( e ( e ( ( d ( d d D c D c c k c k k a m a m m { , m 2 2 t k t k k d C k } , a , a , _ k ) _ C K d K d i } i 2 e k e k d d ) y ) y 2 , , ( , ( ) E E c d c , ) P 2 m k m d ) k } k k P _ _ 2 2 i i } d d ≠ ) ) P K M S Prevented A t t a c k e s r s t ( ( t o E D E o r , a 2 i r e C t , n e ( ) a C s ( E 2 t E 2 s ) e , , w a C C a d = 2 p e = o n e a f c n t ( c t ( d ( a E k d c , , k k C P 2 ) ) , p E ) P r n 2 e c ) v l ) e a n v t e G G { D e D e { e E e d e n E n 2 c c e = e = r d r r e r e y e y a n a n p c p t c t c t ( t f e ( e ( ( d ( a D c D c c k c i a m a m m { , m l t k t k k d C k u a , a , _ k ) _ r K d K d i } i e e k e k d d y , y 2 , , ( E ( , E E c C c E , P 2 m 1 m C E , k ) k 2 C E _ , _ ) 1 C i d i , ) 1 d k d d ) , } , k E E 2 C C } 1 2 ) ) K M S Figure 3: Simple data swap attack and prevention. Passive attackers that can call Encrypt (or ReEncrypt) on a CMK can perform an even more severe version of the attack above and swap the DK-ciphertext pair with a custom one, effectively providing arbitrary plaintext to the enclave. The same issue applies if an attacker can call GenerateDataKey. Note that some cases may require authorization to these operations for non-enclave entities, but this authorization should be revoked after the initial setup. A t t a c k e s E { r t ( n E ( o E c 2 E i r , r = C 2 n e C y e 2 , s ( ) p n = C t E t c e 2 e , D ( ( n ) a C a c c c d = t m m ( e a k k d o n _ , k f c s i d 2 ( w d k , ( d a , 2 P E k p d , 2 , , k E ) C P a 2 C ) ) t , 1 ) t E ) E a C } n c 1 c k ) l a w v i e G { t D e E h e n = c e e E r d r n n y e a c c p c t ( r t ( e c y ( d D m p c { k P a k t m d 2 2 t , k k , a d _ 2 C ≠ K k i } 2 e , d ) P y E , ( C E c 1 2 m ) , k , E _ d C i k 1 d } ) , E C 1 ) K M S Figure 4: Data swap attack with Encrypt operation. The attacks we’ve discussed so far have been on the “envelope” level. Similar issues exist on the DK level if a DK is used multiple times (though this rarely happens). These issues should be solvable with correct encryption context implemented via AAD. Attack A t t a c k e r ( ( E E s , , i t C C n o ) 2 s r ) t e D e ( K a E d , a C t o , t f C a 2 c ( ) k E , C ) E n c l a v e G D D e { e e n E c c e = C C r d r d r e = 2 y e y e a n e = p c p c t c n e t ( t ( e ( c n ( d ( d D c ( c c k c k P a m d ( m { , m { , 2 t k k d k d C k d C a , , k _ k ) _ k 2 ≠ K d P , i } i } ) e k ) P d d P y ) 2 , , ( , ) E E c d ) P ) m k k } _ i d ) K M S Prevented A t t a c k e r ( ( E E s , , i t E E n o C C s r , , t e C D C e ( ) K 2 a E ) d , a C t o , t f C a 2 c ( ) k E , p E r C e , E v C n e ) c n l t a e v d e G D D e { e e n E c c e = C C r d r d r e = 2 y e y e a n e = p c p c t c n e t ( t ( e ( c n ( d ( d D c ( c c k c k F a m d ( m { , m { , A t k k d k d C k d C I a , , k _ k , _ k 2 L K d P , i } E i } , U e k , P d C d E R y ) E 2 , ) , C E ( , C , E E ) c d ) E ) ) m k C k } 2 _ ) P i d ) K M S Figure 5: Attack on a reused DK and proposed prevention. Some funky attacks are possible if an algorithm without key commitment property is used with data keys: an attacker can generate a single ciphertext that correctly decrypts under different keys. Though this is unlikely, the key commitment should be considered as part of a security audit. A t t a c k e s E { E { r t ( n E n E ( o E c 2 c 3 E i r , r = r = C 2 n e C y e y e 2 / s ( ) p n p n = E t E t c t c k 3 e , D ( ( ( ( e , a C a c c c c y E d = t m m m m – C e a k k k k c 1 o n _ , _ , o , f c s i d i d m C ( w d k d k m 2 ( d a , 2 , 3 i ) E k p d , d , t , , k E k E – E P w 2 C 3 C e C ) i , 1 , 1 n 1 ) t E ) E ) c , E h C } C } ( C n 1 1 d ) c k ) ) k l e 2 a y , v d e G { c k D e E o 3 e n = m , c e e m P r d r n i 2 y e a c t , p c t ( m P t { ( e c e 3 ( d d D m n ) c k k P a k t m 2 2 2 t , k / / / a d _ d d P K k i k k 3 e , d 3 3 y E , } , ( C E C c 1 2 2 m ) / ) k , E _ d 3 i k , d } E , C E 1 C ) 1 ) K M S Figure 6: Lack of key commitment may allow an attacker to select plaintext by providing a different encryption key (E2/E3) dynamically, if ciphertext (C2) must be pre-selected. The next class of attacks is when the host can select CMK that enclave uses. The exact nature of the attack depends on specific degrees of freedom, but in the worst case, the host can force the use of a completely unprotected CMK. To protect against these attacks, the enclave must ensure the expected CMK is used; this can be done by hardcoding full ARN, so it is attested. Then the attested ARN must be provided as the optional keyId parameter in Decrypt requests, and validated against keyId from KMS responses. Note that the keyId param is optional, because CiphertextBlob includes a reference to the CMK as metadata (HBKID in Appendix A): the metadata is not cryptographically protected, and the attacker may be able to manipulate it. A t t a c k e D r c c e m m c k k s r d _ _ t y e i i o p c d d r t ( C ? 2 e ( d M ( c k K E m { , , k d C s C _ k ) u ) i } b d s 2 t , i E P t ) u t E i n o c n l a a v t e t G a e { c n E k e = C r e = a n e t c n e ( c D c ( a m d t k k a 2 , K , P e d ) y k ( ) c , m d k k _ } i d 2 ) K M S Figure 7: CMK substitution attack. Using key aliases instead of ARNs is possible but risky, as the aliases are more ambiguous. Specifically, an attacker can manipulate the enclave’s IAM credentials to trick the enclave into using the wrong AWS account or AWS Region and therefore a wrong CMK. That’s why we recommend attesting the IAM role that the enclave must use and validating that role against IAM credentials provided at runtime. The enclave can do this by calling sts:GetCallerIdentity. Replay attacks are an interesting attack vector. Attestations include timestamps that KMS validates to be at most five minutes old. While this means old documents cannot be replayed, there is still a time window when a malicious host can observe a document and use it multiple times. As attestations are not cryptographically bound to the requests, the attacker can use the attestation with any supported operation with arbitrary params. Although the responses are encrypted with the attestation’s public key and cannot be decrypted by the attacker, this gives the attacker some abilities that must be considered during an audit. For example, an attacker can request multiple decryption with different CMK keys and later use the KMS responses to confuse the state machine of the enclave. Note that the user_data and nonce fields from attestation documents are not used by KMS at all. Even when an attacker cannot observe exact traffic exchanged with KMS, the attacker can note times, orders, and sizes of communication. This may be used to deduce some information, depending on the specific protocol your enclaves implement. Finally, requests and responses to KMS include many key specifications and algorithm identifiers (CMK KeySpec, attestation’s KeyEncryptionAlgorithm, Decryption operation’s EncryptionAlgorithm, for example). Ideally these must not be attacker-controlled in requests (e.g. are bundled in EIF) and the identifiers from responses are checked against the expected ones by the enclave. Active attack prevention As a reminder, active attackers can additionally modify all traffic coming in and out of the enclave. This tl;dr checklist helps avoid active attacks: Active attacks are prevented with enclave-initiated TLS. TLS CA is bundled inside the enclave (attested). VPC is used. Many problems may arise when active attacks are in scope. Most importantly, the attestation and its pubkey are not bound to other parts of the request. This allows the attacker to change the CMK ID in requests and responses (even if the ID is bundled in EIF); to encrypt any data key under the attestation pubkey and use it for replays; or to attack not-authenticated AES-CBC encryption in CiphertextForRecipient responses. CMK substitution E n c l a v e G ( { e c E n m _ e k a d r _ C , e a i M E c t d K _ ( e , d a D a s k t d a t u } t k t t b e a e s s K s t t e t i _ y _ t p p u r u t i b i v ) o , A n E t _ t a a ) c k e r G ( { D e c E E e n m _ _ c e k a d r r _ = k y a i e = p t d n e t e 2 c n ( D , ( c c { a a a ( m d t t t c k k a t t m _ } K e e k i e s s 2 d y t t , 2 _ _ d , p p k E u u ) _ b b } d ) , k d ) k ) , K M S Data key replay E n c l a v e G ( { e c E n m _ e k a d C r _ D , e = a i a E c e s t d t _ ( n t e , a d a c o D a k t d ( r a t k } t k d e t t e e k ( a e y s , E K s t P _ e t r _ ) d y _ e p k p p r , u l i C b a v ) ) y , A E t a _ t t a a t ) c a k c e k r d E E k _ _ = a d r = k a e = n n r d c a o ( n m a d ( t o ) t m e ( s ) t _ p u b , d k ) K M S Figure 8: Active attacks on CMK and DK. These vulnerabilities are basically unsolvable without a secure communication channel. Therefore, TLS initiated inside the enclave is required if active attacks are in scope. For the enclave-initiated TLS solution to be secure, the enclave’s CA set must be limited; ideally, the KMS’ CA certificate (Amazon’s) is attested and pinned. With this setup, the active attacker threat may be considered prevented. Note that having a secure communication channel implicitly prevents some of the possible vulnerabilities described in the “passive attacks” section. KMS terminates TLS outside of HSM (most likely), and the attestation’s pubkey encryption is probably done outside of HSM. This makes it impossible to have an end-to-end TLS channel between enclave and HSM, and AWS insiders may theoretically constitute an active attacker threat. Your threat model should account for this possibility. To further protect the communication channel, VPC can be used. This ensures that traffic never leaves AWS infrastructure and generally isolates the parent EC2 at the network level. Moreover, key policy can authorize requests based on the VPC. This makes attacks easier to detect in case of stolen IAM credentials; this is valuable even if key access is authorized via PCRs, as demonstrated in the previous sections. KMS policies Correctly authorizing access to CMK keys is critical. The list below includes basic checks for your KMS key policy. AWS’ recommendations for IAM policies provides more generic advice. Configured KMS policy authorizes enclaves in a reasonable way. No unexpected IAM roles have or can get access. PCR0 is used for authorization. PCRs 1-2 are used for defense in depth. Alternatively, PCR8 is used. Principal for RecipientAttestation is not a wildcard. PCR3 is used to restrict by EC2 IAM role. kms:EncryptionContext condition is used when relevant. For critical key operations (e.g., deletion) the policy requires MFA. TLS and VPC restrictions are considered. For end-to-end security, the clients can verify that the enclave uses correct and properly secured KMS keys. Immutable key policies are likely not possible, and clients must be aware of this. Of course, the exact CMK policy setup is business-dependent. Generally, you should ensure that the key can be managed only by the expected IAM principal, and the principal doesn’t have access to Decrypt operation (and possibly others like GenDataKeys and Encrypt). The figure below shows an interesting example of a vulnerable key policy that violates the “only expected IAM principal” check. One may assume that only the root user and the enclave can operate on the key, but this is incorrect: the first policy entry grants full access to any IAM role that has access to the key configured in the role’s policy. The fix is to use a specific IAM user or role instead of root or to add an explicit deny statement for non-root users. [ { “Sid”: “Enable IAM User Permissions”, “Effect”: “Allow”, “Principal”: { “AWS”: “arn:aws:iam::599412696120:root” }, “Action”: “kms:*”, “Resource”: “*” }, { “Sid”: “Allow Nitro Enclave KMS operations with PCR0 lock”, “Effect”: “Allow”, “Principal”: { “AWS”: “arn:aws:iam::599412696120:role/NitroEnclaveKMSRole” }, “Action”: [“kms:Decrypt”, “kms:GenerateDataKey”, “kms:GenerateDataKeyPair”], “Resource”: “*”, “Condition”: { “StringEqualsIgnoreCase”: { “kms:RecipientAttestation:PCR0”: “00a119d1…0ed55” } } } ] Figure 9: Example policy that is likely to be insecure. For the PCRs, you want to use PCR0, as it binds the policy to specific enclave code. Additionally, using PCRs 1-2 is recommended for the reasons stated in our blog post on the Nitro Enclaves attack surface. Alternatively, you can use PCR8, which allows updating the enclave code without needing to update key policy. This allows more restricted access to key policy modification permission at the cost of managing the signing key. The Principal field and PCR3 measurement provide further restrictions. Principal is used to authorize the IAM role used to access KMS, while PCR3 is measured by hypervisor at the time of enclave launch based on EC2 role. The EC2 role can be dynamically changed and should be considered untrusted from the enclave’s perspective. Yet both Principal and PCR3 can be used to prevent attackers from running (signed) enclaves on their own EC2 instance (which could make side-channel attacks easier) and accessing the KMS key. Access to the key can be further improved with TLS and VPC restrictions. VPC can be enforced with aws:SourceVpc and similar condition keys. TLS can be enforced with the aws:SecureTransport condition (although this condition is redundant, as it’s not possible to access the KMS API with plain HTTP). As the key has to be manageable by some IAM role (at least to allow key deletion), the aws:MultiFactorAuthPresent and aws:MultiFactorAuthAge conditions can be used to strengthen the authorization. KMS policy end-to-end verification So far, our discussion has focused on how to secure the KMS keys. A much more difficult problem arises when you want your system to provide end-to-end verifiability to end-users. If enclaves can be reproducibly built and remotely attested by users, then users likely have to validate that the KMS keys are properly protected, too. Otherwise, a malicious insider can pass remote attestation (not modify enclave code), yet use KMS directly with IAM permissions to get full access to the keys. One solution is to hardcode the hash of the key policy in the enclave, provide full policy along with enclave’s code to clients, and make the enclave validate the hash against the dynamically obtained policy before sending attestation-protected requests to the KMS. This requires the enclave to have kms:GetKeyPolicy and kms:DescribeKey permissions. This alone doesn’t prevent attacks. A malicious IAM user can dynamically change the policy after the enclave’s verification. To prevent this, the policy has to be made immutable, which can be achieved by blocking kms:PutKeyPolicy permission for all users. Note that –bypass-policy-lockout-safety-check flag is required to insert such a statement via CLI. { “Sid”: “DenyPutKeyPolicyForAll”, “Effect”: “Deny”, “Principal”: { “AWS”: “*” }, “Action”: “kms:PutKeyPolicy”, “Resource”: “*” } Figure 10: Example policy that prevents key policy changes. Locking access by PCR0 and denying all kms:PutKeyPolicy operations makes the system quite immutable. This has the obvious downside of making updates and bug fixes difficult. As mentioned earlier, the specific setup must be adjusted based on business requirements. Note that key owners can always contact AWS support to restore default key policies. How AWS authenticates such requests I do not know, but AWS likely won’t check if the key is used in an enclave-enabled setup. This makes a system with full end-to-end trust hard to implement. For example, suppose you create a key policy that gives only one user access to the KMS key. If you then delete that user, the key becomes unmanageable and you must contact AWS Support to regain access to the KMS key. Figure 11: Quote from AWS documentation. Finally, consider implementing publicly observable and verifiable monitoring and alerting for key policies. Such a system would alert end users when a policy changes, mitigating the impact of policy restoration by AWS support. However, we are not aware of any “Certificate Transparency”-style public, append-only log for KMS key policies that an external party can independently verify. Operational concerns Even if the system is secure point-in-time, there are operations that must be periodically performed. These introduce new risks into the system. This checklist covers these concerns: Key rotation and revocation is implemented for CMK. ReEncrypt operation is not used for data keys. Backups: Risks from CMK destruction are mitigated. Regional outages are considered. Data keys are backed up as needed. Users cannot cause a denial of service or balloon the bill. The number of user-triggered KMS operations is limited. Request quotas are considered. Limits on data lengths are respected. KMS’s clients take into account delays in KMS updates. AWS provides mechanisms to easily rotate CMK keys. The only item to note here is that rotating a compromised CMK does not make data keys protected by it non-decryptable. For a CMK revocation, a more involved approach than just rotating CMK and destroying data keys must be implemented. Rotating data keys is hard to implement securely, as the KMS ReEncrypt operation does not support attestations. The system should be designed so that such rotations are not needed. A malicious actor deleting CMK keys permanently creates a risk of non-recoverable system state. The system’s design can sometimes be made so that destruction of a single key is recoverable (e.g., by setting up key hierarchy and using secret sharing). Nevertheless, there should be security controls in place mitigating the risk. First, configure a scheduled deletion period for keys to a time in which your team can act on an incident. Set up CloudWatch alarms for KMS keys for deletion events, and tighten IAM policies with Service Control Policies that prevent KMS key deletion. Single-machine disasters in AWS infrastructure are not a concern, as single-region KMS keys are replicated within the region in multiple Availability Zones in multiple HSMs. However, if the system must be resilient to a regional outage, multi-region keys should be used instead of single-region keys. Encrypted data keys backups are a responsibility of the system, not AWS. Note that the CMK key may become unusable in a few scenarios, and the data key backup system must account for this. Yet another set of risks relates to billing. AWS charges dollars per KMS operations and CMK key maintenance, so the system must not let end-users make the enclaves send arbitrary many requests to KMS. When implementing rate-limits, KMS quotas must be taken into account. Inputs to KMS have various size limits. For example, plaintexts can be up to 4096 bytes long, ciphertexts can be up to 6144 bytes long, and key IDs can be up to 2048 bytes long. These limits are unlikely to be reached with attestation-supported operations, but still should be considered. Finally, changes to KMS resources need some time to propagate and synchronize inside AWS infrastructure. Your system must expect delays and possible temporary inconsistencies when requesting KMS. Software and SDKs Amazon ships a lot of SDKs for various tasks. Among them is aws-nitro-enclaves-sdk-c that provides tools and a library for enclaves-KMS communication. Avoid it: this particular SDK is written in C, and we found it contains vulnerabilities that can be used to exploit enclaves from the parent host. Rather than using the aws-nitro-enclaves-sdk-c, we recommend a combination of other libraries, such as the following: aws-nitro-enclaves-nsm-api (in Rust) to get attestation documents KMS.Client from Boto3 (in Python) to communicate with KMS Any cryptographic library to parse and decrypt responses Final notes Many issues can arise from misusing the KMS within enclave-secured systems. This blog post does not even cover all supported operations (GenerateDataKeyPair, DeriveSharedSecret), possible vulnerabilities (key reuse, key wearout, forward secrecy, nonce management, …) and system features (custom key stores, multi-region keys, …). Make sure to document your system’s protocol, have a cryptographer review it, and check the actual implementation against it. Appendix A Data formats of the CiphertextBlob and CiphertextForRecipient structures are presented below. [ [ [ [ [ [ [ 0 4 3 3 3 5 5 : : 6 7 8 4 8 4 3 ] ] : : : ] 6 5 5 ] ] 4 8 ] ] V H A T K C C O ├ └ e B l y D M M I ─ ─ r K g p F S S D ─ ─ s I I e i D d F n l E 1 v E ├ ├ ├ │ │ └ o l o e n . e n ─ ─ ─ ─ n a n n c 2 r c ─ ─ ─ ─ g c g r . s r s e t y 8 i y c a G ├ └ [ └ h p 4 o p o l C ─ ─ 0 ─ N t 0 n t n g M ─ ─ ] ─ e . : e t o P d 1 d e r a I I I c ( e e D 1 0 C n i r V C M i p . . a 3 o t t a : V P p l g g 0 3 N b 0 1 b t 5 n T h m l L h a . . 1 2 O 3 1 6 i a 4 t y m e e I e i T g 9 e p : t n C r n 3 1 0 b b – ( . n e e : I t t 2 2 2 y S ( ( y e D 1 t : r T e e B 1 t H a k t n E . I s x x 8 0 e A l e e d R 7 n 1 2 e t t d B 3 s – g y s i ) . f . . n k , 2 o , a 6 o 2 1 1 1 c R 0 5 r t n . 6 2 6 r S 0 p 6 i y r 8 . y 1 → A r ( t p a u ( 4 8 b p 1 1 – o C h e n 3 p 0 4 y ( t 6 4 2 p M m d 2 k . 0 t 1 e – b 3 0 r K / o c 1 . e 2 d b y B 4 i i m ( s 1 1 s 8 C y t 8 e A d f e 7 3 . – o t e c t R e l p . – 5 1 ( b n e s t d a N n a e g e 4 0 r i t e r ) t g r . n 9 1 a t e G + r y , i s – c . . n n C v f ) c 0 r 1 3 d a t M e 1 → N i a x y . . o u r 6 O e l 0 p 7 4 m t t h B c T r l 0 t . . , h a e o ) 0 e 1 1 e g a t r d 0 d . i n d a r e 0 D 4 n t g e r 0 a ( 6 d i p s i 7 t p e c e = p v e a k p a r o a ) c ( e t 5 n b = s a n i b 9 d l 7 e d o l B i e 1 – s e n o n 2 d – n b g f 6 a 2 t t ) l r t 5 a y o f a 6 o g m o ) – f ) l r g a H c N r B A m ) g K E ) e / S r A – R 2 N 5 / 6 U U d I k D ) Figure 12: KMS CiphertextBlob. One cannot decrypt its content manually because the KDF label is not public. HBKID (HSM backing key ID) is mapped to CMK ARN internally. C O ├ ├ │ │ │ │ │ │ │ │ │ │ │ │ └ M I ─ ─ ─ S D ─ ─ ─ E 1 v r └ e ├ ├ │ └ n . e e ─ n ─ ─ ─ v 2 r c ─ c ─ ─ ─ e . s i r l 8 i p K ├ ├ │ ├ │ │ │ │ └ y c a └ [ └ o 4 o i e ─ ─ ─ ─ p o l ─ 0 ─ p 0 n e y ─ ─ ─ ─ t n g ─ ] ─ e . : n T e t o d 1 t r v r k ├ ├ └ h e d e r p I A D 1 2 I a e i e ─ ─ ─ a n C n i a M E a 3 n n r d y ─ ─ ─ s c o t t r P S t 5 f s s : E h r n T h a L – a 4 o R i n R R R : y t y m m I 2 9 s e o S = c S S S p e p : s C 5 . c n u r A A A S t n e : I 6 1 i : b S y E E E H e t : a T – . p j H p S S S A d I e { C 7 i 2 e A t _ _ _ – K n 1 s e B . e c – i O O P 2 e f . – I n C 3 n t 2 o A A K 5 y o 2 2 V c t K 5 n E E C 6 : . 5 : r c I e 6 A P P S , 8 6 y i ( n y ( l _ _ 1 2 3 5 4 – 1 p p p f I a g S S _ m 5 8 1 0 c 6 t h k o d t o H H V g 6 4 2 . b e e c e t r A A 1 f 1 c b d r s n e i _ _ _ : b b b 1 y C t 7 t s t 2 1 5 y y y 3 t o e – i t h 5 M t t t 5 e n x e f a m 6 G e e e 4 s t t n i t F s s s 9 e v e i ( ( 1 . } n o e r o ( a a – f f 1 t f l n d c c S ( o o . o e c c H R r r 7 t p ( R f e e A S . h e 3 S a p p – A R R 1 e d 2 A u t t 2 – S S D l e e 5 O A A p a b p t d d 6 A – – ( l t y u ) ) ) E 3 4 p a a t b P 0 0 k i ) e l ( 7 9 c n s i f e 2 6 s t ) c o n 7 e r c → → – x k → → → r d t e O y C C a y C C C A p f f t k f f f E t R R a e D R R R P e ) y E _ d = = R = = = S m ) H C 6 7 a 4 4 4 A E 2 4 t 9 4 4 _ K 1 9 e ← 3 6 4 2 ) B B r B B B 5 i v 6 a e w w w ) l r / / / i f R R R i S S S e A A A d – – – 2 2 2 0 0 0 4 4 4 8 8 8 Figure 13: KMS CiphertextForRecipient. Note the use of AES-CBC.

Uniswap v4 hooks let developers add custom behavior to pools, including dynamic fees, custom accounting, and external integrations. This flexibility moves some security responsibilities into application and hook code. The Cork and Bunni exploits are two app-level incidents that show what can go wrong in that code. Together, they account for more than $20M in losses. Neither incident stemmed from a flaw in the Uniswap v4 core protocol or the PoolManager; both arose from application-specific authorization and accounting logic built around hooks. After analyzing dozens of findings from Trail of Bits audits (including our Uniswap v4-core security review), public reports from other firms, and the Solodit database, I’ve identified seven recurring failure patterns in application and hook code, including missing caller checks and accounting bugs that still satisfy the PoolManager’s settlement invariant. Builders can use these patterns as a secure-development checklist; auditors can use them to focus their review. What the PoolManager guarantees If you’re familiar with Uniswap v3, where each pool was a separate contract, v4 inverts the model. All pool state now lives in a singleton PoolManager contract, with each pool represented in its storage. Uniswap v4 adds hooks: independent contracts that execute custom logic at specific points in the swap and liquidity lifecycle. Figure 1: Pools live inside the singleton PoolManager, and multiple pools can use the same hook contract. Here’s what a pool looks like in v4: struct PoolKey { Currency currency0; Currency currency1; uint24 fee; int24 tickSpacing; IHooks hooks; } Figure 2: A pool’s PoolKey includes both currencies, the fee, tick spacing, and the hook address (v4-core/src/types/PoolKey.sol). Notice that the hook address (IHooks hooks;) is part of the pool’s identity. If you change any of these fields, you’re talking to a different pool. This matters because trusting the wrong PoolKey means trusting the wrong pool. v4 also introduces a session-based model that works like a flash loan. Your contract calls unlock() on the PoolManager, which triggers a callback into your code. At the end, the PoolManager checks that no unsettled currency deltas remain: function unlock(bytes calldata data) external returns (bytes memory result) { Lock.unlock(); // … callback execution happens here … if (NonzeroDeltaCount.read() != 0) revert CurrencyNotSettled(); Lock.lock(); } Figure 3: Simplified PoolManager.unlock() flow: unlock the session, execute the callback, and revert unless all currency deltas settle to zero (v4-core/src/PoolManager.sol). Figure 4: A periphery or hook calls PoolManager.unlock(), handles unlockCallback(), and calls swap() inside the unlocked session. The PoolManager enforces v4’s protocol mechanics, including pool initialization rules, swap and liquidity math, hook-callback sequencing, and end-of-session settlement. Hook developers are responsible for validating the application-specific assumptions their hooks add. Each hook must decide: Who can call its privileged paths Which pools are legitimate How custom balances and deltas should be accounted for Whether external integrations can fail or reenter safely 1. Anyone can call your hook Hook callbacks are external functions on your contract. If you don’t check the caller, an attacker can call those callbacks directly with malicious parameters. A loose unlockCallback path can also reach internal actions that should never be callable. The fix: use BaseHook for hook entrypoints and SafeCallback for unlockCallback. Together, they enforce caller checks on the callback paths they cover: modifier onlyPoolManager() { if (msg.sender != address(poolManager)) revert NotPoolManager(); _; } Figure 5: onlyPoolManager restricts hook callbacks to the configured PoolManager. Add an equivalent caller check only on paths those contracts don’t cover. Real-world example: The Cork exploit (~$12M, May 2025) shows why this check matters. Cork let data from an untrusted path reach hook logic that affected redemptions. That access-control gap, combined with a pricing issue elsewhere in the protocol, gave the attacker a way to drain funds. 2. Treating any pool as legitimate Pool creation through the PoolManager is permissionless by default. Unless your hook restricts initialization in beforeInitialize, anyone can create a pool with your hook address attached. If your hook trusts a user-supplied PoolKey without validation, an attacker can route your logic through a malicious pool with currencies and parameters they choose. An attacker-created pool presents two immediate risks. First, if your hook stores per-pool data keyed by PoolId, the new pool gets its own mapping slot. The attacker can influence values written through activity in that pool, and later accounting paths may treat those values as trusted. Second, currency0 and currency1 are attacker-chosen currencies. If either is an ERC-20, token interactions can trigger malicious behavior or reenter other hook functions mid-flow. The fix: bind your hook to canonical pools during deployment or trusted configuration, or maintain a strict allowlist. Re-check the derived PoolId on every user-controlled path: // Pseudocode for pool binding PoolId poolId = key.toId(); if (!allowedPools[poolId]) revert InvalidPool(); Figure 6: Derive the PoolId from the supplied PoolKey and reject pools that are not allowlisted. Real-world example: In Semantic Layer’s SVFHook finding, the addLiquidity function lets callers specify the PoolKey. An attacker could route deposits through a custom WETH/SVF pool with a malicious hook and earn points at a lower cost than intended. 3. Custom accounting leaks value In v4, a delta is a signed currency-balance change owed to or from the PoolManager. Once your hook touches deltas, a wrong sign, a rounding error, or mixing balance buckets can silently leak value. These bugs are subtle because settlement only checks that the session’s currency deltas resolve; it does not validate the hook’s internal accounting. A hook’s accounting can still be wrong even when settlement succeeds. Return-delta hooks can move beyond fee bookkeeping. If a BeforeSwapDelta consumes the user’s entire specified amount, the PoolManager has no amount left for its concentrated-liquidity swap; the hook supplies the trade instead. This is often called a NoOp swap. Treat that hook as a custom AMM: test conservation, price bounds, rounding, and returned deltas against real balances. Dynamic fees are also price-sensitive. A dynamic-fee pool can accept a per-swap fee override from beforeSwap, and its hook can update the stored LP fee. Bound every fee, limit how quickly privileged changes can move it, and do not derive it directly from inputs an attacker can cheaply manipulate. For hooks that move value, test at least these three accounting invariants: No user receives output that the accounting did not charge for. A same-transaction round trip cannot create value from accounting alone. Internal accounting matches actual asset balances. Those invariants must also hold for the tokens the hook handles. Fee-on-transfer tokens can make the amount received smaller than the amount sent; rebasing tokens can change balances without a transfer; callback-enabled tokens can reenter; and pausable or blacklistable tokens can block settlement. State which behaviors you support and test accounting against observed balance changes. The fix: keep LP funds, fees, and incentives in separate buckets. Label every balance and delta, including who owns it, and who can move it. Real-world example: The Bunni exploit ($8.4M, September 2025) was a rounding bug in BunniHook’s idle-balance accounting. The attacker pushed a pool’s price tick with a flash loan, then made 44 tiny withdrawals that each shrank the active balance disproportionately to the shares burned, eventually extracting profit from the affected pools. Each transaction satisfied the PoolManager’s settlement invariant because the bug was in BunniHook’s internal accounting. 4. Right logic, wrong hook Figure 7: PoolManager runs beforeSwap before executing the swap and afterSwap afterward when the corresponding address flags are set. The beforeSwap hook executes with pre-swap state, but the afterSwap hook sees post-swap state. Code that’s correct in one hook can be unsafe in another. The same timing problem affects liquidity callbacks. In this LiquidityPenaltyHook finding, a JIT-liquidity penalty was computed during afterRemoveLiquidity, but a user could first make a tiny liquidity increase that collected the fees separately. By the time removal ran, the hook saw no fees left to penalize. In our hook audits, we’ve repeatedly observed developers put logic that needs the final swap result in beforeSwap instead of afterSwap. The code looks correct in isolation, but it’s operating on stale data. The fix: verify your logic is in the correct hook for the state it needs. 5. Address bits are part of the API In v4, the hook address itself encodes which hook functions the PoolManager will call. This design makes the deployed address part of a hook’s API, so developers must keep its permission bits in sync with the functions they implement. function hasPermission(IHooks self, uint160 flag) internal pure returns (bool) { return uint160(address(self)) & flag != 0; } Figure 8: hasPermission reads callback permissions from the hook address bits (v4-core/src/libraries/Hooks.sol). Three permission mismatches can cause problems: Callback bit set + callback missing → transaction reverts. Callback implemented + callback bit missing → PoolManager does not call it. Return-delta bit missing → PoolManager may call the callback but treat its returned delta as zero. For example, if the afterSwapReturnDelta bit is missing, your hook might record a fee even though the PoolManager ignored the returned delta. Address bits do not make the hook’s behavior immutable. If a pool’s hook address points to a proxy, the permission bits stay fixed while an upgrade can change the code reached through that address. Review the upgrade admin, delay, storage layout, and implementation checks as part of the hook’s security boundary. Prefer immutable, versioned deployments when possible. The fix: inherit from BaseHook and keep getHookPermissions() in sync with the callbacks and return deltas your hook actually uses. BaseHook validates that the deployed address bits match those declared permissions. Real-world example: In the Sorella Angstrom finding, the hook returned a non-zero delta for the dynamic protocol fee, but hook-config.sol did not encode the afterSwapReturnDelta permission. The PoolManager wasn’t authorized to settle the delta, so every swap reverted with CurrencyNotSettled() once the fee was enabled. 6. Hook failures can block pool actions Hook callbacks execute in the same transaction as the pool action. If reward distribution, dust cleanup, or other non-essential code reverts inside an afterRemoveLiquidity callback, users cannot exit their positions. The same applies to swaps when non-essential code reverts inside afterSwap. The PoolManager preserves atomic execution by reverting the parent action, so hook developers must keep optional logic from blocking core user flows. Required external reads can cause the same denial of service. If a price feed rejects stale data, a lending protocol pauses, or another dependency reverts, the callback can revert the user’s swap or withdrawal. For each dependency, decide which paths must fail closed and which can degrade without blocking safe exits. Never silently use stale pricing data. External calls are not the only source of failure. In our hook audits, we’ve seen happy-path accounting block withdrawals because of a zero balance, decimal mismatch, or missing reward token. The fix: keep non-essential code out of the main user flow. Wrap optional external calls in try/catch, or move optional logic to a separate function users can call after exiting. For safety-critical dependencies, validate freshness and bounds, and provide an explicit exit-safe fallback when the design permits one. 7. State can change during a callback sequence When enabled, beforeSwap and afterSwap run during the same swap, but values cached between them are not automatically safe. A hook can call external contracts, and one hook contract can serve many pools. Nested actions can therefore change shared hook storage, pool state, balances, or oracle data before the outer callback sequence finishes. The fix: avoid shared scratch state. If data must cross callbacks, key it by PoolId and caller, reject overlapping operations while that state is live, and clear it after use. Apply checks-effects-interactions before external calls, and test nested swaps and liquidity changes across multiple pools that share the hook. Building secure hooks If you’re developing a v4 hook, verify these eight items: Gate every callback and unlock path: Use BaseHook for hook entrypoints and SafeCallback for unlockCallback. Add equivalent caller checks only on uncovered paths. Allowlist pools, not just tokens: Bind to specific PoolKey values or maintain strict allowlists. Label every balance and delta: Document who owns it, who can move it, and which token behaviors the accounting supports. Keep LP funds, fees, and incentives separate: Don’t mix balance buckets. Keep non-essential code away from the main user flow: Reward, oracle, and cleanup failures shouldn’t block safe exits. Verify address permissions: Inherit from BaseHook and confirm that the address bits match your declared permissions. If the hook is upgradeable, review its proxy and upgrade controls separately. Fuzz nested callbacks, fee extremes, malicious pools, and malicious or non-standard tokens: Use Echidna and Medusa to test adversarial scenarios, not just happy paths. Isolate callback state: Key temporary data by PoolId and caller, reject overlapping operations, and clear it after use. Auditing v4 hooks If you’re reviewing a v4 hook, ask these seven questions: Can an attacker call a callback directly? Check every external function for access control. Can an attacker route logic through a malicious pool? Trace how PoolKey values are validated. Who owns each balance and delta, and can a return delta or dynamic fee leak value? Test conservation, price bounds, and fee limits. What happens if reward, cleanup, or oracle code reverts during removeLiquidity? Test failure paths and dependency outages. Do the permission bits, implemented functions, returned values, and any proxy upgrade path all match? Verify the address flags and upgrade controls. What breaks if the hook, token, or fee input is malicious? Assume adversarial counterparties. Can state change between callbacks? Test nested actions across multiple pools that share the hook. Security responsibilities for hook developers The PoolManager enforces v4’s protocol-level guarantees, including pool mechanics and settlement. Hook developers secure the application-specific logic they add, including authorization, pool selection, value accounting, and external integrations. Ask which assumptions the hook adds beyond the PoolManager’s guarantees. For operational guidance beyond code review, see Uniswap’s v4 Security Framework. If you’re building on Uniswap v4 and want help reviewing your hooks, reach out to Trail of Bits. And if you’re interested in smart contract security, check out our public tools and research. This post is based on a presentation I gave at EthCC[9]. You can find me on X at @nisedo_.

Codex’s /goal feature amplifies bug hunting, but getting good results requires the right prompt, the right scope, and the right number of outcomes per run. For Patch the Planet, our joint initiative with OpenAI to find and fix bugs in open-source software, we pointed Codex at some of the most widely used, heavily audited codebases in the world, like Rust, curl, and zlib. One tool came up again and again in our internal bug-report channels: /goal, which hands Codex an open-ended objective and lets it work independently toward a success condition. Here are a few highlights: /goal found every Rust bug we submitted, including a soundness hole and a miscompilation now patched in Rust 1.98, from a single variant-analysis pipeline. It turned every project’s past CVEs into Semgrep rules that had to fire on the vulnerable version and stay silent on the patched one, then flagged 11 variant hits across multiple projects. It uncovered two potential high-severity privilege-escalation bugs in Keycloak’s SAML component during a discovery run. Over the first few weeks of Patch the Planet, our engineers independently converged on three techniques for using /goal. We found that getting the most out of /goal means treating the prompt as a set of specific success criteria, not a set of instructions. (Note that this blog post uses /goal to refer to goal-based prompting in general. Codex can also set goals for itself through a tool call, and that’s how we recommend everyone use it; we rarely type the slash command ourselves.) 1. Let Codex write the goal The art of using /goal is prompt design, and we found that Codex knows Codex the best. Internally, our single most repeated /goal tip was to use Codex to help write each /goal prompt. We hand Codex threat model files and the context about what we’re looking for, and then tell it to write the goal prompt. As mentioned before, /goal is a tool Codex can invoke on itself, and a few engineers stopped typing goals by hand entirely. $goal-prompt based on threat model write goal to find single critical issue (RCE) exploitable by remote attacker for kubernetes-client. the kubernetes-client is used in normal config, malicious remote users exploits. Figure 1: A meta-prompt from one of our engineers asking Codex to create a goal prompt. Results are shown in figure 2. This works because Codex knows the target and its own tendencies better than we can specify up front. It can translate a threat model into concrete, testable success criteria, name the code paths worth prioritizing, and phrase the outcome precisely enough that a run actually converges. A goal written this way tends to be tighter than one we’d write cold, and it takes a fraction of the time. Letting the model draft the goal also closes a gap we’d otherwise miss. Any outcome you define can be satisfied in ways you didn’t intend, and the model is often the first to spot where the easy outs are. Now when we ask Codex to draft a goal, we ask it to red-team its own goal by identifying the ways a future model might be lazy in its approach, and to revise the criteria to remove them before the run starts. We also built tooling that makes it easier for Codex to verify its own work. For example, we noticed Codex has a tendency to skip reading the entire codebase even when explicitly asked. We built aicov, a tool that tracks what lines of code Codex has actually read, so it can’t “cheat.” This is an iterative process. As we find more shortcuts a model takes, we exclude them from the next version of the prompt. 2. Define the outcome, not the path A good goal names the outcome, defines it precisely, and then enforces persistence: /goal Audit the kubernetes-client repository in this workspace to find exactly one previously unreported critical remote code execution vulnerability reachable in normal/default client configuration by a malicious remote user or server that controls only network/API responses, Kubernetes objects the client legitimately fetches, or other remote data accepted during normal use. First build a concise threat model of realistic remote attacker entry points and trust boundaries, then prioritize code paths involving deserialization, YAML/JSON/protobuf parsing, dynamic imports/eval/template execution, archive/file extraction, auth redirects, generated client hooks, websocket/exec/attach/port-forward streams, and subprocess or filesystem effects. Do not assume attacker control of local kubeconfig, CLI arguments, environment variables, installed plugins, source code, credentials, privileged cluster/admin access, or prior code execution; explicitly reject findings that rely on those preconditions. Before accepting a candidate, search local known-findings files plus current open issues/PRs for duplicates, then produce a minimal safe proof that demonstrates attacker-controlled code execution or a direct RCE primitive under the stated normal configuration. Stop after one valid critical issue. Write finding to ./findings/ folder. Figure 2: The prompt created by Codex from figure 1 We found the best philosophy is to spend as many tokens as you need defining the outcome, and almost none telling the model how to get there. If you want the bug found through fuzzing, “use fuzzing” is as far as you should go. “Build on top of my existing fuzzing harness” or “build a new fuzzing harness” are both worse. There might be an existing harness that’s just as good. A goal that prescribes the path guarantees Codex never takes another one, and you lose the judgment and open-ended problem solving that make /goal unique. The outcome side takes more care because it has to be calibrated. If it’s too specific, Codex doesn’t have enough to search and the value of an autonomous /goal run is unclear. When we fed Codex the exact root cause of a known bug and asked it to find variants, it found nothing. The scope was too narrow. When we cut the input down to a single sentence describing the class of bugs it should look for based on the known bug, it surfaced numerous bugs. We reported 9 of them, with 3 already fixed and merged upstream. If an outcome is too vague, the model provides outputs that don’t match what you were looking for. One of the worst /goal prompts we saw during Patch the Planet was “find bugs in [X].” The model had no way to tell when it was done. It just kept running, surfacing bugs that had no real-world impact, and wasting tokens. A complete outcome definition also says what doesn’t count as done. The open-source projects in Patch the Planet have some of the most audited code in the world, and more than once /goal came back with “no bugs found.” We treat that as an intermediate result, not a completion condition, and write persistence into the goal itself. The most effective resource for /goal bug hunting is a THREAT_MODEL.md file. We ended up referencing a threat model file in almost every goal we ran because it precisely defines what valid bugs look like without explaining how to find them. We recommend every open-source project create one. 3. Assign one outcome per agent Putting two competing outcomes in one /goal prompt results in uneven optimization. We ran into this repeatedly when a goal asked for both bugs and coverage. When we put “find bugs” and “achieve high coverage” in the same prompt, the run ended up doing one of them far better than the other. This was our experience while using /goal to audit zlib. Codex kept gravitating to the same part of the codebase, fuzzing the areas the model found first without reaching the rest. Our initial instinct was to fix that in the prompt by adding coverage requirements, but Codex then switched its optimization to coverage, and we saw lackluster vulnerability hunting. What worked instead was moving coverage out of the prompt entirely. We asked Codex to first identify the five most promising attack surfaces after scouring through the entire codebase. Then we created a separate /goal session to find bugs in each section. We also added one fully open-ended session alongside them to roam the parts of the codebase the other agents weren’t assigned. This approach worked drastically better. Figure 3: Rust maintainers assumed we had a team of engineers working on finding bugs. It was just one engineer with a strong handle on Codex’s /goal. One of our engineers, Kevin Valerio, created an automated variant-analysis system for the Rust compiler leveraging /goal. Every Rust bug we submitted through Patch the Planet came out of it. P-critical is a label created by Rust maintainers to identify bugs that should be prioritized to patch and merge. The pipeline began by downloading every issue tagged P-critical in the rust-lang/rust repository as JSON. An orchestrator reads the issues and spawns a separate agent for each one. One outcome per agent: instead of a single session told to perform variant-analysis on each bug, the orchestrator creates one Codex session per issue, each running an independent task to find a single outcome. Each session runs in Goal mode with a deliberately small prompt to find a security issue with the same root cause as the original bug in P-critical. It receives a one-sentence description of the risk rather than an exact root cause with a full backtrace, so the model can still have the freedom to explore the codebase more. Before any variant hunt begins, a security gate asks whether the source issue is even a real vulnerability and routes it to skip, no_variant, or bug_found. We are using that to focus on the most impactful P-critical bugs. Every candidate runs a two-pass false-positive gauntlet. The first judge checks that the bug poses a genuine security risk. The second, a different model entirely, runs a PoC-focused pass and demands that the issue can potentially cause security issues relevant to the Rust threat model. A candidate reaches “validated finding” only if both passes agree. Validated findings pass one last human filter. A duplicate check happens before anything is opened. Only bugs that are confirmed upstream and not already found in GitHub’s issue backlog are drafted for submission. Figure 4: The full workflow Kevin Valerio used to find every bug in Rust Where human judgment is needed Since its release, /goal has been a powerful tool for amplifying the bug-hunting work that we do. Codex can create custom security infrastructure that takes a security researcher weeks to build in under a day. It can scour thousands of lines of code faster than any human can. /goal will faithfully pursue whatever outcome we give the model, which means the run is mostly decided before the model starts. But its effectiveness still depends on an expert knowing where to look, verifying its results count as a reportable finding, and knowing what the maintainers on the other side actually want to see as a valid vulnerability disclosure. Prompt engineering is a large part of it, but you can only write a good prompt if you know exactly what you’re looking for.

We’ve added a new chapter to our Testing Handbook: a comprehensive guide to security testing Rust programs. This chapter covers the tools and techniques we use at Trail of Bits to validate the security of Rust programs and systems. fn main() {(|f:&dyn Fn(u128)->Box< dyn Iterator<Item= char>+’static>|f(*[&( 0x7B736D70683F73u128<<64| 0x7A6A6D7C3F7A667D),&(0x7B736Du128 <<64|0x70683F7073737A77)][((std::hint:: black_box(0.0f64)/0.0).to_bits()>>63)as usize]) .for_each(|c|print!(“{c}”)))(Box::leak(Box::new(|n: u128|Box::new(std::iter::successors(Some(n),|&n|Some(n>>8) ).take_while(|&n|n>0).map(|n|((n as u8)^0x1F)as char))as _)))} What’s in the chapter The chapter starts with a security overview of what Rust’s guarantees do and don’t cover, including underappreciated issues like unwind safety, nondeterminism, and arithmetic errors. This leads into an overview of dynamic analysis, which covers a range of boosters for unit tests, how to use Miri to detect undefined behavior, property testing with proptest, coverage measurement, and mutation testing. The static analysis section then covers Clippy in depth, including a list of our favorite lints. Beyond tooling, the chapter also covers what we’ve learned from auditing Rust codebases directly. Our gotchas and footguns checklist is a great reference for manual code reviews, and will help you find subtle issues like a & b == c having different operator precedence than in C. The memory zeroization section offers three solutions to the tricky problem of guaranteeing that secrets are erased from memory. Finally, the specialized testing sections cover tools like Kani (a model checker), and the supply chain section covers the full toolchain for vetting dependencies. Still oxidizing We’ve also released rust-review, a Claude Code plugin for automated Rust security reviews. Co-built with Aptos Labs, it targets over a dozen bug classes, from memory safety and concurrency hazards to FFI pitfalls and async cancellation issues. It’s a fast way to catch security issues in a Rust codebase before they make it to audit. Our goal is to keep the handbook current as the Rust ecosystem evolves. If your favorite tool or gotcha isn’t covered, submit a PR. And if you need help securing your Rust systems, contact us.

In April we released Mewt, our open-source mutation-testing engine that finds the gaps in your test suite. Today we’re expanding it with support for DAML, the language Canton Network applications are written in. Mewt now reads DAML, generates several classes of mutants (including two built for DAML’s authorization primitives), and runs them through your existing test suite to count how many mutants survive. If you want to try it, simply install Mewt from the repository, point a mewt.toml at your project and its test command, and use mewt run. For a team shipping DAML to production, that count is what a passing test run is actually worth: it puts a number on how much your suite checks, whereas a green run on its own does not. Why DAML’s coverage reports lie Test coverage is the most reassuring lie in smart-contract development. Hitting 100% line coverage tells you the test runner walked the code; it does not tell you whether any test would fail if that code stopped doing what it is supposed to. We have been grading test harnesses by how many mutants they kill since at least 2019, and our primer on finding the bugs your tests don’t catch shows how a green suite can still miss the bug that matters. DAML’s built-in coverage measures execution at the template and choice level: which templates were created and which choices were exercised over the test run. It reports whether each choice was exercised, not what happened inside it. A test that exercises a choice once and asserts nothing about the result reports that choice as covered. The report prints the same green percentage whether the test verifies the outcome or discards it. How mutation testing works Instead of asking whether your tests reached the code, mutation testing grades your tests by sabotaging that code. The engine generates mutants, copies of the code that each carry one small deliberate change: a flipped comparison, a removed branch, a dropped party. It then runs your test suite against each one. A mutant that makes the suite fail is caught; a mutant that passes every test survives. Every survivor is a change your tests let through, and each one is either harmless or a potential bug. The harmless ones are equivalent code no test could distinguish or a branch no execution reaches, and you can set those aside. The rest are a to-do list: each one is a specific test you are missing, a case your suite should check but does not, occasionally with a real bug sitting behind the gap. The primer above describes a real audit where a mutation campaign surfaced a high-severity bug that the project’s tests had missed. Mutation testing forces the unhappy path A DAML contract encodes rights and obligations between named parties: who holds what, who owes what to whom, and who must authorize each step. A party is not an anonymous address. It represents a real organization or person, and the contract is the rulebook for how those parties interact, including which of them can take which action, what each is allowed to see, and what stays private between them. Authorization is how that rulebook is enforced: who may take which action. It is also easy to get wrong in ordinary ways, such as a typo in a controller clause, a missing party, an extra one left over from a refactor. Every combination type-checks, so nothing rejects it before it ships. A static analyzer can flag suspicious patterns, but it has no way to know which party should hold which authority on your contract. That knowledge lives in your specification, and for most projects, the only executable form of the specification is the test suite. Happy-path tests supply every signature the contract asks for and confirm the transaction succeeds. They never try the negative case—removing a required signature and checking that the ledger rejects the transaction—so they never actually test whether that signature was required at all. If the tests don’t encode that rule, nothing downstream can recover it. Mutation testing is what tells you whether they do. A green test run tells you your tests passed today. Mutation testing asks the harder question: would your tests catch a mistake, now or after the next code change? Where the answer is no, you have found a test case worth writing. What Mewt adds for DAML Mewt parses every language it supports with a tree-sitter grammar. As of mid-2026, there is no maintained tree-sitter grammar for DAML, so we reused the upstream tree-sitter-haskell grammar. DAML is Haskell-shaped, but its contract constructs (template, choice, controller, and signatory) are not Haskell, and the grammar parses them as error-recovered subtrees. That matters less than it sounds. The common mutations still work on DAML’s ordinary expressions, so Mewt swaps arithmetic and comparison operators, flips Booleans, and removes branches just as it does in any other language, with only small adjustments where DAML’s surface syntax differs (DAML writes /= where most languages write !=). We got most of the value of a from-scratch grammar without building one. The new engineering went into DAML’s authorization primitives, where the authorization bugs from the previous section live. Mewt adds two DAML-specific mutations: Controller party swap (CPS in Mewt’s output): replace one party in a controller clause with another party that is in scope at that site. Controller party removal (CPR): drop one party from a multi-party controller list. Both target the same question: if the set of parties allowed to exercise this choice silently changed, would any test fail? They are a deliberately small starting set aimed at the bug class above, and more DAML-specific mutations are in the pipeline. Driving a campaign needs no new harness. A short mewt.toml names the files to mutate and the test command (dpm test for a Daml 3 project), and mewt run does the rest, reporting each mutant as caught or surviving. The setup is deliberately small: trying it on your own project costs minutes, and we encourage exactly that. What a surviving mutant looks like Picture a conditional payment between a buyer and a seller: the buyer sets money aside for the goods, and paying it out to the seller requires both parties to sign off. The buyer’s signature is the delivery confirmation. In DAML, that policy is one line: the controller line on the Release choice. template ConditionalPayment with buyer : Party seller : Party amount : Decimal where signatory buyer observer seller choice Release : () with paid : Decimal controller buyer, seller do assert (paid == amount) Figure 1: A payment that requires both the buyer and the seller to approve its release A typical happy-path test creates the payment and has both parties approve the release. The actAs buyer <> actAs seller line submits the command with both parties’ authority: testHappyPath : Script () testHappyPath = script do buyer <- allocateParty “Buyer” seller <- allocateParty “Seller” payment <- submit buyer do createCmd ConditionalPayment with buyer seller amount = 100.0 submit (actAs buyer <> actAs seller) do exerciseCmd payment Release with paid = 100.0 pure () Figure 2: The happy-path test. It passes, and coverage reports 100%. The test passes, and by the usual measure the suite looks complete: running dpm test with coverage reporting enabled shows full coverage. $ dpm test –show-coverage –coverage-ignore-choice Archive testHappyPath: ok, 0 active contracts, 2 transactions. – Internal templates: 1 defined, 1 (100.0%) created – Internal template choices: 1 defined, 1 (100.0%) exercised Figure 3: The coverage report for the happy-path test. Every template is created and every choice is exercised, for 100% coverage. The –coverage-ignore-choice Archive flag deserves a word. Every DAML template automatically gets an implicit Archive choice. It is not part of the business logic under test, so we exclude it for simplicity. With it included, this one-choice template would report 50% even though the test exercises everything we wrote. Run Mewt on the project and it generates seven mutants. The test suite catches three of them. Four survive. Here is one of the survivors, shown as the diff Mewt reports: choice Release : () with paid : Decimal – controller buyer, seller + controller seller do assert (paid == amount) Figure 4: The controller-removal mutant that survives the test suite Re-run the test suite against this mutant. It still passes, and coverage still reports 100%. The contract claims releasing the buyer’s money requires both parties. The mutant lets the seller release it to themselves without the buyer ever confirming delivery. The tests report green either way. Only a test that tries the forbidden path, the seller acting alone, expecting the ledger to reject it, can tell the two contracts apart. No such test exists, and the mutation score says so. (The other three survivors tell the same story from different angles: the buyer-alone twin of this mutant, and two mutants that weaken the paid == amount check to <= and >=, which survive because the test only ever pays the exact amount.) Step back, and this is the whole point of the exercise. Your tests are the executable specification of your code. Here the implementation changed, one required approval instead of two, and the specification did not react. That means the expected behavior was underspecified all along: whether both the buyer and the seller have to sign off, or just one of them, was never actually written down anywhere a machine could check. Every controller combination type-checks, and coverage reports 100% for all of them. The only place “both must sign” can exist in checkable form is a test that expects the weakened contract to fail, and writing that test is exactly what the surviving mutant tells you to do. Limitations and what comes next Mewt is not magic. Two limits are worth knowing before you run your first campaign: not every survivor is a real gap, and a campaign costs time. The roadmap that follows them is where we are taking the work next. Equivalent mutants exist: some survivors turn out to be semantically identical to the original program, so no test could ever catch them. Few public DAML codebases on GitHub come with a full test suite, so we are glad OpenZeppelin open-sourced its canton-stablecoin reference implementation. Mewt generated hundreds of mutants for it. We ran the highest-priority ones through the existing test suite, and seven of those survived. Three were equivalent mutants or sat behind a guard that no path reaches, and the other four were genuine missing test cases. None of the survivors we reviewed pointed to a bug. Such a clean result is what you want when you run Mewt on your own code, and triaging them took minutes. One of those equivalent mutants shows what that means concretely. A helper computed accrued debt: accrueDebt currentDebt lastAccrual now annualRate = if currentDebt == 0.0 || annualRate == 0.0 then currentDebt else let elapsedYears = … — elapsed time as a fraction of a year in currentDebt * (1.0 + annualRate * elapsedYears) Figure 5: The accrueDebt helper. Its first-line guard is a shortcut that returns the same value the calculation already produces. Mewt forced the if to always take the else branch. No test failed, and none ever could: when the debt is zero, the formula multiplies by zero and returns zero, and when the rate is zero, it multiplies the debt by one and returns it unchanged. The guard is a shortcut that returns the value the formula already produces, so removing it changes nothing. Mewt suppresses the equivalent mutants it can detect. The rest need a reviewer’s judgment to dismiss. Campaigns cost time in two places. The machine part: Mewt runs your test suite once per mutant, so the wall-clock cost is roughly the number of mutants times how long one test run takes, plus a rebuild if your project needs one. That is minutes on a small codebase and hours on a large one or a slow suite, so the cadence that works is nightly or weekly rather than per-commit. The human part: someone has to look at the survivors. We are working on that front from several directions at Trail of Bits, including our mutation-testing skill that helps configure campaigns for your project, and Trailmark with its genotoxic triage skill. None of these understand DAML yet, but the direction is clear: given the right harness and tools, the time-consuming parts of a campaign can be handed to AI agents. The effort is modest and the payoff is concrete: each genuine survivor is a specific test you can write, and every test you add makes your suite enforce one more guarantee your contracts are supposed to make. Also on the roadmap: choice-consumption mutations (consuming vs nonconsuming) sit cleanly on top of the controller-mutation scaffolding and target a bug class Mewt does not yet reach. Dive in Install Mewt from the repository, point a mewt.toml at your project and its test command, and mewt run. The quickstart in the README covers the rest. DAML works out of the box. Everything here ran on Daml 3.4 with dpm, but Mewt just drives whatever test command you configure, so Daml 2 projects using the daml assistant work the same way. Mutation testing complements the rest of your security stack, the type checkers, linters, and property tests you already run, rather than replacing any of it. If you’re building on Canton, we help teams with security reviews of DAML applications and with the way the code gets built: working directly with your engineers on the development process itself. Contact us.

We’re running Patch the Planet, an ongoing collaboration with OpenAI that pairs Trail of Bits engineers directly with more than 30 open-source projects. Its goal is to front-run a serious problem facing open-source maintainers: highly capable models like GPT-5.5-Cyber will soon create a firehose of bug reports, and OSS maintainers are already spread thin. Our plan is to point OpenAI’s latest models at real codebases, find the security bugs first, work with maintainers to patch them, and find ways to decrease the burden on maintainers in the long run. We’ll publish field reports like this one as the initiative progresses; follow along via the Patch the Planet tag. The expertise barrier that kept bespoke fuzzing campaigns out of reach for most attackers is gone. We watched GPT-5.5-Cyber build in a single day what would have taken weeks for a skilled security researcher: harnesses across a dozen entrypoints, sanitizer and variant builds, seeds, and multiple findings currently undergoing coordinated disclosure. This particular instance focused on zlib, a widely used data format and lossless data compression software library. We pointed GPT-5.5-Cyber at the library and drove it through Codex with the /goal command, asking it to find a specific class of bugs that are critically dangerous in compression libraries. We’ll publish the full harness and findings for inspection once the vulnerabilities are patched and a new release is cut. The lab GPT-5.5-Cyber built in a day We didn’t tell the model how to find these bugs. The obvious first move is to read the source code, but zlib has been reviewed so thoroughly that there’s little left to find that way. GPT-5.5-Cyber worked that out for itself, judged static review to be a poor use of tokens, and decided the higher value path was to build fuzz tooling to dynamically test the code. Earlier models given the same goal tend to read the code and flag whatever looks suspicious, ultimately leading to mediocre outcomes. We believe the frontier 5.5-Cyber model combined with the /goal feature is what let it execute end-to-end without hand-holding. /goal forced the objective to live across multiple turns and compactions so the model held scope, and 5.5-Cyber was smart enough to reject weak findings, expand coverage when a line of investigation died, and keep running until it had workable proof-of-concepts backed by sanitizer output. Over the next several hours, it built the campaign out one piece at a time: It used ASan and UBSan builds so memory errors became observable. It repurposed existing edge-case tests as guidance for the fuzz seed corpus. It wrote C/C++ harnesses across a dozen entrypoints, including inflate, inflateBack, uncompress2, gzFile, MiniZip, puff, blast, infback9, gzjoin, gzappend, and several contrib stream wrappers. It used compile-time variant builds (INFLATE_STRICT, BUILDFIXED, PKZIP_BUG_WORKAROUND, etc.) to reach code that the default zlib build hides. Each of these decisions is routine on its own, but stringing them together in the right order across a dozen entrypoints, without being handed the steps, is a relatively large shift in how capable frontier models are. While zlib already has fuzzing coverage from its OSS-Fuzz harness, GPT-5.5-Cyber went beyond the default harness shape, which passes random inputs to the gz* APIs. Instead of directly fuzzing the gz* APIs, its most successful harness found bugs in valid gz* states that could only be constructed by operating system backpressure. Reporting discipline is the hard part In general, models tend to struggle with deciding when a finding is severe enough to justify escalating it into reporting. Weaker models tend to escalate bugs that cause the program to crash, but are not reachable under real-world conditions. Early on, GPT-5.5-Cyber hit a null callback crash in inflateBack. The crash was real, but reaching it required a caller to set up a state that was extraordinarily unlikely in real-world conditions, so the model logged it as unreachable and moved on. This agent kept going without human intervention and found several higher-impact issues. That discipline is the whole game. The value of the zlib harness came from automation plus a strict definition of what counted as a reportable finding. Without strong validity rules baked into the goal and a model truly capable of evaluating those rules, the agent will generate mountains of noise with high confidence: invalid uses of the public API, expected parser errors, internal API misuse, etc. The moat is gone Setting up a bespoke fuzzing campaign used to mean finding someone who could write harnesses, reason about valid API state, and differentiate between a bug and a crash that can’t happen in practice. This asymmetry kept casual attackers out of the game for most targets. That moat is mostly gone now, and it shifts the threat model in two directions at the same time. For a skilled researcher, it is a force multiplier: the weeks-long tax on every new target drops to a day or less, so the same person can audit far more code. For a low-skill attacker, the floor rises: the tedious, expertise-heavy work of getting a harness off the ground can now be driven by starting a goal and supervising the loop. For anyone shipping security-critical code, the practical takeaway is clear. Bespoke fuzzing is no longer a luxury reserved for projects with mature OSS-Fuzz coverage, and it is no longer expensive for the people whom you would rather not have running it. The defensive move is to do it first, with the validity rules that turn agent output into a high-signal source you can act on. Lessons learned The fuzzing lab answered the question we came in with and left us a much bigger one. We didn’t ask GPT-5.5-Cyber to build a fuzzing campaign; it decided that was the job and did it. The thing worth watching for now is what else these new models will reach for once you hand them a goal and step back, especially the approaches we would never have thought to ask for before. That is also why the front-running work being done by Patch the Planet matters. Every new capability that helps us find bugs faster is just as available to an attacker, so the advantage goes to whoever finds the bugs and fixes them first.