Add john fixes

safe-global · Aug 21, 2024 · d4a9be6 · d4a9be6
1 parent 2299bce
commit d4a9be6
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 12 deletions.
diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec
@@ -16,17 +16,29 @@ methods{
 
     function WebAuthnHarness.checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal returns (bool) =>
     checkInjectiveSummary(challenge, authenticatorData, clientDataFields, result);
+    function _.isValidSignature(bytes32,bytes) external => DISPATCHER(optimistic=true, use_fallback=true);
 
     function _._ external => DISPATCH [
         proxy._,
         singleton._
     ] default NONDET;
 }
 
-function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes
-{
-    env e;
-    return WebAuthnHarness.GETencodeSigningMessageSummary(e, challenge, authenticatorData, clientDataFields);
+ghost mapping(bytes32 => mapping(bytes32 => mapping(bytes32 => bytes32))) componentToEncodeHash;
+ghost mapping(bytes32 => bytes32) revChallenge;
+ghost mapping(bytes32 => bytes32) revAuthenticator;
+ghost mapping(bytes32 => bytes32) revClientData;
+
+function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes {
+    bytes32 authHash = keccak256(authenticatorData);
+    bytes32 clientHash = keccak256(clientDataFields);
+    bytes32 toRetHash = componentToEncodeHash[challenge][authHash][clientHash];
+    require(revChallenge[toRetHash] == challenge);
+    require(revAuthenticator[toRetHash] == authHash);
+    require(revClientData[toRetHash] == clientHash);
+    bytes toRet;
+    require keccak256(toRet) == toRetHash;
+    return toRet;
 }
 
 ghost checkInjectiveSummary(bytes32, bytes32, bytes32, bytes32) returns bool {

diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec
@@ -12,10 +12,21 @@ methods {
     function SafeWebAuthnSignerFactory.getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v);
 }
 
-function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes
-{
-    env e;
-    return WebAuthnHarness.GETencodeSigningMessageSummary(e, challenge, authenticatorData, clientDataFields);
+ghost mapping(bytes32 => mapping(bytes32 => mapping(bytes32 => bytes32))) componentToEncodeHash;
+ghost mapping(bytes32 => bytes32) revChallenge;
+ghost mapping(bytes32 => bytes32) revAuthenticator;
+ghost mapping(bytes32 => bytes32) revClientData;
+
+function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes {
+    bytes32 authHash = keccak256(authenticatorData);
+    bytes32 clientHash = keccak256(clientDataFields);
+    bytes32 toRetHash = componentToEncodeHash[challenge][authHash][clientHash];
+    require(revChallenge[toRetHash] == challenge);
+    require(revAuthenticator[toRetHash] == authHash);
+    require(revClientData[toRetHash] == clientHash);
+    bytes toRet;
+    require keccak256(toRet) == toRetHash;
+    return toRet;
 }
 
 ghost checkInjectiveSummary(bytes32, bytes32, bytes32, bytes32) returns bool {

diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
@@ -113,7 +113,6 @@ rule verifySignatureConsistent(){
     env e1;
     env e2;
     require e1.msg.value == 0 && e2.msg.value == 0;
-    method f;
     calldataarg args;
 
     bytes32 challenge;
@@ -127,7 +126,6 @@ rule verifySignatureConsistent(){
     bool result1 = verifySignature@withrevert(e1, challenge, bytesSignature, authenticatorFlags, x, y, verifiers);
     bool firstCallRevert = lastReverted;
 
-    f(e, args);
 
     bool result2 = verifySignature@withrevert(e2, challenge, bytesSignature, authenticatorFlags, x, y, verifiers);
     bool secondCallRevert = lastReverted;
@@ -150,7 +148,6 @@ rule castSignatureConsistent(){
 
     require (e1.msg.value == e2.msg.value) && (e1.msg.value == e.msg.value) && (e.msg.value == 0);
 
-    method f;
     calldataarg args;
 
     bytes signature;
@@ -164,7 +161,6 @@ rule castSignatureConsistent(){
     firstIsValid, firstData = castSignature@withrevert(e1, signature);
     bool firstRevert = lastReverted;
 
-    f(e, args);
 
     secondIsValid, secondData = castSignature@withrevert(e2, signature);
     bool secondRevert = lastReverted;