Skip to content

Commit

Permalink
Added summaries and additional fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@yoav-el-certora
yoav-el-certora committed May 30, 2024
1 parent 6ad4b5e commit 6c7348e
Show file tree
Hide file tree
Showing 4 changed files with 92 additions and 21 deletions.
8 changes: 8 additions & 0 deletions certora/confs/SafeWebAuthnSignerSingleton.conf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,13 @@
"assert_autofinder_success": true,
"files": [
"modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/libraries/WebAuthn.sol",
"modules/passkey/contracts/libraries/P256.sol",
"modules/passkey/contracts/libraries/ERC1271.sol",
"certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol",
"certora/harnesses/WebAuthnHarness.sol",
],
"java_args": [
" -ea -Dlevel.setup.helpers=info"
Expand All @@ -12,14 +17,17 @@
"process": "emv",
"prover_args": [
" -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on"
//" -useBitVectorTheory"
],
"packages":[
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"solc": "solc8.23",
"rule_sanity": "basic",
"solc_via_ir": false,
"optimistic_loop": true,
"loop_iter": "6",
"optimistic_hashing": true,
"prover_version": "master",
"server": "production",
Expand Down
4 changes: 4 additions & 0 deletions certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,4 +19,8 @@ contract SafeWebAuthnSignerSingletonHarness is SafeWebAuthnSignerSingleton {
(uint256 x, uint256 y, P256.Verifiers verifiers) = getConfiguration();
success = WebAuthn.verifySignature(message, signature, WebAuthn.USER_VERIFICATION, x, y, verifiers);
}

function getConfigurationHarnessed(bytes32 message, bytes calldata signature) public pure returns (uint256 new_x, uint256 new_y, P256.Verifiers new_verifiers) {
(uint256 new_x, uint256 new_y, P256.Verifiers new_verifiers) = getConfiguration();
}
}
17 changes: 17 additions & 0 deletions certora/harnesses/WebAuthnHarness.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,5 +89,22 @@ contract WebAuthnHarness {
function getSha256(bytes memory input) public view returns (bytes32 digest) {
return WebAuthn._sha256(input);
}

mapping (bytes32 => mapping (bytes32 => mapping (bytes32 => bytes))) symbolicMessageSummary;

function GETencodeSigningMessageSummary(bytes32 challenge, bytes calldata authenticatorData, string calldata clientDataFields) public returns (bytes memory){
bytes32 hashed_authenticatorData = keccak256(authenticatorData);
bytes32 hashed_clientDataFields = keccak256(abi.encodePacked(clientDataFields));

bytes memory bytes_mapping = symbolicMessageSummary[challenge][hashed_authenticatorData][hashed_clientDataFields];

require (checkInjective(challenge, hashed_authenticatorData, hashed_clientDataFields, keccak256(bytes_mapping)));

return bytes_mapping;
}

function checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal view returns (bool){
return true;
}

}
84 changes: 63 additions & 21 deletions certora/specs/SafeWebAuthnSignerSingleton.spec
View file
Original file line number Diff line number Diff line change
@@ -1,51 +1,93 @@
using SafeWebAuthnSignerProxy as proxy;
using WebAuthnHarness as WebAuthnHarness;

methods {
function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns (bool) =>
verifySignatureAllowMalleabilityGhost(a, b, c, d, e, f);

function WebAuthn.encodeSigningMessage(bytes32 challenge, bytes calldata authenticatorData, string calldata clientDataFields) internal returns (bytes memory) =>
GETencodeSigningMessageCVL(challenge, authenticatorData, clientDataFields);

function WebAuthnHarness.checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal returns (bool) =>
checkInjectiveSummary(challenge, authenticatorData, clientDataFields, result);
}

function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes
{
env e;
return WebAuthnHarness.GETencodeSigningMessageSummary(e, challenge, authenticatorData, clientDataFields);
}

ghost checkInjectiveSummary(bytes32, bytes32, bytes32, bytes32) returns bool {
axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 z1. forall bytes32 x2. forall bytes32 y2. forall bytes32 z2. forall bytes32 result.
checkInjectiveSummary(x1, y1, z1, result) && checkInjectiveSummary(x2, y2, z2, result) => x1 == x2;
}

ghost verifySignatureAllowMalleabilityGhost(P256.Verifiers, bytes32, uint256, uint256, uint256, uint256) returns bool {
axiom forall P256.Verifiers a. forall bytes32 message1. forall bytes32 message2. forall uint256 c. forall uint256 d. forall uint256 e. forall uint256 f.
verifySignatureAllowMalleabilityGhost(a, message1, c, d, e, f) &&
verifySignatureAllowMalleabilityGhost(a, message2, c, d, e, f) => message1 == message2;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Implementation of _verifySignature Function (Integrity) │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule verifySignatureIntegrity(env e){
rule verifySignatureUniqueness(env e){
bytes32 first_message;
bytes32 second_message;
bytes signature;

require (first_message != second_message);

bool first_message_verified = verifySignatureHarnessed(e, first_message, signature);
bool second_message_verified = verifySignatureHarnessed(e, second_message, signature);

assert !(first_message_verified && second_message_verified);
}

rule verifySignatureIntegrity(env e){
bytes32 first_message;
bytes32 second_message;
bytes signature;

bool first_message_verified = verifySignatureHarnessed(e, first_message, signature);
require (first_message_verified);

bool second_message_verified = verifySignatureHarnessed(e, second_message, signature);

assert (first_message_verified == true && second_message_verified == true) => first_message == second_message;
assert first_message == second_message => first_message_verified == second_message_verified;
assert second_message_verified <=> first_message == second_message;
}


/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ getConfiguration Function (Integrity) │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

// TODO Not Completed Yet
// rule verifyGetConfigurationIntegrity(env e){
// bytes32 data;
// bytes first_signature;

// uint256 x;
// uint256 y;
// P256.Verifiers verifiers;
// uint256 new_x; uint256 new_y; P256.Verifiers new_verifiers;
// bytes32 message;

// // bytes data = assignValues(e, x, y, verifiers);
// (new_x, new_y, new_verifiers) = temp(e, x, y, verifiers);

// // (x, y, verifiers) = getConfiguration(e);
// // (new_x, new_y, new_verifiers) = getConfigurationHarnessed(e, data);
// x = proxy.getX();
// y = proxy.getY();
// verifiers = proxy.getVerifiers();
// (new_x, new_y, new_verifiers) = proxy.getConfiguration(e);

// assert x == new_x;
// assert y == new_y;
// assert verifiers == new_verifiers;
// satisfy true;
// }


/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Both is valid Signature behave the same way │
Expand All @@ -56,42 +98,44 @@ rule verifyIsValidSignatureAreEqual(env e){
bytes data;
bytes first_signature;

bool hashed_data_verified = verifySignatureHarnessed(e, keccak256(data), first_signature);
bytes4 magicValue_hashed = isValidSignature(e, data, first_signature);

bytes second_signature;
bytes32 message;
bool message_verified = verifySignatureHarnessed(e, message, second_signature);
bytes4 magicValue_message = isValidSignature(e, message, first_signature);

assert (hashed_data_verified == true && message_verified == true) => message == keccak256(data);
assert message == keccak256(data) => hashed_data_verified == message_verified;
assert (magicValue_hashed == to_bytes4(0x20c13b0b) && magicValue_message == to_bytes4(0x1626ba7e)) => message == keccak256(data);
assert message == keccak256(data) => (magicValue_hashed == to_bytes4(0x20c13b0b) && magicValue_message == to_bytes4(0x1626ba7e)) ||
(magicValue_hashed != to_bytes4(0x20c13b0b) && magicValue_message != to_bytes4(0x1626ba7e));
}


/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Once signer passed isValidSignature it will never fail on it after any call │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule verifyIsValidSignatureWillContinueToSucceed(env e){
method f;
calldataarg args;
bytes32 message;
bytes signature;

bool first_verified = verifySignatureHarnessed(e, message, signature);
require first_verified == true;

f(e, args);

bool second_verified = verifySignatureHarnessed(e, message, signature);
assert second_verified;
}


/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Once isValidSignature failed, it will never pass before createSigner called │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule IsValidSignatureMustSucceedAfterCreation(env e){
rule IsValidSignatureWillSucceedOnlyAfterCreation(env e){
method f;
calldataarg args;

Expand All @@ -103,8 +147,6 @@ rule IsValidSignatureMustSucceedAfterCreation(env e){

f(e, args);


bool second_verified = verifySignatureHarnessed(e, message, signature);
assert second_verified => f.selector == sig:SafeWebAuthnSignerFactory.createSigner(uint256, uint256, P256.Verifiers).selector;
}

0 comments on commit 6c7348e

Please sign in to comment.