From ea9049ed7709f7b3512bf04ef5bf54fa1f086202 Mon Sep 17 00:00:00 2001 From: John Toman Date: Tue, 18 Aug 2026 11:43:59 -0700 Subject: [PATCH] RIP king --- composer/spec/prop_inference.py | 3 +-- composer/spec/prop_refinement.py | 4 +--- composer/spec/types.py | 6 ++---- .../autoprove_report_grouping_system.j2 | 2 +- composer/templates/foundry_feedback_prompt.j2 | 5 ----- .../foundry_property_generation_prompt.j2 | 11 ++++------- ...foundry_property_generation_system_prompt.j2 | 2 +- .../nosource_property_generation_prompt.j2 | 4 ---- composer/templates/property_analysis_prompt.j2 | 4 ---- .../property_analysis_system_prompt.j2 | 11 +---------- .../templates/property_generation_prompt.j2 | 4 ---- .../property_generation_system_prompt.j2 | 16 +++++++++------- composer/templates/property_judge_prompt.j2 | 10 +++------- composer/templates/solana/property_prompt.j2 | 16 +--------------- composer/templates/soroban/property_prompt.j2 | 17 +---------------- 15 files changed, 25 insertions(+), 90 deletions(-) diff --git a/composer/spec/prop_inference.py b/composer/spec/prop_inference.py index e137a501..e919fadf 100644 --- a/composer/spec/prop_inference.py +++ b/composer/spec/prop_inference.py @@ -152,11 +152,10 @@ def _agent_round_key(i: int) -> str: properties which are difficult or impossible to prove using the Certora Prover: -1. Attack vectors or invariants that reference off-chain events (like +1. Invariants or safety properties that reference off-chain events (like key compromising, phishing, etc.) 2. Reasoning about hash function behavior or hash collisions (e.g., "invalid signatures should be rejected") -3. Event emission (not impossible, simply difficult and tedious) In addition, due to the advent of checked arithmetic, properties that assert no overflow are considered uninteresting. Further, properties diff --git a/composer/spec/prop_refinement.py b/composer/spec/prop_refinement.py index f14d2d11..192c4837 100644 --- a/composer/spec/prop_refinement.py +++ b/composer/spec/prop_refinement.py @@ -137,11 +137,9 @@ def diff_states(state_a: list[str], state_b: list[str]) -> Group: return Group(*out) def sort_to_string( - s: Literal["attack_vector", "invariant", "safety_property"] + s: Literal["invariant", "safety_property"] ) -> str: match s: - case "attack_vector": - return "Attack Vector" case "invariant": return "Invariant" case "safety_property": diff --git a/composer/spec/types.py b/composer/spec/types.py index 49d71f80..ca1b7ed1 100644 --- a/composer/spec/types.py +++ b/composer/spec/types.py @@ -84,8 +84,8 @@ class Curtailed[T]: from pydantic import BaseModel, Field -type PropertyType = Literal["attack_vector", "safety_property", "invariant"] -"""The kind of a property: an attack vector, a safety property, or a state +type PropertyType = Literal["safety_property", "invariant"] +"""The kind of a property: a safety property or a state invariant. Shared so every layer (inference, report, grouping) addresses the same vocabulary instead of redeclaring the literal.""" @@ -96,8 +96,6 @@ class UntitledPropertyFormulation(BaseModel): @property def sort_description(self) -> str: match self.sort: - case "attack_vector": - return "Attack Vector" case "invariant": return "Invariant" case "safety_property": diff --git a/composer/templates/autoprove_report_grouping_system.j2 b/composer/templates/autoprove_report_grouping_system.j2 index 68c52e45..6fce0df3 100644 --- a/composer/templates/autoprove_report_grouping_system.j2 +++ b/composer/templates/autoprove_report_grouping_system.j2 @@ -4,7 +4,7 @@ audit-style report. You are given a list of inferred properties. Each property has: - the component it belongs to, - a unique title, - - a `sort` ("invariant", "safety_property", "attack_vector"), + - a `sort` ("invariant", "safety_property"), - an English description of what it establishes. Your job is to group every property into exactly one **high-level property** suitable for an diff --git a/composer/templates/foundry_feedback_prompt.j2 b/composer/templates/foundry_feedback_prompt.j2 index a74d2873..2d21ad96 100644 --- a/composer/templates/foundry_feedback_prompt.j2 +++ b/composer/templates/foundry_feedback_prompt.j2 @@ -37,12 +37,7 @@ Understand the properties being demonstrated: {% for prop in properties %} <{{ prop.sort }}> Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }} - {% if prop.sort == "attack_vector" %} - Goal: the test(s) must demonstrate whether this attack/exploit can occur, with pass/fail semantics - wired so a regression is DETECTED as a failure. See Criterion 6. - {% else %} Goal: the test(s) must demonstrate that this property holds in the implementation. - {% endif %} {% endfor %} diff --git a/composer/templates/foundry_property_generation_prompt.j2 b/composer/templates/foundry_property_generation_prompt.j2 index 23963a46..8846d0e3 100644 --- a/composer/templates/foundry_property_generation_prompt.j2 +++ b/composer/templates/foundry_property_generation_prompt.j2 @@ -10,11 +10,7 @@ for the contract `{{ contract_name }}`: {% for prop in properties %} <{{ prop.sort }}> Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }} - {% if prop.sort == "attack_vector" %} - Goal: demonstrate that this attack/exploit *cannot* occur. - {% else %} Goal: demonstrate that this property holds. - {% endif %} {% endfor %} @@ -69,12 +65,13 @@ Call `forge_test()`. It runs `forge test` on your current buffer. pick a different precondition. - Cheatcode misuse → look up the cheatcode with the search tools and re-read the parameter shape. -* If a test is *supposed* to fail (the failure itself proves an - attack vector exists), mark it via `expect_test_failure` and +* If a test is *supposed* to fail (the failure itself proves a + safety property is violated), + mark it via `expect_test_failure` and re-run `forge_test`. The runner excludes expected-fail tests from the all-green check. -Remember: If an attack vector *IS* possible, or a safety property/invariant +Remember: If a safety property/invariant does *NOT* hold, you should produce a test that *fails* and mark it as an expected failure. Do *NOT* produce a test that passes to demonstrate "the bug exists", this is the *opposite* of what we want. diff --git a/composer/templates/foundry_property_generation_system_prompt.j2 b/composer/templates/foundry_property_generation_system_prompt.j2 index 128b8547..0e6d4a9e 100644 --- a/composer/templates/foundry_property_generation_system_prompt.j2 +++ b/composer/templates/foundry_property_generation_system_prompt.j2 @@ -48,7 +48,7 @@ wholesale, so always re-emit the full source. fail. The `forge_test` runner excludes expected-fail tests from the all-green check. Use this sparingly: only when the *failure* of the test is itself the demonstration the property requires (e.g., proving - an attack vector is reachable). For routine "this should revert" + a safety property is violated). For routine "this should revert" assertions, prefer `vm.expectRevert(...)` inline. * `feedback_tool(rebuttals=[])` -- submit the current buffer (and any skip declarations) to the feedback judge for review. A judge acceptance diff --git a/composer/templates/nosource_property_generation_prompt.j2 b/composer/templates/nosource_property_generation_prompt.j2 index f7c745a8..4e5901e0 100644 --- a/composer/templates/nosource_property_generation_prompt.j2 +++ b/composer/templates/nosource_property_generation_prompt.j2 @@ -12,11 +12,7 @@ You must write a single CVL specification covering the following properties: {% for prop in properties %} <{{ prop.sort }}> Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }} - {% if prop.sort == "attack_vector" %} - Goal: demonstrate that this attack/exploit *cannot* occur. - {% else %} Goal: demonstrate that this property holds. - {% endif %} {% endfor %} diff --git a/composer/templates/property_analysis_prompt.j2 b/composer/templates/property_analysis_prompt.j2 index be35ca44..3f7a3303 100644 --- a/composer/templates/property_analysis_prompt.j2 +++ b/composer/templates/property_analysis_prompt.j2 @@ -20,8 +20,4 @@ audit effort. You do NOT need to find evidence that these safety properties/invariants *DEFINITELY* hold, simply that they, with extreme likelihood, *SHOULD* hold for a correct implementation. - - You do not need to find evidence that the attack vectors/issues actually exist in the {% if sort != "greenfield" %}implementation{% else %}design{% endif %}, - simply that these bugs/attacks/etc. are *plausible* given the feature and its {% if sort != "greenfield" %}implementation{% else %}design{% endif %}. - diff --git a/composer/templates/property_analysis_system_prompt.j2 b/composer/templates/property_analysis_system_prompt.j2 index d8995602..1a78b037 100644 --- a/composer/templates/property_analysis_system_prompt.j2 +++ b/composer/templates/property_analysis_system_prompt.j2 @@ -40,15 +40,6 @@ Security properties fall into one of three categories: Good example: "A user without the admin role should not be able to approve other admins" Good example: "A user should not be able to change anyone's balance but their own" Bad example: "A user should not be able to hack the protocol" (overly broad) -3. Attack vectors: These are potential issues/edge cases that could be exploited in ways detrimental to the protocol/application. - IMPORTANT: you do *NOT* need to find evidence that these issues actually exists, simply that they are PLAUSIBLE given the {% if sort != "greenfield" %}current implementation{% else %}design{% endif %}. - For instance, you do not need to find evidence of a rounding error in price calculation, simply that rounding is used in a price calculation, and there is a plausible - way for that to lead to an exploit. - Good example: "A malicious actor could manipulate a price oracle to unbalance the pool, allowing free minting" - Good example: "There could be a rounding discrepancy between the swap function and the previewSwap function which could provide arbitrage opportunities" - Bad example: "There could be a rounding error, and that would be bad somehow" (does not lead to a concrete issue/exploit) - Bad example: "The protocol could be hacked" (overly broad) - Bad example: "The underlying EVM consensus layer could be compromised allowing attackers to set arbitrary storage states" (implausible) {{ backend_guidance }} @@ -105,7 +96,7 @@ consequence, defensibility in your `reasoning`. Every contract in the tree has a stable, authoritative implementation. Use the tools to ground your reasoning in the actual implementation when the design -document is ambiguous, or when an attack vector hinges on a code-level detail +document is ambiguous, or when the precise statement of a proeprty hinges on a code-level detail (storage layout, ordering of state mutations, external-call placement). Don't speculate when you can look. {% endif %} diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index 03c43137..2191ca32 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -10,11 +10,7 @@ You must write a single CVL specification covering the following properties for {% for prop in properties %} <{{ prop.sort }}> Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }} - {% if prop.sort == "attack_vector" %} - Goal: demonstrate that this attack/exploit *cannot* occur. - {% else %} Goal: demonstrate that this property holds. - {% endif %} {% endfor %} diff --git a/composer/templates/property_generation_system_prompt.j2 b/composer/templates/property_generation_system_prompt.j2 index ee4a4b51..39353be4 100644 --- a/composer/templates/property_generation_system_prompt.j2 +++ b/composer/templates/property_generation_system_prompt.j2 @@ -45,10 +45,12 @@ change no longer describe your working copy — re-run them before relying on th ## Expecting Rule Failure When you author a rule you expect to fail (that is, not receive `VERIFIED` from the prover) you can mark that -rule as "expected to fail" using the `expect_rule_failure` tool. This should be used *exceedingly* sparingly; the following -are good reasons to use this "expect failure" functionality: -1. You have been asked to formalize a rule indicating an attack vector does not exist, and you have a rule that formalizes the *absence* - of a vulnerability. However, the prover (correctly) reports a counterexample, confirming the vulnerability exists. In this case, - the rule failure is the intended result. -2. Verifying the rule is hitting some limitation in the prover (including prover errors, etc.), - and you have exhausted all reasonable alternative formulations to work around these prover limitations (errors, timeouts, imprecision). +rule as "expected to fail" using the `expect_rule_failure` tool. This should be used only when you have been asked to formalize +a rule a safety property/invariant holds, and you have a rule that formalizes the *absence* + of a vulnerability. However, the prover (correctly) reports a counterexample that shows the vulnerability exists. In this case, + the rule failure is the intended result; it loudly signals to the reader that something might be wrong in the implementation. + +If verifying a rule is hitting some limitation in the prover (including prover errors, etc.), +and you have exhausted all reasonable alternative formulations to work around these prover limitations (errors, timeouts, imprecision), +do not mark the rule as "expected to fail"; use the `record_skip` tool to indicate why you cannot deliver a result for the rule. +Do *not* ship a broken rule and mark it as expected to fail. diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index c23ac043..6bbcbb98 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -44,19 +44,15 @@ Understand the properties being formalized: {% for prop in properties %} <{{ prop.sort }}> Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }} - {% if prop.sort == "attack_vector" %} - Goal: the specification must demonstrate that this attack/exploit *cannot* occur. - {% else %} Goal: the specification must demonstrate that this property holds. - {% endif %} {% endfor %} -**IMPORTANT**: If the attack vector *DOES* exist, or the safety property/invariant *DOES NOT* -exist, then a specification *must* produce a violation (an unsatisfied proof) in the corresponding properties. +**IMPORTANT**: If the safety property/invariant *DOES NOT* hold, +then a specification *must* produce a violation (an unsatisfied proof) in the corresponding properties. A "green" verification result should *never* testify to the presence of a bug, only to a lack of them. A rule/invariant that fails to verify against the current code because it demonstrates a potential -vulnerability/attack vector is the *desired* result. +vulnerability/violation is the *desired* result. ## Step 3 diff --git a/composer/templates/solana/property_prompt.j2 b/composer/templates/solana/property_prompt.j2 index b2255daa..8a69c717 100644 --- a/composer/templates/solana/property_prompt.j2 +++ b/composer/templates/solana/property_prompt.j2 @@ -35,17 +35,7 @@ Security properties fall into three categories: Good: "No sequence of actions lets a user withdraw more than they have deposited." Bad: "A user should not be able to hack the program" (overly broad). -3. **Attack vectors** — plausible issues/edge cases exploitable to the protocol's detriment. You do - NOT need evidence they exist, only that they are PLAUSIBLE given the implementation. - Good: "If `vault` is an `UncheckedAccount` whose owner is not checked, an attacker can pass a - look-alike account they control and redirect the withdrawal." - Good: "If the `authority` account is not constrained to sign, anyone can invoke `withdraw` as - the authority (missing signer check)." - Good: "If the fee PDA's `bump` is taken from the instruction rather than re-derived, an attacker - can substitute a different PDA." - Bad: "The program could be exploited somehow" (overly broad). - -When reasoning about attack vectors and the checks each account requires, consider these vulnerability patterns: +When reasoning about safety property and the checks each account requires, consider these vulnerability patterns: {% include "rust/_vulnerability_patterns.j2" %} @@ -75,8 +65,4 @@ Output the results using the result tool. You need not prove a safety property/invariant definitely holds — only that it, with extreme likelihood, SHOULD hold for a correct implementation. - - For attack vectors you need not find evidence the issue exists — only that it is plausible - given the program and its implementation. - diff --git a/composer/templates/soroban/property_prompt.j2 b/composer/templates/soroban/property_prompt.j2 index a451c884..1852b316 100644 --- a/composer/templates/soroban/property_prompt.j2 +++ b/composer/templates/soroban/property_prompt.j2 @@ -25,7 +25,7 @@ This runs as a multi-round loop, and this is one round of it. If a ` - - Attack vectors need a credible reason, not proof. - Do not propose classic reentrancy properties. Soroban does not allow reentrancy so proposing it spends a verification cycle on something the platform guarantees. The