diff --git a/.github/workflows/certora_passkey.yml b/.github/workflows/certora_passkey.yml new file mode 100644 index 00000000..626a6612 --- /dev/null +++ b/.github/workflows/certora_passkey.yml @@ -0,0 +1,66 @@ +name: certora + +on: + push: + branches: + - main + paths: + - modules/passkey/** + pull_request: + branches: + - main + paths: + - modules/passkey/** + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + strategy: + matrix: + rule: + [ + 'GetConfigurationConf', + 'GetSigner', + 'ProxySimulator', + 'SafeWebAuthnSignerFactory', + 'SafeWebAuthnSignerProxy', + 'SafeWebAuthnSignerSingleton', + 'SignerCreationCantOverride', + 'SingletonIsValidSignatureRevertingConditions', + 'ValidSignatureForSignerIntegrity', + 'VerifyEQtoIsValidSignatureForSigner', + 'WebAuthn', + ] + steps: + - uses: actions/checkout@v4 + + - name: Install pnpm + uses: pnpm/action-setup@v4 + with: + version: 9 + + - name: Install python + uses: actions/setup-python@v4 + with: { python-version: 3.11 } + + - name: Install certora cli + run: pip install -r modules/passkey/certora/requirements.txt + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.26/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.26 + + - name: Install dependencies + run: pnpm install + + - name: Verify rule ${{ matrix.rule }} + working-directory: ./modules/passkey + run: | + echo "Certora key length" ${#CERTORAKEY} + certoraRun certora/conf/${{ matrix.rule }}.conf --wait_for_results=all + env: + CERTORAKEY: ${{ secrets.CERTORA_KEY }} diff --git a/modules/4337/package.json b/modules/4337/package.json index 128c7522..faafe8b7 100644 --- a/modules/4337/package.json +++ b/modules/4337/package.json @@ -24,6 +24,7 @@ "benchmark": "pnpm run test test/gas/*.ts", "deploy-all": "hardhat deploy-contracts --network", "deploy": "hardhat deploy --network", + "deploy-custom": "rm -rf deployments/custom && npm run deploy custom", "lint": "pnpm run lint:sol && npm run lint:ts", "lint:sol": "solhint 'contracts/**/*.sol'", "lint:ts": "eslint ./src && eslint ./test", diff --git a/modules/allowances/.env.sample b/modules/allowances/.env.sample index c3c43746..d069fcb9 100644 --- a/modules/allowances/.env.sample +++ b/modules/allowances/.env.sample @@ -1,3 +1,4 @@ MNEMONIC= INFURA_KEY= ETHERSCAN_API_KEY= +CUSTOM_NODE_URL= diff --git a/modules/allowances/hardhat.config.ts b/modules/allowances/hardhat.config.ts index 66fab4dd..834d076f 100644 --- a/modules/allowances/hardhat.config.ts +++ b/modules/allowances/hardhat.config.ts @@ -9,7 +9,7 @@ import { getSingletonFactoryInfo } from '@safe-global/safe-singleton-factory' dotenv.config() -const { INFURA_KEY, MNEMONIC, ETHERSCAN_API_KEY } = process.env +const { INFURA_KEY, MNEMONIC, ETHERSCAN_API_KEY, CUSTOM_NODE_URL } = process.env const sharedNetworkConfig: HttpNetworkUserConfig = { accounts: { @@ -19,6 +19,15 @@ const sharedNetworkConfig: HttpNetworkUserConfig = { }, } +const customNetwork = CUSTOM_NODE_URL + ? { + custom: { + ...sharedNetworkConfig, + url: CUSTOM_NODE_URL, + }, + } + : {} + const config: HardhatUserConfig = { paths: { artifacts: 'build/artifacts', @@ -78,6 +87,7 @@ const config: HardhatUserConfig = { ...sharedNetworkConfig, url: `https://api.avax.network/ext/bc/C/rpc`, }, + ...customNetwork, }, deterministicDeployment, namedAccounts: { diff --git a/modules/allowances/package.json b/modules/allowances/package.json index 1eb9b591..3bdbe393 100644 --- a/modules/allowances/package.json +++ b/modules/allowances/package.json @@ -14,6 +14,7 @@ "test": "hardhat test", "coverage": "hardhat coverage", "deploy": "hardhat deploy-verify --network", + "deploy-custom": "rm -rf deployments/custom && npm run deploy custom", "prepare": "pnpm run clean && npm run build", "lint": "pnpm run lint:sol && npm run lint:ts", "lint:sol": "solhint 'contracts/**/*.sol'", diff --git a/modules/passkey/certora/conf/GetConfigurationConf.conf b/modules/passkey/certora/conf/GetConfigurationConf.conf new file mode 100644 index 00000000..376e99bc --- /dev/null +++ b/modules/passkey/certora/conf/GetConfigurationConf.conf @@ -0,0 +1,25 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/munged/SafeWebAuthnSignerSingleton.sol", + "certora/harnesses/GetConfigurationProxyHarness.sol", + "contracts/SafeWebAuthnSignerFactory.sol" + ], + "link": [ + "GetConfigurationProxyHarness:_SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "prover_args": [ + " -split false" + ], + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "GetConfigurationProxyHarness:certora/specs/GetConfigurationSpec.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/GetSigner.conf b/modules/passkey/certora/conf/GetSigner.conf new file mode 100644 index 00000000..47b76324 --- /dev/null +++ b/modules/passkey/certora/conf/GetSigner.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/GetSignerHarness.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol" + ], + "hashing_length_bound": "4694", + "link": [ + "GetSignerHarness:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "144", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "GetSignerHarness:certora/specs/GetSigner.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/ProxySimulator.conf b/modules/passkey/certora/conf/ProxySimulator.conf new file mode 100644 index 00000000..2b690656 --- /dev/null +++ b/modules/passkey/certora/conf/ProxySimulator.conf @@ -0,0 +1,27 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/ProxySimulator.sol", + "contracts/SafeWebAuthnSignerProxy.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol" + ], + "hashing_length_bound": "2048", + "link": [ + "ProxySimulator:_proxy=SafeWebAuthnSignerProxy", + "SafeWebAuthnSignerProxy:_VERIFIERS=P256", + "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "ProxySimulator:certora/specs/ProxySimulator.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/SafeWebAuthnSignerFactory.conf b/modules/passkey/certora/conf/SafeWebAuthnSignerFactory.conf new file mode 100644 index 00000000..edd74628 --- /dev/null +++ b/modules/passkey/certora/conf/SafeWebAuthnSignerFactory.conf @@ -0,0 +1,30 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/FactoryHarnessForSignerConsistency.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol" + ], + "link": [ + "FactoryHarnessForSignerConsistency:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "rule": [ + "createAndGetSignerEquivalence", + "getSignerRevertingConditions", + "hasNoCodeIntegrity", + "isValidSignatureForSignerConsistency", + "singletonNeverChanges" + ], + "process": "emv", + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "FactoryHarnessForSignerConsistency:certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/SafeWebAuthnSignerProxy.conf b/modules/passkey/certora/conf/SafeWebAuthnSignerProxy.conf new file mode 100644 index 00000000..878ade7a --- /dev/null +++ b/modules/passkey/certora/conf/SafeWebAuthnSignerProxy.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "contracts/SafeWebAuthnSignerProxy.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol" + ], + "link": [ + "SafeWebAuthnSignerProxy:_VERIFIERS=P256", + "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "SafeWebAuthnSignerProxy:certora/specs/SafeWebAuthnSignerProxy.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/SafeWebAuthnSignerSingleton.conf b/modules/passkey/certora/conf/SafeWebAuthnSignerSingleton.conf new file mode 100644 index 00000000..5b287008 --- /dev/null +++ b/modules/passkey/certora/conf/SafeWebAuthnSignerSingleton.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "contracts/SafeWebAuthnSignerFactory.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol" + ], + "link": [ + "SafeWebAuthnSignerFactory:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/SignerCreationCantOverride.conf b/modules/passkey/certora/conf/SignerCreationCantOverride.conf new file mode 100644 index 00000000..1fd022f8 --- /dev/null +++ b/modules/passkey/certora/conf/SignerCreationCantOverride.conf @@ -0,0 +1,31 @@ +{ + "assert_autofinder_success": true, + "exclude_rule": [ + "createAndVerifyEQtoIsValidSignatureForSigner" + ], + "files": [ + "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol", + "contracts/libraries/P256.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol" + ], + "hashing_length_bound": "912", + "link": [ + "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule": [ + "SignerCreationCantOverride" + ], + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/SingletonIsValidSignatureRevertingConditions.conf b/modules/passkey/certora/conf/SingletonIsValidSignatureRevertingConditions.conf new file mode 100644 index 00000000..669c773e --- /dev/null +++ b/modules/passkey/certora/conf/SingletonIsValidSignatureRevertingConditions.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "contracts/SafeWebAuthnSignerFactory.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule": [ + "isValidSignatureRevertingConditions" + ], + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/ValidSignatureForSignerIntegrity.conf b/modules/passkey/certora/conf/ValidSignatureForSignerIntegrity.conf new file mode 100644 index 00000000..2c7b962f --- /dev/null +++ b/modules/passkey/certora/conf/ValidSignatureForSignerIntegrity.conf @@ -0,0 +1,26 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol" + ], + "link": [ + "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule": [ + "isValidSignatureForSignerIntegrity" + ], + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/VerifyEQtoIsValidSignatureForSigner.conf b/modules/passkey/certora/conf/VerifyEQtoIsValidSignatureForSigner.conf new file mode 100644 index 00000000..12d76bcc --- /dev/null +++ b/modules/passkey/certora/conf/VerifyEQtoIsValidSignatureForSigner.conf @@ -0,0 +1,33 @@ +{ + "assert_autofinder_success": true, + "dynamic_bound": "1", + "files": [ + "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "certora/munged/SafeWebAuthnSignerProxy.sol", + "certora/munged/WebAuthn.sol", + "certora/harnesses/WebAuthnHarnessWithMunge.sol" + ], + "hashing_length_bound": "906", + "link": [ + "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "prover_args": [ + "-depth 12" + ], + "rule": [ + "createAndVerifyEQtoIsValidSignatureForSigner" + ], + "rule_sanity": "basic", + "smt_timeout": "600", + "solc": "solc8.26", + "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/conf/WebAuthn.conf b/modules/passkey/certora/conf/WebAuthn.conf new file mode 100644 index 00000000..4172b58d --- /dev/null +++ b/modules/passkey/certora/conf/WebAuthn.conf @@ -0,0 +1,17 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/WebAuthnHarnessWithMunge.sol" + ], + "loop_iter": "6", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "process": "emv", + "rule_sanity": "basic", + "solc": "solc8.26", + "verify": "WebAuthnHarnessWithMunge:certora/specs/WebAuthn.spec" +} \ No newline at end of file diff --git a/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol b/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol new file mode 100644 index 00000000..fd584e3a --- /dev/null +++ b/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {SafeWebAuthnSignerFactory} from "../munged/FactoryForSignerConsistency.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; + +contract FactoryHarnessForSignerConsistency is SafeWebAuthnSignerFactory { + //Harness + function hasNoCode(address account) external view returns (bool result) { + // solhint-disable-next-line no-inline-assembly + return SafeWebAuthnSignerFactory._hasNoCode(account); + } + + function createAndVerify( + bytes32 message, + bytes calldata signature, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) external returns (bytes4 magicValue) { + address signer = this.createSigner(x, y, verifiers); + + bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature); + + // Use low-level call to invoke isValidSignature on the signer address + (bool success, bytes memory result) = signer.staticcall(data); + require(success); + magicValue = abi.decode(result, (bytes4)); + } + + /** + munge to pass the SignerCreationCantOverride rule. + */ + function _hasNoCode(address account) internal view override returns (bool result) { + return account.code.length == 0; + } +} diff --git a/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol b/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol new file mode 100644 index 00000000..05c17bc1 --- /dev/null +++ b/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable no-complex-fallback */ +pragma solidity >=0.8.0; + +import {P256} from "../../contracts/libraries/WebAuthn.sol"; + +/** + * @title Safe WebAuthn Signer Proxy + * @dev A specialized proxy to a {SafeWebAuthnSignerSingleton} signature validator implementation + * for Safe accounts. Using a proxy pattern for the signature validator greatly reduces deployment + * gas costs. + * @custom:security-contact bounty@safe.global + */ +contract GetConfigurationProxyHarness { + /** + * @notice The {SafeWebAuthnSignerSingleton} implementation to proxy to. + */ + address internal immutable _SINGLETON; + + /** + * @notice The x coordinate of the P-256 public key of the WebAuthn credential. + */ + uint256 internal immutable _X; + + /** + * @notice The y coordinate of the P-256 public key of the WebAuthn credential. + */ + uint256 internal immutable _Y; + + /** + * @notice The P-256 verifiers used for ECDSA signature verification. + */ + P256.Verifiers internal immutable _VERIFIERS; + + function getX() external view returns (uint256) { + return _X; + } + function getY() external view returns (uint256) { + return _Y; + } + function getVerifiers() external view returns (P256.Verifiers) { + return _VERIFIERS; + } + + /** + * @notice Creates a new WebAuthn Safe Signer Proxy. + * @param singleton The {SafeWebAuthnSignerSingleton} implementation to proxy to. + * @param x The x coordinate of the P-256 public key of the WebAuthn credential. + * @param y The y coordinate of the P-256 public key of the WebAuthn credential. + * @param verifiers The P-256 verifiers used for ECDSA signature verification. + */ + constructor(address singleton, uint256 x, uint256 y, P256.Verifiers verifiers) { + _SINGLETON = singleton; + _X = x; + _Y = y; + _VERIFIERS = verifiers; + } + + /** + * @dev Fallback function forwards all transactions and returns all received return data. + */ + //fallback() external payable { + function getConfiguration() external returns (uint256 x, uint256 y, P256.Verifiers verifiers) { + address singleton = _SINGLETON; + uint256 x = _X; + uint256 y = _Y; + P256.Verifiers verifiers = _VERIFIERS; + + // solhint-disable-next-line no-inline-assembly + assembly { + // Forward the call to the singleton implementation. We append the configuration to the + // calldata instead of having the singleton implementation read it from storage. This is + // both more gas efficient and required for ERC-4337 compatibility. Note that we append + // the configuration fields in reverse order since the fields are packed, and this makes + // it so we don't need to mask any bits from the `verifiers` value. This computes `data` + // to be `abi.encodePacked(msg.data, x, y, verifiers)`. + let data := mload(0x40) + mstore(add(data, add(calldatasize(), 0x36)), verifiers) + mstore(add(data, add(calldatasize(), 0x20)), y) + mstore(add(data, calldatasize()), x) + calldatacopy(data, 0x00, calldatasize()) + + let success := staticcall(gas(), singleton, data, add(calldatasize(), 0x56), 0, 0) + returndatacopy(0, 0, returndatasize()) + if iszero(success) { + revert(0, returndatasize()) + } + return(0, returndatasize()) + } + } +} diff --git a/modules/passkey/certora/harnesses/GetSignerHarness.sol b/modules/passkey/certora/harnesses/GetSignerHarness.sol new file mode 100644 index 00000000..8766656d --- /dev/null +++ b/modules/passkey/certora/harnesses/GetSignerHarness.sol @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {SafeWebAuthnSignerFactory} from "../munged/SafeWebAuthnSignerFactory.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; + +contract GetSignerHarness is SafeWebAuthnSignerFactory { + function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); + } + function castToAddress(uint256 value) public pure returns (address addr) { + addr = address(uint160(value)); + } + + /** + * munged getSigner + */ + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view override returns (address signer) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", // munged for word alignment workaround (32 bytes) + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + signer = address(uint160(uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))))); + } +} diff --git a/modules/passkey/certora/harnesses/ProxySimulator.sol b/modules/passkey/certora/harnesses/ProxySimulator.sol new file mode 100644 index 00000000..4d5bec7b --- /dev/null +++ b/modules/passkey/certora/harnesses/ProxySimulator.sol @@ -0,0 +1,23 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable no-complex-fallback */ +pragma solidity >=0.8.0; + +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; + +contract ProxySimulator { + address internal _proxy; + + constructor(address proxy) { + _proxy = proxy; + } + + function authenticate(bytes32 message, bytes calldata signature) external returns (bytes4) { + bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature); + + (bool success, bytes memory result) = _proxy.call(data); + + require(success); + + return abi.decode(result, (bytes4)); + } +} diff --git a/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol new file mode 100644 index 00000000..c7a12e1c --- /dev/null +++ b/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {SafeWebAuthnSignerFactory} from "../munged/SafeWebAuthnSignerFactory.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; + +contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory { + //Harness + function hasNoCode(address account) external view returns (bool result) { + // solhint-disable-next-line no-inline-assembly + return SafeWebAuthnSignerFactory._hasNoCode(account); + } + + function createAndVerify( + bytes32 message, + bytes calldata signature, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) external returns (bytes4 magicValue) { + address signer = this.createSigner(x, y, verifiers); + + bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature); + + // Use low-level call to invoke isValidSignature on the signer address + (bool success, bytes memory result) = signer.staticcall(data); + require(success); + magicValue = abi.decode(result, (bytes4)); + } + + /** + munge to pass the SignerCreationCantOverride rule. + */ + function _hasNoCode(address account) internal view override returns (bool result) { + return account.code.length == 0; + } +} diff --git a/modules/passkey/certora/harnesses/Utilities.sol b/modules/passkey/certora/harnesses/Utilities.sol new file mode 100644 index 00000000..1f2b7b30 --- /dev/null +++ b/modules/passkey/certora/harnesses/Utilities.sol @@ -0,0 +1,20 @@ +import {P256} from "../../contracts/libraries/WebAuthn.sol"; + +interface IConfigHolder { + function getConfiguration() external pure returns (uint256 x, uint256 y, P256.Verifiers verifiers); +} + +contract Utilities { + function havocAll() external { + (bool success, ) = address(0xdeadbeef).call(abi.encodeWithSelector(0x12345678)); + require(success); + } + + function justRevert() external { + revert(); + } + + function getConfiguration(address proxy) external view returns (uint256 x, uint256 y, P256.Verifiers verifiers) { + return IConfigHolder(proxy).getConfiguration(); + } +} diff --git a/modules/passkey/certora/harnesses/WebAuthnHarness.sol b/modules/passkey/certora/harnesses/WebAuthnHarness.sol new file mode 100644 index 00000000..2f178713 --- /dev/null +++ b/modules/passkey/certora/harnesses/WebAuthnHarness.sol @@ -0,0 +1,142 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.0; + +import {P256, WebAuthn} from "../../contracts/libraries/WebAuthn.sol"; + +contract WebAuthnHarness { + mapping(bytes32 => mapping(bytes32 => string)) symbolicClientDataJson; + + function summaryEncodeDataJson(bytes32 challenge, string calldata clientDataFields) public returns (string memory) { + bytes32 hashClientDataFields = keccak256(abi.encodePacked(clientDataFields)); + string memory stringResult = symbolicClientDataJson[challenge][hashClientDataFields]; + bytes32 hashResult = keccak256(abi.encodePacked(stringResult)); + + require(checkInjective(challenge, hashClientDataFields, hashResult)); + + return stringResult; + } + + function checkInjective(bytes32 challenge, bytes32 clientDataFields, bytes32 result) internal view returns (bool) { + return true; + } + + function compareSignatures(WebAuthn.Signature memory sig1, WebAuthn.Signature memory sig2) public pure returns (bool) { + if (sig1.r != sig2.r || sig1.s != sig2.s) { + return false; + } + + if (keccak256(abi.encodePacked(sig1.clientDataFields)) != keccak256(abi.encodePacked(sig2.clientDataFields))) { + return false; + } + + if (keccak256(sig1.authenticatorData) != keccak256(sig2.authenticatorData)) { + return false; + } + + return true; + } + + function encodeSignature(WebAuthn.Signature calldata sig) external pure returns (bytes memory signature) { + signature = abi.encode(sig.authenticatorData, sig.clientDataFields, sig.r, sig.s); + } + + function castSignature(bytes calldata signature) external pure returns (bool isValid, WebAuthn.Signature calldata data) { + return WebAuthn.castSignature(signature); + } + + function castSignatureSuccess(bytes32 unused, bytes calldata signature) external pure returns (bool) { + (bool isValid, ) = WebAuthn.castSignature(signature); + return isValid; + } + + function castSignature_notreturns(bytes calldata signature) external pure { + WebAuthn.castSignature(signature); + } + + function compareStrings(string memory str1, string memory str2) public view returns (bool) { + bytes memory str1Bytes = bytes(str1); + bytes memory str2Bytes = bytes(str2); + return getSha256(str1Bytes) == getSha256(str2Bytes); + } + + function encodeClientDataJson(bytes32 challenge, string calldata clientDataFields) public pure returns (string memory clientDataJson) { + return WebAuthn.encodeClientDataJson(challenge, clientDataFields); + } + + function encodeSigningMessage( + bytes32 challenge, + bytes calldata authenticatorData, + string calldata clientDataFields + ) public view returns (bytes memory message) { + return WebAuthn.encodeSigningMessage(challenge, authenticatorData, clientDataFields); + } + + function checkAuthenticatorFlags( + bytes calldata authenticatorData, + WebAuthn.AuthenticatorFlags authenticatorFlags + ) public pure returns (bool success) { + return WebAuthn.checkAuthenticatorFlags(authenticatorData, authenticatorFlags); + } + + function prepareSignature( + bytes calldata authenticatorData, + string calldata clientDataFields, + uint256 r, + uint256 s + ) public pure returns (bytes memory signature, WebAuthn.Signature memory structSignature) { + signature = abi.encode(authenticatorData, clientDataFields, r, s); + structSignature = WebAuthn.Signature(authenticatorData, clientDataFields, r, s); + } + + function verifySignature( + bytes32 challenge, + bytes calldata signature, + WebAuthn.AuthenticatorFlags authenticatorFlags, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) public view returns (bool success) { + return WebAuthn.verifySignature(challenge, signature, authenticatorFlags, x, y, verifiers); + } + + function verifySignature( + bytes32 challenge, + WebAuthn.Signature calldata signature, + WebAuthn.AuthenticatorFlags authenticatorFlags, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) public view returns (bool success) { + return WebAuthn.verifySignature(challenge, signature, authenticatorFlags, x, y, verifiers); + } + + 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; + } +} diff --git a/modules/passkey/certora/harnesses/WebAuthnHarnessWithMunge.sol b/modules/passkey/certora/harnesses/WebAuthnHarnessWithMunge.sol new file mode 100644 index 00000000..d50eb437 --- /dev/null +++ b/modules/passkey/certora/harnesses/WebAuthnHarnessWithMunge.sol @@ -0,0 +1,142 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.0; + +import {P256, WebAuthn} from "../munged/WebAuthn.sol"; + +contract WebAuthnHarnessWithMunge { + mapping(bytes32 => mapping(bytes32 => string)) symbolicClientDataJson; + + function summaryEncodeDataJson(bytes32 challenge, string calldata clientDataFields) public returns (string memory) { + bytes32 hashClientDataFields = keccak256(abi.encodePacked(clientDataFields)); + string memory stringResult = symbolicClientDataJson[challenge][hashClientDataFields]; + bytes32 hashResult = keccak256(abi.encodePacked(stringResult)); + + require(checkInjective(challenge, hashClientDataFields, hashResult)); + + return stringResult; + } + + function checkInjective(bytes32 challenge, bytes32 clientDataFields, bytes32 result) internal view returns (bool) { + return true; + } + + function compareSignatures(WebAuthn.Signature memory sig1, WebAuthn.Signature memory sig2) public pure returns (bool) { + if (sig1.r != sig2.r || sig1.s != sig2.s) { + return false; + } + + if (keccak256(abi.encodePacked(sig1.clientDataFields)) != keccak256(abi.encodePacked(sig2.clientDataFields))) { + return false; + } + + if (keccak256(sig1.authenticatorData) != keccak256(sig2.authenticatorData)) { + return false; + } + + return true; + } + + function encodeSignature(WebAuthn.Signature calldata sig) external pure returns (bytes memory signature) { + signature = abi.encode(sig.authenticatorData, sig.clientDataFields, sig.r, sig.s); + } + + function castSignature(bytes calldata signature) external pure returns (bool isValid, WebAuthn.Signature calldata data) { + return WebAuthn.castSignature(signature); + } + + function castSignatureSuccess(bytes32 unused, bytes calldata signature) external pure returns (bool) { + (bool isValid, ) = WebAuthn.castSignature(signature); + return isValid; + } + + function castSignature_notreturns(bytes calldata signature) external pure { + WebAuthn.castSignature(signature); + } + + function compareStrings(string memory str1, string memory str2) public view returns (bool) { + bytes memory str1Bytes = bytes(str1); + bytes memory str2Bytes = bytes(str2); + return getSha256(str1Bytes) == getSha256(str2Bytes); + } + + function encodeClientDataJson(bytes32 challenge, string calldata clientDataFields) public pure returns (string memory clientDataJson) { + return WebAuthn.encodeClientDataJson(challenge, clientDataFields); + } + + function encodeSigningMessage( + bytes32 challenge, + bytes calldata authenticatorData, + string calldata clientDataFields + ) public view returns (bytes memory message) { + return WebAuthn.encodeSigningMessage(challenge, authenticatorData, clientDataFields); + } + + function checkAuthenticatorFlags( + bytes calldata authenticatorData, + WebAuthn.AuthenticatorFlags authenticatorFlags + ) public pure returns (bool success) { + return WebAuthn.checkAuthenticatorFlags(authenticatorData, authenticatorFlags); + } + + function prepareSignature( + bytes calldata authenticatorData, + string calldata clientDataFields, + uint256 r, + uint256 s + ) public pure returns (bytes memory signature, WebAuthn.Signature memory structSignature) { + signature = abi.encode(authenticatorData, clientDataFields, r, s); + structSignature = WebAuthn.Signature(authenticatorData, clientDataFields, r, s); + } + + function verifySignature( + bytes32 challenge, + bytes calldata signature, + WebAuthn.AuthenticatorFlags authenticatorFlags, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) public view returns (bool success) { + return WebAuthn.verifySignature(challenge, signature, authenticatorFlags, x, y, verifiers); + } + + function verifySignature( + bytes32 challenge, + WebAuthn.Signature calldata signature, + WebAuthn.AuthenticatorFlags authenticatorFlags, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) public view returns (bool success) { + return WebAuthn.verifySignature(challenge, signature, authenticatorFlags, x, y, verifiers); + } + + 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; + } +} diff --git a/modules/passkey/certora/munged/FactoryForSignerConsistency.sol b/modules/passkey/certora/munged/FactoryForSignerConsistency.sol new file mode 100644 index 00000000..71582890 --- /dev/null +++ b/modules/passkey/certora/munged/FactoryForSignerConsistency.sol @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {ISafeSignerFactory} from "../../contracts/interfaces/ISafeSignerFactory.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; +import {SafeWebAuthnSignerSingleton} from "../../contracts/SafeWebAuthnSignerSingleton.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; + +/** + * @title Safe WebAuthn Signer Factory + * @dev A factory contract for creating WebAuthn signers. Additionally, the factory supports + * signature verification without deploying a signer proxies. + * @custom:security-contact bounty@safe.global + */ +contract SafeWebAuthnSignerFactory is ISafeSignerFactory { + /** + * @notice The {SafeWebAuthnSignerSingleton} implementation to that is used for signature + * verification by this contract and any proxies it deploys. + */ + SafeWebAuthnSignerSingleton public immutable SINGLETON; + + /** + * @notice Creates a new WebAuthn Safe signer factory contract. + * @dev The {SafeWebAuthnSignerSingleton} singleton implementation is created with as part of + * this constructor. This ensures that the singleton contract is known, and lets us make certain + * assumptions about how it works. + */ + constructor() { + SINGLETON = new SafeWebAuthnSignerSingleton(); + } + + /** + * @inheritdoc ISafeSignerFactory + */ + // funtion is not really virtual, Munged! + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view virtual override returns (address signer) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + signer = address(uint160(uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))))); + } + + /** + * @inheritdoc ISafeSignerFactory + */ + function createSigner(uint256 x, uint256 y, P256.Verifiers verifiers) external returns (address signer) { + signer = getSigner(x, y, verifiers); + + if (_hasNoCode(signer)) { + SafeWebAuthnSignerProxy created = new SafeWebAuthnSignerProxy{salt: bytes32(0)}(address(SINGLETON), x, y, verifiers); + assert(address(created) == signer); + emit Created(signer, x, y, verifiers); + } + } + + /** + * @inheritdoc ISafeSignerFactory + */ + function isValidSignatureForSigner( + bytes32 message, + bytes calldata signature, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) external view override returns (bytes4 magicValue) { + address singleton = address(SINGLETON); + bytes memory data = abi.encodePacked( + abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature), + x, + y, + verifiers + ); + + // solhint-disable-next-line no-inline-assembly + assembly { + // staticcall to the singleton contract with return size given as 32 bytes. The + // singleton contract is known and immutable so it is safe to specify return size. + if staticcall(gas(), singleton, add(data, 0x20), mload(data), 0, 32) { + magicValue := mload(0) + } + } + } + + /** + * @dev Checks if the provided account has no code. + * @param account The address of the account to check. + * @return result True if the account has no code, false otherwise. + */ + // funtion is not really virtual, munged! + function _hasNoCode(address account) internal view virtual returns (bool result) { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + result := iszero(extcodesize(account)) + } + } +} diff --git a/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol b/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol new file mode 100644 index 00000000..9f6ef9b7 --- /dev/null +++ b/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol @@ -0,0 +1,106 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {ISafeSignerFactory} from "../../contracts/interfaces/ISafeSignerFactory.sol"; +import {SafeWebAuthnSignerProxy} from "./SafeWebAuthnSignerProxy.sol"; +import {SafeWebAuthnSignerSingleton} from "./SafeWebAuthnSignerSingleton.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; + +/** + * @title Safe WebAuthn Signer Factory + * @dev A factory contract for creating WebAuthn signers. Additionally, the factory supports + * signature verification without deploying a signer proxies. + * @custom:security-contact bounty@safe.global + */ +contract SafeWebAuthnSignerFactory is ISafeSignerFactory { + /** + * @notice The {SafeWebAuthnSignerSingleton} implementation to that is used for signature + * verification by this contract and any proxies it deploys. + */ + SafeWebAuthnSignerSingleton public immutable SINGLETON; + + /** + * @notice Creates a new WebAuthn Safe signer factory contract. + * @dev The {SafeWebAuthnSignerSingleton} singleton implementation is created with as part of + * this constructor. This ensures that the singleton contract is known, and lets us make certain + * assumptions about how it works. + */ + constructor() { + SINGLETON = new SafeWebAuthnSignerSingleton(); + } + + /** + * @inheritdoc ISafeSignerFactory + */ + // funtion is not really virtual, Munged! + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view virtual override returns (address signer) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + signer = address(uint160(uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))))); + } + + /** + * @inheritdoc ISafeSignerFactory + */ + function createSigner(uint256 x, uint256 y, P256.Verifiers verifiers) external returns (address signer) { + signer = getSigner(x, y, verifiers); + + if (_hasNoCode(signer)) { + SafeWebAuthnSignerProxy created = new SafeWebAuthnSignerProxy{salt: bytes32(0)}(address(SINGLETON), x, y, verifiers); + assert(address(created) == signer); + emit Created(signer, x, y, verifiers); + } + } + + /** + * @inheritdoc ISafeSignerFactory + */ + function isValidSignatureForSigner( + bytes32 message, + bytes calldata signature, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) external view override returns (bytes4 magicValue) { + address singleton = address(SINGLETON); + bytes memory data = abi.encodePacked( + abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature), + x, + y, + verifiers + ); + + // solhint-disable-next-line no-inline-assembly + assembly { + // staticcall to the singleton contract with return size given as 32 bytes. The + // singleton contract is known and immutable so it is safe to specify return size. + // MUNGED!! + // if staticcall(gas(), singleton, add(data, 0x20), mload(data), 0, 32) { + // magicValue := mload(0) + // } + if staticcall(gas(), singleton, add(data, 0x20), mload(data), mload(0x40), 32) { + magicValue := mload(mload(0x40)) + } + } + } + + /** + * @dev Checks if the provided account has no code. + * @param account The address of the account to check. + * @return result True if the account has no code, false otherwise. + */ + // funtion is not really virtual, munged! + function _hasNoCode(address account) internal view virtual returns (bool result) { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + result := iszero(extcodesize(account)) + } + } +} diff --git a/modules/passkey/certora/munged/SafeWebAuthnSignerProxy.sol b/modules/passkey/certora/munged/SafeWebAuthnSignerProxy.sol new file mode 100644 index 00000000..7dbae901 --- /dev/null +++ b/modules/passkey/certora/munged/SafeWebAuthnSignerProxy.sol @@ -0,0 +1,81 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable no-complex-fallback */ +pragma solidity >=0.8.0; + +import {P256} from "./WebAuthn.sol"; + +/** + * @title Safe WebAuthn Signer Proxy + * @dev A specialized proxy to a {SafeWebAuthnSignerSingleton} signature validator implementation + * for Safe accounts. Using a proxy pattern for the signature validator greatly reduces deployment + * gas costs. + * @custom:security-contact bounty@safe.global + */ +contract SafeWebAuthnSignerProxy { + /** + * @notice The {SafeWebAuthnSignerSingleton} implementation to proxy to. + */ + address internal immutable _SINGLETON; + + /** + * @notice The x coordinate of the P-256 public key of the WebAuthn credential. + */ + uint256 internal immutable _X; + + /** + * @notice The y coordinate of the P-256 public key of the WebAuthn credential. + */ + uint256 internal immutable _Y; + + /** + * @notice The P-256 verifiers used for ECDSA signature verification. + */ + P256.Verifiers internal immutable _VERIFIERS; + + /** + * @notice Creates a new WebAuthn Safe Signer Proxy. + * @param singleton The {SafeWebAuthnSignerSingleton} implementation to proxy to. + * @param x The x coordinate of the P-256 public key of the WebAuthn credential. + * @param y The y coordinate of the P-256 public key of the WebAuthn credential. + * @param verifiers The P-256 verifiers used for ECDSA signature verification. + */ + constructor(address singleton, uint256 x, uint256 y, P256.Verifiers verifiers) { + _SINGLETON = singleton; + _X = x; + _Y = y; + _VERIFIERS = verifiers; + } + + /** + * @dev Fallback function forwards all transactions and returns all received return data. + */ + fallback() external payable { + address singleton = _SINGLETON; + uint256 x = _X; + uint256 y = _Y; + P256.Verifiers verifiers = _VERIFIERS; + + // solhint-disable-next-line no-inline-assembly + assembly { + // Forward the call to the singleton implementation. We append the configuration to the + // calldata instead of having the singleton implementation read it from storage. This is + // both more gas efficient and required for ERC-4337 compatibility. Note that we append + // the configuration fields in reverse order since the fields are packed, and this makes + // it so we don't need to mask any bits from the `verifiers` value. This computes `data` + // to be `abi.encodePacked(msg.data, x, y, verifiers)`. + let data := mload(0x40) + // MUNGED mstore(add(data, add(calldatasize(), 0x36)), verifiers) + mstore(add(data, add(calldatasize(), 0x40)), shl(80, verifiers)) + mstore(add(data, add(calldatasize(), 0x20)), y) + mstore(add(data, calldatasize()), x) + calldatacopy(data, 0x00, calldatasize()) + + let success := delegatecall(gas(), singleton, data, add(calldatasize(), 0x56), 0, 0) + returndatacopy(0, 0, returndatasize()) + if iszero(success) { + revert(0, returndatasize()) + } + return(0, returndatasize()) + } + } +} diff --git a/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol b/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol new file mode 100644 index 00000000..b37f59a6 --- /dev/null +++ b/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {SignatureValidator} from "../../contracts/base/SignatureValidator.sol"; +import {P256, WebAuthn} from "../../contracts/libraries/WebAuthn.sol"; + +/** + * @title Safe WebAuthn Signer Singleton + * @dev A singleton contract that implements WebAuthn signature verification. This singleton + * contract must be used with the specialized proxy {SafeWebAuthnSignerProxy}, as it encodes the + * credential configuration (public key coordinates and P-256 verifier to use) in calldata, which is + * required by this implementation. + * @custom:security-contact bounty@safe.global + */ +contract SafeWebAuthnSignerSingleton is SignatureValidator { + /** + * @inheritdoc SignatureValidator + */ + function _verifySignature(bytes32 message, bytes calldata signature) internal view virtual override returns (bool success) { + (uint256 x, uint256 y, P256.Verifiers verifiers) = getConfiguration(); + success = WebAuthn.verifySignature(message, signature, WebAuthn.USER_VERIFICATION, x, y, verifiers); + } + + /** + * @notice Returns the x coordinate, y coordinate, and P-256 verifiers used for ECDSA signature + * validation. The values are expected to appended to calldata by the caller. See the + * {SafeWebAuthnSignerProxy} contract implementation. + * @return x The x coordinate of the P-256 public key. + * @return y The y coordinate of the P-256 public key. + * @return verifiers The P-256 verifiers. + */ + function getConfiguration() public pure returns (uint256 x, uint256 y, P256.Verifiers verifiers) { + // solhint-disable-next-line no-inline-assembly + // solhint-disable-next-line no-inline-assembly + // MUNGED! - Added new line + uint256 mask = type(uint176).max; + assembly ("memory-safe") { + x := calldataload(sub(calldatasize(), 86)) + y := calldataload(sub(calldatasize(), 54)) + // MUNGED! Original line is - verifiers := shr(80, calldataload(sub(calldatasize(), 22))) + verifiers := and(mask, calldataload(sub(calldatasize(), 32))) + } + } +} diff --git a/modules/passkey/certora/munged/WebAuthn.sol b/modules/passkey/certora/munged/WebAuthn.sol new file mode 100644 index 00000000..14daefb6 --- /dev/null +++ b/modules/passkey/certora/munged/WebAuthn.sol @@ -0,0 +1,360 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.0; + +import {P256} from "../../contracts/libraries/P256.sol"; + +/** + * @title WebAuthn Signature Verification + * @dev Library for verifying WebAuthn signatures for public key credentials using the ES256 + * algorithm with the P-256 curve. + * @custom:security-contact bounty@safe.global + */ +library WebAuthn { + using P256 for P256.Verifiers; + + /** + * @notice The WebAuthn signature data format. + * @dev WebAuthn signatures are expected to be the ABI-encoded bytes of the following structure. + * @param authenticatorData The authenticator data from the WebAuthn credential assertion. + * @param clientDataFields The additional fields from the client data JSON. This is the comma + * separated fields as they appear in the client data JSON from the WebAuthn credential + * assertion after the leading {type} and {challenge} fields. + * @param r The ECDSA signature's R component. + * @param s The ECDSA signature's S component. + */ + struct Signature { + bytes authenticatorData; + string clientDataFields; + uint256 r; + uint256 s; + } + + /** + * @notice A WebAuthn authenticator bit-flags + * @dev Represents flags that are included in a WebAuthn assertion's authenticator data and can + * be used to check on-chain how the user was authorized by the device when signing. + */ + type AuthenticatorFlags is bytes1; + + /** + * @notice Authenticator data flag indicating user presence (UP). + * @dev A test of user presence is a simple form of authorization gesture and technical process + * where a user interacts with an authenticator by (typically) simply touching it (other + * modalities may also exist), yielding a Boolean result. Note that this does not constitute + * user verification because a user presence test, by definition, is not capable of biometric + * recognition, nor does it involve the presentation of a shared secret such as a password or + * PIN. + * + * See . + */ + AuthenticatorFlags internal constant USER_PRESENCE = AuthenticatorFlags.wrap(0x01); + + /** + * @notice Authenticator data flag indicating user verification (UV). + * @dev The technical process by which an authenticator locally authorizes the invocation of the + * authenticatorMakeCredential and authenticatorGetAssertion operations. User verification MAY + * be instigated through various authorization gesture modalities; for example, through a touch + * plus pin code, password entry, or biometric recognition (e.g., presenting a fingerprint). The + * intent is to distinguish individual users. + * + * Note that user verification does not give the Relying Party a concrete identification of the + * user, but when 2 or more ceremonies with user verification have been done with that + * credential it expresses that it was the same user that performed all of them. The same user + * might not always be the same natural person, however, if multiple natural persons share + * access to the same authenticator. + * + * See . + */ + AuthenticatorFlags internal constant USER_VERIFICATION = AuthenticatorFlags.wrap(0x04); + + /** + * @notice Casts calldata bytes to a WebAuthn signature data structure. + * @param signature The calldata bytes of the WebAuthn signature. + * @return isValid Whether or not the encoded signature bytes is valid. + * @return data A pointer to the signature data in calldata. + * @dev This method casts the dynamic bytes array to a signature calldata pointer with some + * additional verification. Specifically, we ensure that the signature bytes encoding is no + * larger than standard ABI encoding form, to prevent attacks where valid signatures are padded + * with 0s in order to increase signature verifications the costs for ERC-4337 user operations. + */ + function castSignature(bytes calldata signature) internal pure returns (bool isValid, Signature calldata data) { + uint256 authenticatorDataLength; + uint256 clientDataFieldsLength; + // MUNGED Initiating isValid for future usage + isValid = true; + + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + data := signature.offset + + // Read the lengths of the dynamic byte arrays in assembly. This is done because + // Solidity generates calldata bounds checks which aren't required for the security of + // the signature verification, as it can only lead to _shorter_ signatures which are + // are less gas expensive anyway. + + // MUNGED To simplify prover execution + let t1 := calldataload(data) + isValid := and(isValid, lt(t1, signature.length)) + authenticatorDataLength := calldataload(add(data, t1)) + let t2 := calldataload(add(data, 0x20)) + isValid := and(isValid, lt(t2, signature.length)) + clientDataFieldsLength := calldataload(add(data, calldataload(add(data, 0x20)))) + } + + // Use of unchecked math as any overflows in dynamic length computations would cause + // out-of-gas reverts when computing the WebAuthn signing message. + unchecked { + // Allow for signature encodings where the dynamic bytes are aligned to 32-byte + // boundaries. This allows for high interoperability (as this is how Solidity and most + // tools `abi.encode`s the `Signature` struct) while setting a strict upper bound to how + // many additional padding bytes can be added to the signature, increasing gas costs. + // Note that we compute the aligned lengths with the formula: `l + 0x1f & ~0x1f`, which + // rounds `l` up to the next 32-byte boundary. + uint256 alignmentMask = ~uint256(0x1f); + uint256 authenticatorDataAlignedLength = (authenticatorDataLength + 0x1f) & alignmentMask; + uint256 clientDataFieldsAlignedLength = (clientDataFieldsLength + 0x1f) & alignmentMask; + + // The fixed parts of the signature length are 6 32-byte words for a total of 192 bytes: + // - offset of the `authenticatorData` bytes + // - offset of the `clientDataFields` string + // - signature `r` value + // - signature `s` value + // - length of the `authenticatorData` bytes + // - length of the `clientDataFields` string + // + // This implies that the signature length must be less than or equal to: + // 192 + authenticatorDataAlignedLength + clientDataFieldsAlignedLength + // which is equivalent to strictly less than: + // 193 + authenticatorDataAlignedLength + clientDataFieldsAlignedLength + + // MUNGED To simplify prover execution + isValid = isValid && signature.length < 193 + authenticatorDataAlignedLength + clientDataFieldsAlignedLength; + } + } + + /** + * @notice Encodes the client data JSON string from the specified challenge, and additional + * client data fields. + * @dev The client data JSON follows a very specific encoding process outlined in the Web + * Authentication standard. See . + * @param challenge The WebAuthn challenge used for the credential assertion. + * @param clientDataFields Client data fields. + * @return clientDataJson The encoded client data JSON. + */ + function encodeClientDataJson( + bytes32 challenge, + string calldata clientDataFields + ) internal pure returns (string memory clientDataJson) { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + // The length of the encoded JSON string. This is always 82 plus the length of the + // additional client data fields: + // - 36 bytes for: `{"type":"webauthn.get","challenge":"` + // - 43 bytes for base-64 encoding of 32 bytes of data + // - 2 bytes for: `",` + // - `clientDataFields.length` bytes for the additional client data JSON fields + // - 1 byte for: `}` + let encodedLength := add(82, clientDataFields.length) + + // Set `clientDataJson` return parameter to point to the start of the free memory. + // This is where the encoded JSON will be stored. + clientDataJson := mload(0x40) + + // Write the constant bytes of the encoded client data JSON string as per the JSON + // serialization specification. Note that we write the data backwards, this is to avoid + // overwriting previously written data with zeros. Offsets are computed to account for + // both the leading 32-byte length and leading zeros from the constants. + mstore(add(clientDataJson, encodedLength), 0x7d) // } + mstore(add(clientDataJson, 81), 0x222c) // ", + mstore(add(clientDataJson, 36), 0x2c226368616c6c656e6765223a22) // ,"challenge":" + mstore(add(clientDataJson, 22), 0x7b2274797065223a22776562617574686e2e67657422) // {"type":"webauthn.get" + mstore(clientDataJson, encodedLength) + + // Copy the client data fields from calldata to their reserved space in memory. + calldatacopy(add(clientDataJson, 113), clientDataFields.offset, clientDataFields.length) + + // Store the base-64 URL character lookup table into the scratch and free memory pointer + // space in memory [^1]. The table is split into two 32-byte parts and stored in memory + // from address 0x1f to 0x5e. Note that the offset is chosen in such a way that the + // least significant byte of `mload(x)` is the base-64 ASCII character for the 6-bit + // value `x`. We will write the free memory pointer at address `0x40` before leaving the + // assembly block accounting for the allocation of `clientDataJson`. + // + // - [^1](https://docs.soliditylang.org/en/stable/internals/layout_in_memory.html). + mstore(0x1f, "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdef") + mstore(0x3f, "ghijklmnopqrstuvwxyz0123456789-_") + + // Initialize a pointer for writing the base-64 encoded challenge. + let ptr := add(clientDataJson, 68) + + // Base-64 encode the challenge to its reserved space in memory. + // + // To minimize stack and jump operations, we partially unroll the loop. With full 6 + // iterations of the loop, we need to encode seven 6-bit groups and one 4-bit group. In + // total, it encodes 6 iterations * 7 groups * 6 bits = 252 bits. The remaining 4-bit + // group is encoded after the loop. `i` is initialized to 250, which is the number of + // bits by which we need to shift the data to get the first 6-bit group, and then we + // subtract 6 to get the next 6-bit group. + // + // We want to exit when all full 6 bits groups are encoded. After 6 iterations, `i` will + // be -2 and the **signed** comparison with 0 will break the loop. + for { + let i := 250 + } sgt(i, 0) { + // Advance the pointer by the number of bytes written (7 bytes in this case). + ptr := add(ptr, 7) + // Move `i` by 42 = 6 bits * 7 (groups processed in each iteration). + i := sub(i, 42) + } { + // Encode 6-bit groups into characters by looking them up in the character table. + // 0x3f is a mask to get the last 6 bits so that we can index directly to the + // base-64 lookup table. + mstore8(ptr, mload(and(shr(i, challenge), 0x3f))) + mstore8(add(ptr, 1), mload(and(shr(sub(i, 6), challenge), 0x3f))) + mstore8(add(ptr, 2), mload(and(shr(sub(i, 12), challenge), 0x3f))) + mstore8(add(ptr, 3), mload(and(shr(sub(i, 18), challenge), 0x3f))) + mstore8(add(ptr, 4), mload(and(shr(sub(i, 24), challenge), 0x3f))) + mstore8(add(ptr, 5), mload(and(shr(sub(i, 30), challenge), 0x3f))) + mstore8(add(ptr, 6), mload(and(shr(sub(i, 36), challenge), 0x3f))) + } + + // Encode the final 4-bit group, where 0x0f is a mask to get the last 4 bits. + mstore8(ptr, mload(shl(2, and(challenge, 0x0f)))) + + // Update the free memory pointer to point to the end of the encoded string. + // Store the length of the encoded string at the beginning of `result`. + mstore(0x40, and(add(clientDataJson, add(encodedLength, 0x3f)), not(0x1f))) + } + } + + /** + * @notice Encodes the message that is signed in a WebAuthn assertion. + * @dev The signing message is defined to be the concatenation of the authenticator data bytes + * with the 32-byte SHA-256 digest of the client data JSON. The hashing algorithm used on the + * signing message itself depends on the public key algorithm that was selected on WebAuthn + * credential creation. + * @param challenge The WebAuthn challenge used for the credential assertion. + * @param authenticatorData Authenticator data. + * @param clientDataFields Client data fields. + * @return message Signing message bytes. + */ + function encodeSigningMessage( + bytes32 challenge, + bytes calldata authenticatorData, + string calldata clientDataFields + ) internal view returns (bytes memory message) { + string memory clientDataJson = encodeClientDataJson(challenge, clientDataFields); + bytes32 clientDataHash = _sha256(bytes(clientDataJson)); + + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + // The length of the signing message, this is the length of the authenticator data plus + // the 32-byte hash of the client data JSON. + let messageLength := add(authenticatorData.length, 32) + + // Allocate the encoded signing `message` at the start of the free memory. Note that we + // pad the allocation to 32-byte boundary as Solidity typically does. + message := mload(0x40) + mstore(0x40, and(add(message, add(messageLength, 0x3f)), not(0x1f))) + mstore(message, messageLength) + + // The actual message data is written to 32 bytes past the start of the allocation, as + // the first 32 bytes contains the length of the byte array. + let messagePtr := add(message, 32) + + // Copy the authenticator from calldata to the start of the `message` buffer that was + // allocated. Note that we start copying 32 bytes after the start of the allocation to + // account for the length. + calldatacopy(messagePtr, authenticatorData.offset, authenticatorData.length) + + // Finally, write the client data JSON hash to the end of the `message`. + mstore(add(messagePtr, authenticatorData.length), clientDataHash) + } + } + + /** + * @notice Checks that the required authenticator data flags are set. + * @param authenticatorData The authenticator data. + * @param authenticatorFlags The authenticator flags to check for. + * @return success Whether the authenticator data flags are set. + */ + function checkAuthenticatorFlags( + bytes calldata authenticatorData, + AuthenticatorFlags authenticatorFlags + ) internal pure returns (bool success) { + success = authenticatorData[32] & AuthenticatorFlags.unwrap(authenticatorFlags) == AuthenticatorFlags.unwrap(authenticatorFlags); + } + + /** + * @notice Verifies a WebAuthn signature. + * @param challenge The WebAuthn challenge used in the credential assertion. + * @param signature The encoded WebAuthn signature bytes. + * @param authenticatorFlags The authenticator data flags that must be set. + * @param x The x-coordinate of the credential's public key. + * @param y The y-coordinate of the credential's public key. + * @param verifiers The P-256 verifier configuration to use. + * @return success Whether the signature is valid. + */ + function verifySignature( + bytes32 challenge, + bytes calldata signature, + AuthenticatorFlags authenticatorFlags, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) internal view returns (bool success) { + Signature calldata signatureStruct; + (success, signatureStruct) = castSignature(signature); + if (success) { + success = verifySignature(challenge, signatureStruct, authenticatorFlags, x, y, verifiers); + } + } + + /** + * @notice Verifies a WebAuthn signature. + * @param challenge The WebAuthn challenge used in the credential assertion. + * @param signature The WebAuthn signature data. + * @param authenticatorFlags The authenticator data flags that must be set. + * @param x The x-coordinate of the credential's public key. + * @param y The y-coordinate of the credential's public key. + * @param verifiers The P-256 verifier configuration to use. + * @return success Whether the signature is valid. + */ + function verifySignature( + bytes32 challenge, + Signature calldata signature, + AuthenticatorFlags authenticatorFlags, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) internal view returns (bool success) { + // The order of operations here is slightly counter-intuitive (in particular, you do not + // need to encode the signing message if the expected authenticator flags are missing). + // However, ordering things this way helps the Solidity compiler generate meaningfully more + // optimal code for the "happy path" when Yul optimizations are turned on. + bytes memory message = encodeSigningMessage(challenge, signature.authenticatorData, signature.clientDataFields); + if (checkAuthenticatorFlags(signature.authenticatorData, authenticatorFlags)) { + success = verifiers.verifySignatureAllowMalleability(_sha256(message), signature.r, signature.s, x, y); + } + } + + /** + * @notice Compute the SHA-256 hash of the input bytes. + * @dev The Solidity compiler sometimes generates a memory copy loop for the call to the SHA-256 + * precompile, even if the input is already in memory. Force this not to happen by manually + * implementing the call to the SHA-256 precompile. + * @param input The input bytes to hash. + * @return digest The SHA-256 digest of the input bytes. + */ + function _sha256(bytes memory input) public view returns (bytes32 digest) { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + // The SHA-256 precompile is at address 0x0002. Note that we don't check the whether or + // not the precompile reverted or if the return data size is 32 bytes, which is a + // reasonable assumption for the precompile, as it is specified to always return the + // SHA-256 of its input bytes. + pop(staticcall(gas(), 0x0002, add(input, 0x20), mload(input), 0, 32)) + digest := mload(0) + } + } +} diff --git a/modules/passkey/certora/properties.txt b/modules/passkey/certora/properties.txt new file mode 100644 index 00000000..56b63c66 --- /dev/null +++ b/modules/passkey/certora/properties.txt @@ -0,0 +1,31 @@ +Factory - Immutability of Singleton Contract. [Critical] +Factory - getSigner is unique for every x,y and verifier combination (need to make sure it is required) [High] +Factory - createSigner and getSigner always returns the same address. [Medium] +Factory - Deterministic Address Calculation for Signers. [High] +Factory - Correctness of Signer Creation. (Cant called twice, override) [Cannot understand the risk] +Factory - Signature Validation (isValidSignatureForSigner Integrity) [Critical] +Factory - Code Presence Check (_hasNoCode Integrity) [Deprecated - internal code] +Proxy - Immutability of Configuration Parameters (x, y, Singleton, verifier) [Critical] +Proxy - Delegate Call Integrity (calls the _verifySignature implementation in the Singleton) [Low] +Proxy - Fallback data corruption (uses data appending that needed to be verified) [Low] +Proxy - verify return data from Delegate call. [Low] +Proxy - No buffer overflow when appending Parameters. //(Maybe for Dravee) [Low] +Singleton - Implementation of _verifySignature Function (Integrity) [High/Medium] +Singleton - getConfiguration Function (Integrity). [High/Medium] +Singleton - Both is valid Signature behave the same way. [Low] +Singleton - Once signer passed isValidSignature it will never fail on it after any call. [Low] +Singleton - Once isValidSignature failed, it will never pass before createSigner called. [High] +WebAuthn - castSignature Integrity [Low/Medium] +WebAuthn - encodeClientDataJson Integrity [Medium] +WebAuthn - encodeSigningMessage Integrity [Medium] +WebAuthn - verifySignature Integrity [Medium] +WebAuthn - Both verifySignature behave the same way. [Low] +WebAuthn - given input in encodeSigningMessage(), one should produce only one valid output. [Medium - Maybe duplication] + i.e., one cannot reuse a signature valid for one challenge to be valid for another challenge + +// Optional +Checks for Revert condition on critical Functions (isValidSignature, + verifySignature, Proxy Fallback, createSigner, getSigner) [Low] + + // Open Question for Dravee: + What is the user protection against hacks? \ No newline at end of file diff --git a/modules/passkey/certora/requirements.txt b/modules/passkey/certora/requirements.txt new file mode 100644 index 00000000..31db1d46 --- /dev/null +++ b/modules/passkey/certora/requirements.txt @@ -0,0 +1 @@ +certora-cli==7.17.2 diff --git a/modules/passkey/certora/specs/GetConfigurationSpec.spec b/modules/passkey/certora/specs/GetConfigurationSpec.spec new file mode 100644 index 00000000..bd68bbf7 --- /dev/null +++ b/modules/passkey/certora/specs/GetConfigurationSpec.spec @@ -0,0 +1,36 @@ +using GetConfigurationProxyHarness as proxy; + +methods { + function GetConfigurationProxyHarness.getX() external returns (uint256) envfree; + function GetConfigurationProxyHarness.getY() external returns (uint256) envfree; + function GetConfigurationProxyHarness.getVerifiers() external returns (P256.Verifiers) envfree; + + function _._ external => DISPATCH [ + SafeWebAuthnSignerSingleton.getConfiguration() + ] default HAVOC_ALL; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ getConfiguration Function (Integrity) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule verifyGetConfigurationIntegrity(env e){ + + uint256 x; + uint256 y; + P256.Verifiers verifiers; + uint256 new_x; uint256 new_y; P256.Verifiers new_verifiers; + bytes32 message; + + 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; +} diff --git a/modules/passkey/certora/specs/GetSigner.spec b/modules/passkey/certora/specs/GetSigner.spec new file mode 100644 index 00000000..4304f5d9 --- /dev/null +++ b/modules/passkey/certora/specs/GetSigner.spec @@ -0,0 +1,89 @@ +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ + getSigner is unique for every x,y and verifier combination, proved with assumptions: + 1.) value before cast to address <= max_uint160. + 2.) munging required to complete signer data to be constructed from full 32bytes size arrays + function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", <--------------- HERE! + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); + } +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +// helper rule to justify the use of the harnessed implementation (proved). +rule mungedEquivalence() +{ + env e1; + env e2; + + require e1.msg.value == 0 && e2.msg.value == 0; + uint256 x; + uint256 y; + P256.Verifiers verifier; + + storage s = lastStorage; + + uint256 harnessedSignerValue = getSignerHarnessed@withrevert(e1, x, y, verifier); + bool harnessedSignerRevert1 = lastReverted; + + address harnessedSigner = castToAddress@withrevert(e1, harnessedSignerValue); + bool harnessedSignerRevert2 = harnessedSignerRevert1 && lastReverted; + + address signer = getSigner@withrevert(e2, x, y, verifier) at s; + bool signerRevert = lastReverted; + + assert (harnessedSignerRevert2 == signerRevert); + assert (!harnessedSignerRevert2 && !signerRevert) => (harnessedSigner == signer); +} + +rule uniqueSigner(){ + env e; + + uint256 firstX; + uint256 firstY; + P256.Verifiers firstVerifier; + + uint256 firstSignerValue = getSignerHarnessed(e, firstX, firstY, firstVerifier); + require firstSignerValue <= max_uint160; // <=== needed assumption + + address firstSigner = castToAddress(e, firstSignerValue); + + uint256 secondX; + uint256 secondY; + P256.Verifiers secondVerifier; + + uint256 secondSignerValue = getSignerHarnessed(e, secondX, secondY, secondVerifier); + require secondSignerValue <= max_uint160; // <=== needed assumption + + address secondSigner = castToAddress(e, secondSignerValue); + + assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Deterministic address in get signer (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule deterministicSigner() +{ + env e1; + env e2; + + uint x; + uint y; + P256.Verifiers verifier; + + address signer = getSigner(e1, x, y, verifier); + + assert signer == getSigner(e2, x, y, verifier); +} \ No newline at end of file diff --git a/modules/passkey/certora/specs/ProxySimulator.spec b/modules/passkey/certora/specs/ProxySimulator.spec new file mode 100644 index 00000000..e04d33f1 --- /dev/null +++ b/modules/passkey/certora/specs/ProxySimulator.spec @@ -0,0 +1,54 @@ +using SafeWebAuthnSignerProxy as SafeWebAuthnSignerProxy; +using WebAuthnHarnessWithMunge 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 _._ external => DISPATCH [ + SafeWebAuthnSignerProxy._, + SafeWebAuthnSignerSingleton._ + ] default NONDET; +} + +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; +} + +// This is the same MAGIC_VALUE constant used in ERC1271. +definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); + +/* +Property 14. Proxy - verify return data from the fallback is only one of the magicNumbers +Uses another contract that simulates interaction with the proxy. The reason is that the prover doesn't check all +possible calldata values so this simulation will make the prover choose different values that will be passed on the calldata. +Rule stuck. +*/ +rule proxyReturnValue { + env e; + bytes32 message; + bytes signature; + + bytes4 ret = authenticate(e, message, signature); + + satisfy ret == MAGIC_VALUE() || ret == to_bytes4(0); +} diff --git a/modules/passkey/certora/specs/SafeWebAuthnSignerFactory.spec b/modules/passkey/certora/specs/SafeWebAuthnSignerFactory.spec new file mode 100644 index 00000000..8522d88e --- /dev/null +++ b/modules/passkey/certora/specs/SafeWebAuthnSignerFactory.spec @@ -0,0 +1,248 @@ +using SafeWebAuthnSignerProxy as proxy; +using SafeWebAuthnSignerSingleton as singleton; +using WebAuthnHarnessWithMunge as WebAuthnHarness; + + +methods{ + function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v); + function createSigner(uint256, uint256, P256.Verifiers) external returns (address); + function hasNoCode(address) external returns (bool) envfree; + + 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 _.isValidSignature(bytes32,bytes) external => DISPATCHER(optimistic=true, use_fallback=true); + + function _._ external => DISPATCH [ + proxy._, + singleton._ + ] default NONDET; +} + +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 { + 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; +} + +// Summary is correct only if the unique signer rule is proved spec GetSigner +ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address { + axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1. + forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2. + (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); +} + +definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Singleton implementation never change (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule singletonNeverChanges() +{ + env e; + method f; + calldataarg args; + address currentSingleton = currentContract.SINGLETON; + + f(e, args); + + assert currentSingleton == currentContract.SINGLETON; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ createSigner and getSigner always returns the same address (Proved under assumption) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule createAndGetSignerEquivalence(){ + env e; + + uint256 createX; + uint256 createY; + P256.Verifiers createVerifier; + + address signer1 = createSigner(e, createX, createY, createVerifier); + + uint256 getX; + uint256 getY; + P256.Verifiers getVerifier; + + address signer2 = getSigner(e, getX, getY, getVerifier); + + assert signer1 == signer2 <=> (createX == getX && createY == getY && createVerifier == getVerifier); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Correctness of Signer Creation. (Cant called twice and override) (Bug CERT-6252) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +ghost mathint numOfCreation; +ghost mapping(address => uint) address_map; +ghost address signerAddress; + +hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{ + require(v == signerAddress); + numOfCreation = numOfCreation + 1; +} + +rule SignerCreationCantOverride() +{ + env e; + require numOfCreation == 0; + + uint x; + uint y; + P256.Verifiers verifier; + + address a = getSigner(e, x, y, verifier); + require address_map[a] == 0; + + createSigner(e, x, y, verifier); + createSigner@withrevert(e, x, y, verifier); + + assert numOfCreation < 2; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Has no code integrity (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule hasNoCodeIntegrity() +{ + address a; + assert (a == proxy) => !hasNoCode(a); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner equiv to first deploying the signer with the factory, and then | +| verifying the signature with it directly (CERT-6221) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule createAndVerifyEQtoIsValidSignatureForSigner() +{ + env e; + uint x; + uint y; + P256.Verifiers verifier; + bytes signature; + bytes32 message; + + signerAddress = getSigner(e, x, y, verifier); + require(numOfCreation == 0); + require(hasNoCode(e, signerAddress)); + require(WebAuthnHarness.castSignatureSuccess(e, message, signature)); + + + storage s = lastStorage; + + bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + + bytes4 magic2 = createAndVerify(e, message, signature, x, y, verifier) at s; + + assert magic1 == magic2 && numOfCreation == 1; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner Consistency (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule isValidSignatureForSignerConsistency(method f) filtered { + f -> f.selector != sig:WebAuthnHarness.encodeClientDataJson(bytes32,string).selector +} { + env e; + env e1; + env e2; + require e1.msg.value == 0 && e2.msg.value == 0; + + calldataarg args; + + uint x; + uint y; + P256.Verifiers verifier; + + bytes signature; + bytes32 message; + + bytes4 magic1 = isValidSignatureForSigner@withrevert(e1, message, signature, x, y, verifier); + bool firstRevert = lastReverted; + + f(e, args); + + bytes4 magic2 = isValidSignatureForSigner@withrevert(e2, message, signature, x, y, verifier); + bool secondRevert = lastReverted; + + assert firstRevert == secondRevert; + assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner Integrity (Violated) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule isValidSignatureForSignerIntegrity() +{ + env e; + + uint x; + uint y; + P256.Verifiers verifier; + bytes signature; + bytes32 message; + + bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + + satisfy magic1 == MAGIC_VALUE(); +} + + +rule getSignerRevertingConditions { + env e; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + bool triedTransferringEth = e.msg.value != 0; + + getSigner@withrevert(e, x, y, verifiers); + + assert lastReverted <=> triedTransferringEth; +} diff --git a/modules/passkey/certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec b/modules/passkey/certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec new file mode 100644 index 00000000..8522d88e --- /dev/null +++ b/modules/passkey/certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec @@ -0,0 +1,248 @@ +using SafeWebAuthnSignerProxy as proxy; +using SafeWebAuthnSignerSingleton as singleton; +using WebAuthnHarnessWithMunge as WebAuthnHarness; + + +methods{ + function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v); + function createSigner(uint256, uint256, P256.Verifiers) external returns (address); + function hasNoCode(address) external returns (bool) envfree; + + 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 _.isValidSignature(bytes32,bytes) external => DISPATCHER(optimistic=true, use_fallback=true); + + function _._ external => DISPATCH [ + proxy._, + singleton._ + ] default NONDET; +} + +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 { + 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; +} + +// Summary is correct only if the unique signer rule is proved spec GetSigner +ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address { + axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1. + forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2. + (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); +} + +definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Singleton implementation never change (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule singletonNeverChanges() +{ + env e; + method f; + calldataarg args; + address currentSingleton = currentContract.SINGLETON; + + f(e, args); + + assert currentSingleton == currentContract.SINGLETON; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ createSigner and getSigner always returns the same address (Proved under assumption) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule createAndGetSignerEquivalence(){ + env e; + + uint256 createX; + uint256 createY; + P256.Verifiers createVerifier; + + address signer1 = createSigner(e, createX, createY, createVerifier); + + uint256 getX; + uint256 getY; + P256.Verifiers getVerifier; + + address signer2 = getSigner(e, getX, getY, getVerifier); + + assert signer1 == signer2 <=> (createX == getX && createY == getY && createVerifier == getVerifier); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Correctness of Signer Creation. (Cant called twice and override) (Bug CERT-6252) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +ghost mathint numOfCreation; +ghost mapping(address => uint) address_map; +ghost address signerAddress; + +hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{ + require(v == signerAddress); + numOfCreation = numOfCreation + 1; +} + +rule SignerCreationCantOverride() +{ + env e; + require numOfCreation == 0; + + uint x; + uint y; + P256.Verifiers verifier; + + address a = getSigner(e, x, y, verifier); + require address_map[a] == 0; + + createSigner(e, x, y, verifier); + createSigner@withrevert(e, x, y, verifier); + + assert numOfCreation < 2; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Has no code integrity (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule hasNoCodeIntegrity() +{ + address a; + assert (a == proxy) => !hasNoCode(a); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner equiv to first deploying the signer with the factory, and then | +| verifying the signature with it directly (CERT-6221) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule createAndVerifyEQtoIsValidSignatureForSigner() +{ + env e; + uint x; + uint y; + P256.Verifiers verifier; + bytes signature; + bytes32 message; + + signerAddress = getSigner(e, x, y, verifier); + require(numOfCreation == 0); + require(hasNoCode(e, signerAddress)); + require(WebAuthnHarness.castSignatureSuccess(e, message, signature)); + + + storage s = lastStorage; + + bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + + bytes4 magic2 = createAndVerify(e, message, signature, x, y, verifier) at s; + + assert magic1 == magic2 && numOfCreation == 1; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner Consistency (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule isValidSignatureForSignerConsistency(method f) filtered { + f -> f.selector != sig:WebAuthnHarness.encodeClientDataJson(bytes32,string).selector +} { + env e; + env e1; + env e2; + require e1.msg.value == 0 && e2.msg.value == 0; + + calldataarg args; + + uint x; + uint y; + P256.Verifiers verifier; + + bytes signature; + bytes32 message; + + bytes4 magic1 = isValidSignatureForSigner@withrevert(e1, message, signature, x, y, verifier); + bool firstRevert = lastReverted; + + f(e, args); + + bytes4 magic2 = isValidSignatureForSigner@withrevert(e2, message, signature, x, y, verifier); + bool secondRevert = lastReverted; + + assert firstRevert == secondRevert; + assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner Integrity (Violated) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule isValidSignatureForSignerIntegrity() +{ + env e; + + uint x; + uint y; + P256.Verifiers verifier; + bytes signature; + bytes32 message; + + bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + + satisfy magic1 == MAGIC_VALUE(); +} + + +rule getSignerRevertingConditions { + env e; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + bool triedTransferringEth = e.msg.value != 0; + + getSigner@withrevert(e, x, y, verifiers); + + assert lastReverted <=> triedTransferringEth; +} diff --git a/modules/passkey/certora/specs/SafeWebAuthnSignerProxy.spec b/modules/passkey/certora/specs/SafeWebAuthnSignerProxy.spec new file mode 100644 index 00000000..65532fa5 --- /dev/null +++ b/modules/passkey/certora/specs/SafeWebAuthnSignerProxy.spec @@ -0,0 +1,67 @@ +using SafeWebAuthnSignerSingleton as SafeWebAuthnSignerSingleton; + +persistent ghost uint delegateSuccess; + +hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + // DELEGATECALL is used in this contract, but it only ever calls into the singleton. + assert (executingContract != currentContract || addr == SafeWebAuthnSignerSingleton, + "we should only `delegatecall` into the singleton." + ); + delegateSuccess = rc; +} + +/* +Property 11. Proxy - Immutability of Configuration Parameters (x, y, Singleton, verifier) +x, y, singleton and verifiers never changes after any function call. +Rule verified. +*/ +rule configParametersImmutability { + env e; + method f; + calldataarg args; + + address singletonBefore = currentContract._SINGLETON; + uint256 xBefore = currentContract._X; + uint256 yBefore = currentContract._Y; + P256.Verifiers verifiersBefore = currentContract._VERIFIERS; + + f(e, args); + + address singletonAfter = currentContract._SINGLETON; + uint256 xAfter = currentContract._X; + uint256 yAfter = currentContract._Y; + P256.Verifiers verifiersAfter = currentContract._VERIFIERS; + + assert singletonBefore == singletonAfter && + xBefore == xAfter && + yBefore == yAfter && + verifiersBefore == verifiersAfter; +} + +/* +Property 12. Proxy - Delegate Call Integrity (calls the Singleton) +Hooking on delegate calls will make sure we'll get a violation if the singleton isn't the contract called. +Rule verified. +*/ +rule delegateCallsOnlyToSingleton { + env e; + method f; + calldataarg args; + + f(e, args); + + assert true; +} + +/* +Property 13. Proxy - Fallback reverting conditions. +Fallback reverts iff the delegatecall didn't succeed. Data manipulation does not revert. +Rule verified. +*/ +rule fallbackRevertingConditions(method f, calldataarg args) filtered { f -> f.isFallback } { + env e; + + f@withrevert(e, args); + + assert lastReverted <=> delegateSuccess == 0; +} diff --git a/modules/passkey/certora/specs/SafeWebAuthnSignerSingleton.spec b/modules/passkey/certora/specs/SafeWebAuthnSignerSingleton.spec new file mode 100644 index 00000000..faa8e2e0 --- /dev/null +++ b/modules/passkey/certora/specs/SafeWebAuthnSignerSingleton.spec @@ -0,0 +1,154 @@ +using WebAuthnHarnessWithMunge 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 SafeWebAuthnSignerFactory.getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v); +} + +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 { + 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; +} + +// Summary is correct only if the unique signer rule is proved spec GetSigner +ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address { + axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1. + forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2. + (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); +} + +definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Implementation of isValidSignature Function (Integrity) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule verifySignatureUniqueness(env e){ + bytes32 first_message; + bytes32 second_message; + WebAuthn.Signature sigStruct; + bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct); + + bytes4 first_message_verified = isValidSignature(e, first_message, signature); + bytes4 second_message_verified = isValidSignature(e, second_message, signature); + + assert (first_message != second_message) => !(first_message_verified == MAGIC_VALUE() && second_message_verified == MAGIC_VALUE()); + satisfy true; +} + +rule verifySignatureIntegrity(env e){ + bytes32 first_message; + bytes32 second_message; + WebAuthn.Signature sigStruct; + bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct); + + bytes4 first_message_verified = isValidSignature(e, first_message, signature); + require (first_message_verified == MAGIC_VALUE()); + + bytes4 second_message_verified = isValidSignature(e, second_message, signature); + + assert (second_message_verified == MAGIC_VALUE()) <=> (first_message == second_message); + satisfy true; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Both isValidSignature behave the same way │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule verifyIsValidSignatureAreEqual(env e){ + bytes data; + bytes first_signature; + WebAuthn.Signature sigStruct; + first_signature = WebAuthnHarness.encodeSignature(e, sigStruct); + + bytes4 magicValue_hashed = isValidSignature(e, data, first_signature); + + bytes32 message; + bytes4 magicValue_message = isValidSignature(e, message, first_signature); + + 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(0) && magicValue_message == to_bytes4(0)); + satisfy (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(method f) filtered { + f -> f.selector != sig:WebAuthnHarness.encodeClientDataJson(bytes32,string).selector +} { + env e; + require e.msg.value == 0; + + calldataarg args; + + bytes32 message; + bytes signature; + + bytes4 firstVerified = isValidSignature@withrevert(e, message, signature); + bool firstReverted = lastReverted; + + f(e, args); + + bytes4 secondVerify = isValidSignature@withrevert(e, message, signature); + bool secondRevert = lastReverted; + + assert firstReverted == secondRevert; + assert (!firstReverted && !secondRevert) => (firstVerified == secondVerify); + + satisfy (!firstReverted && firstVerified == to_bytes4(0x1626ba7e)); + satisfy true; +} + +rule isValidSignatureRevertingConditions { + env e; + bytes32 message; + + WebAuthn.Signature sigStruct; + bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct); + + bool triedTransferringEth = e.msg.value != 0; + bool dataLengthInsufficient = sigStruct.authenticatorData.length <= 32; + + isValidSignature@withrevert(e, message, signature); + + assert lastReverted <=> (triedTransferringEth || dataLengthInsufficient); +} diff --git a/modules/passkey/certora/specs/WebAuthn.spec b/modules/passkey/certora/specs/WebAuthn.spec new file mode 100644 index 00000000..ca1f5f5a --- /dev/null +++ b/modules/passkey/certora/specs/WebAuthn.spec @@ -0,0 +1,316 @@ + +methods { + function WebAuthn.encodeClientDataJson(bytes32 challenge, string calldata clientDataFields) internal returns (string memory) => + SencodeDataJsonCVL(challenge, clientDataFields); + + function checkInjective(bytes32 challenge, bytes32 clientDataFields, bytes32 result) internal returns (bool) => + checkInjectiveSummary(challenge, clientDataFields, result); + + 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 SencodeDataJsonCVL(bytes32 challenge, string clientDataFields) returns string +{ + env e; + return summaryEncodeDataJson(e, challenge, clientDataFields); +} + +ghost checkInjectiveSummary(bytes32, bytes32, bytes32) returns bool { + axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 x2. forall bytes32 y2. forall bytes32 result. + (checkInjectiveSummary(x1, y1, result) && checkInjectiveSummary(x2, y2, 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; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ shaIntegrity 2 different inputs results in 2 different hashes (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule shaIntegrity(){ + env e; + + bytes input1; + bytes input2; + + bytes32 input1_sha = getSha256(e, input1); + bytes32 input2_sha = getSha256(e, input2); + + assert (keccak256(input1) != keccak256(input2)) <=> input1_sha != input2_sha; +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ every 2 challenges results in unique message when using encodeSigningMessage (Timeout cert-6290) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule uniqueMessagePerChallenge(){ + env e; + + bytes32 challenge1; + bytes32 challenge2; + bytes authenticatorData; + require authenticatorData.length % 32 == 0; + string clientDataField; + + bytes message1 = encodeSigningMessage(e, challenge1, authenticatorData, clientDataField); + bytes message2 = encodeSigningMessage(e, challenge2, authenticatorData, clientDataField); + + assert (challenge1 != challenge2) <=> (getSha256(e, message1) != getSha256(e, message2)); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ verifySignature functions are equivalent (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule verifySignatureEq(){ + env e; + + // verify signature related args + bytes32 challenge; + WebAuthn.AuthenticatorFlags authenticatorFlags; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + // signature related args + bytes authenticatorData; + string clientDataFields; + uint256 r; + uint256 s; + bytes bytesSignature; + WebAuthn.Signature structSignature; + + bytesSignature, structSignature = prepareSignature(e, authenticatorData, clientDataFields, r, s); + + storage firstStorage = lastStorage; + + bool result1 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers); + bool firstCallRevert = lastReverted; + + bool result2 = verifySignature@withrevert(e, challenge, structSignature, authenticatorFlags, x, y, verifiers) at firstStorage; + bool secondCallRevert = lastReverted; + + assert firstCallRevert == secondCallRevert; + assert (!firstCallRevert && !secondCallRevert) => result1 == result2; +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ verifySignature consistent (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule verifySignatureConsistent(){ + env e; + env e1; + env e2; + require e1.msg.value == 0 && e2.msg.value == 0; + calldataarg args; + + bytes32 challenge; + WebAuthn.AuthenticatorFlags authenticatorFlags; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + bytes bytesSignature; + + + bool result1 = verifySignature@withrevert(e1, challenge, bytesSignature, authenticatorFlags, x, y, verifiers); + bool firstCallRevert = lastReverted; + + + bool result2 = verifySignature@withrevert(e2, challenge, bytesSignature, authenticatorFlags, x, y, verifiers); + bool secondCallRevert = lastReverted; + + assert firstCallRevert == secondCallRevert; + assert (!firstCallRevert && !secondCallRevert) => result1 == result2; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ CastSignature Consistent (Once valid always valid, Once failed always failed, includes revert cases and middle call)| +│ (Proved) | +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule castSignatureConsistent(){ + env e; + env e1; + env e2; + + require (e1.msg.value == e2.msg.value) && (e1.msg.value == e.msg.value) && (e.msg.value == 0); + + calldataarg args; + + bytes signature; + + bool firstIsValid; + WebAuthn.Signature firstData; + + bool secondIsValid; + WebAuthn.Signature secondData; + + firstIsValid, firstData = castSignature@withrevert(e1, signature); + bool firstRevert = lastReverted; + + + secondIsValid, secondData = castSignature@withrevert(e2, signature); + bool secondRevert = lastReverted; + + if (!firstRevert && !secondRevert) { + assert compareSignatures(e, firstData, secondData) && firstIsValid == secondIsValid; + } + + assert (firstRevert == secondRevert); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ CastSignature Canonical Deterministic Decoding (Proved) | +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule castSignatureDeterministicDecoding(){ + env e; + + WebAuthn.Signature structSignature; + bytes encodeSig = encodeSignature(e, structSignature); + + WebAuthn.Signature decodedSignature; + bool isValid; + + isValid, decodedSignature = castSignature(e, encodeSig); + + assert isValid <=> compareSignatures(e, structSignature, decodedSignature); +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ CastSignature Length Check Validity (Proved) | +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +/* note: the rule requires specific features still not available on a stable certora-cli +rule castSignatureLengthCheckValidity(){ + env e; + + WebAuthn.Signature structSignature; + bytes encodeSig; + + WebAuthn.Signature decodedSignature; + bool isValid; + + isValid, decodedSignature = castSignature(e, encodeSig); + bool length_is_correct = encodeSig.length <= encodeSignature(e, decodedSignature).length; + + assert isValid <=> length_is_correct; +} +*/ +/* +┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ castSignature Reverting Conditions | +| Will only revert if function was paid. | +| Passes - https://prover.certora.com/output/15800/9d6be0f24e094ffe94b9faf1ed8bfc8f?anonymousKey=517b64e4e1693de5294f836400a5581fc7ec0bcf | +└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule castSignatureRevertingConditions { + env e; + bytes signature; + + bool triedTransferringEth = e.msg.value != 0; + + castSignature_notreturns@withrevert(e, signature); + + assert lastReverted <=> triedTransferringEth; +} + +/* +┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ encodeClientDataJson Reverting Conditions | +| Will only revert if function was paid. | +| Passes - https://prover.certora.com/output/15800/ccc8d2fd45b04cf5ac8efdf263820324?anonymousKey=68d9ae2e6f4f22dd7aae9f8bddbc5faf7de12df1 | +└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule encodeClientDataJsonRevertingConditions { + env e; + bytes32 challenge; + string clientDataFields; + + bool triedTransferringEth = e.msg.value != 0; + + encodeClientDataJson@withrevert(e, challenge, clientDataFields); + + assert lastReverted <=> triedTransferringEth; +} + +/* +┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ encodeSigningMessage Reverting Conditions | +| Will only revert if function was paid. | +| Passes - https://prover.certora.com/output/15800/93685eaf7e7146eabaa38125dc32f29b?anonymousKey=eaf6d4135849f0476d8e9e6a758cca8818a96b94 | +└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule encodeSigningMessageRevertingConditions { + env e; + bytes32 challenge; + bytes authenticatorData; + string clientDataFields; + + bool triedTransferringEth = e.msg.value != 0; + + encodeSigningMessage@withrevert(e, challenge, authenticatorData, clientDataFields); + + assert lastReverted <=> triedTransferringEth; +} + +/* +┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ checkAuthenticatorFlags Reverting Conditions | +| Will only revert if function was paid or the bytes array `authenticatorData`'s length is too small (<= 32 bytes). | +| Passes - https://prover.certora.com/output/15800/d2d34792998c479db5f38430efc7dc8b?anonymousKey=7e68511768f3da35bdb9f75c9f86d40d2e07e2aa | +└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule checkAuthenticatorFlagsRevertingConditions { + env e; + bytes authenticatorData; + WebAuthn.AuthenticatorFlags authenticatorFlags; + + bool triedTransferringEth = e.msg.value != 0; + bool dataLengthInsufficient = authenticatorData.length <= 32; + + checkAuthenticatorFlags@withrevert(e, authenticatorData, authenticatorFlags); + + assert lastReverted <=> (triedTransferringEth || dataLengthInsufficient); +} + +/* +┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ verifySignature Reverting Conditions | +| Will only revert if function was paid or the bytes array `authenticatorData`'s in `signature` length is too small (<= 32 bytes). | +| Passes - https://prover.certora.com/output/15800/d2d34792998c479db5f38430efc7dc8b?anonymousKey=7e68511768f3da35bdb9f75c9f86d40d2e07e2aa | +└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule verifySignatureRevertingConditions { + env e; + bytes32 challenge; + WebAuthn.Signature signature; + WebAuthn.AuthenticatorFlags authenticatorFlags; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + bool triedTransferringEth = e.msg.value != 0; + bool dataLengthInsufficient = signature.authenticatorData.length <= 32; + + verifySignature@withrevert(e, challenge, signature, authenticatorFlags, x, y, verifiers); + + assert lastReverted <=> (triedTransferringEth || dataLengthInsufficient); +} diff --git a/modules/passkey/package.json b/modules/passkey/package.json index 870c43e0..1ee6b84a 100644 --- a/modules/passkey/package.json +++ b/modules/passkey/package.json @@ -34,6 +34,7 @@ "codesize": "hardhat codesize", "deploy-all": "hardhat deploy-contracts --network", "deploy": "hardhat deploy --network", + "deploy-custom": "rm -rf deployments/custom && npm run deploy custom", "fmt": "prettier --write .", "fmt:check": "prettier --check .", "lint": "pnpm run lint:sol && pnpm run lint:ts", diff --git a/modules/recovery/package.json b/modules/recovery/package.json index 15cc2d54..68db638a 100644 --- a/modules/recovery/package.json +++ b/modules/recovery/package.json @@ -16,6 +16,7 @@ "build:sol": "rimraf build typechain-types && hardhat compile", "build:ts": "rimraf dist && tsc", "deploy-all": "hardhat deploy-contracts --network", + "deploy-custom": "rm -rf deployments/custom && npm run deploy custom", "lint": "pnpm run lint:ts", "lint:ts": "eslint ./src", "lint:fix": "eslint ./src --fix",