diff --git a/src/kontrol/kdist/keccak.md b/src/kontrol/kdist/keccak.md index 9c9b3befc..993b30f85 100644 --- a/src/kontrol/kdist/keccak.md +++ b/src/kontrol/kdist/keccak.md @@ -1,7 +1,7 @@ Keccak Assumptions ============== -The provided K Lemmas define assumptions and properties related to the keccak hash function used in the verification of smart contracts within the symbolic execution context. +The provided K Lemmas define assumptions and properties related to the `keccak` hash function used in the verification of smart contracts within the symbolic execution context. ```k module KECCAK-LEMMAS @@ -9,56 +9,54 @@ module KECCAK-LEMMAS imports INT-SYMBOLIC ``` -1. The result of the `keccak` function is always a non-negative integer, and it is always less than 2^256. +1. `keccak` always returns an integer in the range `[0, 2 ^ 256)`. ```k rule 0 <=Int keccak( _ ) => true [simplification, smt-lemma] rule keccak( _ ) true [simplification, smt-lemma] ``` -2. The result of the `keccak` function applied on a symbolic input does not equal any concrete value. +2. No value outside of the `[0, 2 ^ 256)` range can be the result of a `keccak`. ```k - // keccak does not equal a concrete value - rule [keccak-eq-conc-false]: keccak(_A) ==Int _B => false [symbolic(_A), concrete(_B), simplification(30), comm] - rule [keccak-neq-conc-true]: keccak(_A) =/=Int _B => true [symbolic(_A), concrete(_B), simplification(30), comm] + rule [keccak-out-of-range]: X ==Int keccak (_) => false requires X =Int pow256 [concrete(X), simplification] + rule [keccak-out-of-range-ml]: { X #Equals keccak (_) } => #Bottom requires X =Int pow256 [concrete(X), simplification] ``` -In addition, equality involving keccak of a symbolic variable is reduced to a comparison that always results in `false` for concrete values. +3. This lemma directly simplifies an expression that involves a `keccak` and is often introduced by the Solidity compiler. ```k - rule [keccak-eq-conc-false-ml-lr]: { keccak(A) #Equals B } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification] - rule [keccak-eq-conc-false-ml-rl]: { B #Equals keccak(A) } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification] + rule chop (0 -Int keccak(BA)) => pow256 -Int keccak(BA) + [simplification] ``` -3. Injectivity of Keccak. If `keccak(A)` equals `keccak(B)`, then `A` must equal `B`. - -In reality, cryptographic hash functions like `keccak` are not injective. They are designed to be collision-resistant, meaning it is computationally infeasible to find two different inputs that produce the same hash output, but not impossible. -The assumption of injectivity simplifies reasoning about the keccak function in formal verification, but it is not fundamentally true. It is used to aid in the verification process. +4. The result of a `keccak` is assumed not to fall too close to the edges of its official range. This accounts for the shifts added to the result of a `keccak` when accessing storage slots, and is a hypothesis made by the ecosystem. ```k - // keccak is injective - rule [keccak-inj]: keccak(A) ==Int keccak(B) => A ==K B [simplification] - rule [keccak-inj-ml]: { keccak(A) #Equals keccak(B) } => { true #Equals A ==K B } [simplification] + rule BOUND:Int true requires BOUND <=Int 32 [simplification, concrete(BOUND)] + rule keccak(B:Bytes) true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)] ``` -4. Negating keccak. Instead of allowing a negative value, the rule adjusts it within the valid range, ensuring the value remains non-negative. +5. `keccak` is injective: that is, if `keccak(A)` equals `keccak(B)`, then `A` equals `B`. + +In reality, cryptographic hash functions like `keccak` are not injective. They are designed to be collision-resistant, meaning it is computationally infeasible to find two different inputs that produce the same hash output, but not impossible. +This assumption reflects that hypothesis in the context of formal verification, making it more tractable. ```k - // chop of negative keccak - rule chop (0 -Int keccak(BA)) => pow256 -Int keccak(BA) - [simplification] + rule [keccak-inj]: keccak(A) ==Int keccak(B) => A ==K B [simplification] + rule [keccak-inj-ml]: { keccak(A) #Equals keccak(B) } => { true #Equals A ==K B } [simplification] ``` -5. Ensure that any value resulting from a `keccak` is within the valid range of 0 and 2^256 - 1. +6. `keccak` of a symbolic parameter does not equal a concrete value. This lemma is based on our experience in Foundry-supported testing and is specific to how `keccak` functions are used in practical symbolic execution. The underlying hypothesis that justifies it is that the storage slots of a given mapping are presumed to be disjoint from slots of other mappings and also the non-mapping slots of a contract. ```k - // keccak cannot equal a number outside of its range - rule { X #Equals keccak (_) } => #Bottom - requires X =Int pow256 - [concrete(X), simplification] + rule [keccak-eq-conc-false]: keccak(_A) ==Int _B => false [symbolic(_A), concrete(_B), simplification(30), comm] + rule [keccak-neq-conc-true]: keccak(_A) =/=Int _B => true [symbolic(_A), concrete(_B), simplification(30), comm] - rule keccak(B:Bytes) true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)] + rule [keccak-eq-conc-false-ml-lr]: { keccak(A) #Equals B } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification] + rule [keccak-eq-conc-false-ml-rl]: { B #Equals keccak(A) } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification] +``` +```k endmodule ``` \ No newline at end of file