Update certora-cli to 7.3.0

[ernestognw]

Replaces #4957 and #5019

PR Checklist

• Tests
• Documentation
• Changeset entry (run npx changeset add)

[socket-security]

New and removed dependencies detected. Learn more about Socket for GitHub ↗︎

Package	New capabilities	Transitives	Size	Publisher
pypi/[email protected]	environment, eval, filesystem, network, shell	0	22.7 MB	certora, shellyg

View full report↗︎

[ernestognw]

The CI uses 0.8.24. When I compile locally with 0.8.25 everything works fine but switching to 0.8.24 produce the same results as the CI.

I'll keep investigating

[changeset-bot]

⚠️ No Changeset found

Latest commit: 2e9cd8c

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

[Amxx]

Note: ERC721 safeMint and safeTransferFrom rules fail because failure of the underlying checkOnERC721Received is not modeled in the assert success <=> (...); description on liveness.

AFAIK, we a few options (in order of difficulty):

• require that to has no code in the rule
• require that to has no code, or that the check passes in the helper
• "leak" the data for the helper (return value) to verify the check in the liveness assert

[ernestognw]

Note: ERC721 safeMint and safeTransferFrom rules fail because failure of the underlying checkOnERC721Received is not modeled in the assert success <=> (...); description on liveness.

I am not sure of that since we're summarizing the result of an onERC721Received call so the checkOnERC721Received should not fail. The summarization is in certora/specs/methods/IERC721Receiver.spec.

Am I missing something?

[Amxx]

I'm not sure why that happens, but clearly there is an issue here

See this.

[ernestognw]

Attempted to retake this, and found a couple of issues. New errors appear in pretty much every spec, similar to the following:

EVM instruction at PC 2786 jumps to unknown destination 5140, from 2783#2705/16. Possible unresolved function pointer.

Also the CLI hangs up when I run node certora/run.js --all, and most importantly, the Certora Prover and the CLI report the jobs succeded even though the verification of multiple rules failed. My guess is that they might have changed the definition of what a successful verification is, possibly affecting our CI as well.

Here's how Certora is presenting the status as passed although rules didn't:

[socket-security]

🚨 Potential security issues detected. Learn more about Socket for GitHub ↗︎

To accept the risk, merge this PR and you will not be notified again.

Alert	Package	Note	Source	CI
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫
AI-detected potential code anomaly	pypi/[email protected]	Notes: The code contains multiple potential security risks, including unauthorized file writes, command injection, information leakage, and code injection. It should be reviewed and modified to ensure proper input validation, sanitization, and secure handling of user input. The presence of 'eval' raises concerns about the safety and security of the code. Confidence: 0.80 Severity: 0.70	fv-requirements.txt	🚫

View full report↗︎

Next steps

What is an AI-detected potential code anomaly?

AI has identified unusual behaviors that may pose a security risk.

An AI system found a low-risk anomaly in this package. It may still be fine to use, but you should check that it is safe before proceeding.

Take a deeper look at the dependency

Take a moment to review the security alert above. Review the linked package source code to understand the potential risk. Ensure the package is not malicious before proceeding. If you're unsure how to proceed, reach out to your security team or ask the Socket team for help at support [AT] socket [DOT] dev.

Remove the package

If you happen to install a dependency that Socket reports as Known Malware you should immediately remove it and select a different dependency. For other alert types, you may may wish to investigate alternative packages or consider if there are other ways to mitigate the specific risk posed by the dependency.

Mark a package as acceptable risk

To ignore an alert, reply with a comment starting with @SocketSecurity ignore followed by a space separated list of ecosystem/package-name@version specifiers. e.g. @SocketSecurity ignore npm/[email protected] or ignore all packages with @SocketSecurity ignore-all

• @SocketSecurity ignore pypi/[email protected]
• @SocketSecurity ignore pypi/[email protected]
• @SocketSecurity ignore pypi/[email protected]
• @SocketSecurity ignore pypi/[email protected]
• @SocketSecurity ignore pypi/[email protected]
• @SocketSecurity ignore pypi/[email protected]
• @SocketSecurity ignore pypi/[email protected]