diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/README.md b/01.Lesson_GettingStarted/ERC20Lesson1/README.md index 1f77e03a..d5c13e9a 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/README.md +++ b/01.Lesson_GettingStarted/ERC20Lesson1/README.md @@ -76,6 +76,11 @@ certoraRun --help
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***ERC20***. +
+ ### ***Results*** The prover will print various information to the console. @@ -99,6 +104,20 @@ Follow the "Verification results" link in the command line, or go to [prover.cer You'll see a table with the verification results, similar to this image: ![results](images/results.jpg) For each rule, the table either displays a checkmark when the rule was proved or a x-mark when a violation of the rule was discovered. +
+ +## Results in VSCode IDE ## + +The results will appear under the job title. After a job is sent to the cloud, the 'Go To Rule Report' icon to the left of +the job will turn light blue. Clicking it will open the rule report in the web. + +![Screen Shot 2023-03-07 at 11 21 42](https://user-images.githubusercontent.com/101042618/223378848-63242073-2987-4efd-adc9-fbb155344837.png) + +To see the call trace, click a violated rule's details: + +![Screen Shot 2023-03-07 at 11 24 10](https://user-images.githubusercontent.com/101042618/223379486-a728d578-4f72-481f-ab8f-959dd4451db3.png) + +
## Understanding Rule Violations @@ -131,6 +150,11 @@ No violations were found. Great!
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the job ***bankfixed integrityofdeposit***. +
+ ## Preconditions and Helper Variables Let’s define [another property](TotalGreaterThanUser.spec) and verify that after mint, the `totalSupply` in the system is at least the balance of the beneficiary: @@ -176,6 +200,11 @@ You will see the message in the run results mail and in the job's list in [prove
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the jobs ***bankfixed totalfundsafterdepos*** and ***bankfixed running with precondition***. +
+ ## Parametric Rules Many properties can be generalized to be used for all functions. @@ -209,3 +238,9 @@ Notice that this rule uncovers a bug in `decreaseAllowance`. Parametric rules enable expressing reusable and concise correctness conditions. Note that they are not dependent on the implementation. You can integrate them easily into the CI to verify changes to the code, including signature changes, new functions, and implementation changes. + +
+### ***Running in the IDE*** + +Alternatively, use the ***Certora VSCode extension IDE*** to run the jobs ***parametric rule on bank*** and ***parametric rule on bankfixed***. +
diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf new file mode 100644 index 00000000..24cd4d84 --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "01 erc20", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf new file mode 100644 index 00000000..e6a22624 --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_fixed.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20Fixed.spec" + ], + "solc": "solc8.0", + "msg": "01 erc20 fixed", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf new file mode 100644 index 00000000..cb61d910 --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_parametric_rule.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:Parametric.spec" + ], + "solc": "solc8.0", + "msg": "01 erc20 parametric rule", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf new file mode 100644 index 00000000..1ec7471b --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermint.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:TotalGreaterThanUser.spec" + ], + "solc": "solc8.0", + "msg": "01 erc20 totalsupplyaftermint", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "rule": [ + "totalSupplyAfterMint" + ], + "process": "emv", + "settings": [ + "-rule=totalSupplyAfterMint" + ] +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf new file mode 100644 index 00000000..fc5967b0 --- /dev/null +++ b/01.Lesson_GettingStarted/ERC20Lesson1/certora/conf/01_erc20_totalsupplyaftermintwithpr.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "ERC20.sol:ERC20" + ], + "verify": [ + "ERC20:TotalGreaterThanUser.spec" + ], + "solc": "solc8.0", + "msg": "01 erc20 totalsupplyaftermintwithpr", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "rule": [ + "totalSupplyAfterMintWithPrecondition" + ], + "process": "emv", + "settings": [ + "-rule=totalSupplyAfterMintWithPrecondition" + ] +} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/README.md b/01.Lesson_GettingStarted/README.md index dfc369fc..546da294 100644 --- a/01.Lesson_GettingStarted/README.md +++ b/01.Lesson_GettingStarted/README.md @@ -16,7 +16,10 @@ - [ ] In the VSCode extensions/marketplace search for [Certora Verification Language LSP](https://marketplace.visualstudio.com/items?itemName=Certora.evmspec-lsp) and install it. This is an extension developed for supporting the spec language - the language in which we will be writing specifications. The extension supports syntax highlighting, autocompletion and more. -- [ ] It is also recommended to install the [Ethereum Security Bundle](https://marketplace.visualstudio.com/items?itemName=tintinweb.ethereum-security-bundle) by tintinweb on the VSCode extensions/marketplace, to get support for the Solidity contracts. +- [x] It is recommanded to install [Certora IDE](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover) in the VSCode extensions/marketplace as well, to get an easy-to-use interface for running jobs. + +- [x] It is also recommended to install the [Ethereum Security Bundle](https://marketplace.visualstudio.com/items?itemName=tintinweb.ethereum-security-bundle) by tintinweb on the VSCode extensions/marketplace, to get support for the Solidity contracts. +
diff --git a/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf b/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf new file mode 100644 index 00000000..8015e4d8 --- /dev/null +++ b/02.Lesson_InvestigateViolations/Borda/certora/conf/02_borda_bug_1.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "BordaBug1.sol:Borda" + ], + "verify": [ + "Borda:Borda.spec" + ], + "solc": "solc7.6", + "msg": "02 borda bug 1", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf b/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf new file mode 100644 index 00000000..a08dfa63 --- /dev/null +++ b/02.Lesson_InvestigateViolations/ERC20/certora/conf/02_erc20_bug_fixed.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "ERC20Fixed.sol:ERC20" + ], + "verify": [ + "ERC20:ERC20.spec" + ], + "solc": "solc8.0", + "msg": "02 erc20 bug fixed", + "optimistic_loop": true, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf new file mode 100644 index 00000000..8b50a337 --- /dev/null +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/certora/conf/02_meeting_scheduler_bug_1.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "MeetingSchedulerBug1.sol:MeetingScheduler" + ], + "verify": [ + "MeetingScheduler:meetings.spec" + ], + "solc": "solc8.7", + "msg": "02 meeting scheduler bug 1", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/02.Lesson_InvestigateViolations/README.md b/02.Lesson_InvestigateViolations/README.md index 9d1d0d8b..edf5aef9 100644 --- a/02.Lesson_InvestigateViolations/README.md +++ b/02.Lesson_InvestigateViolations/README.md @@ -34,11 +34,12 @@ For each of the systems in this directory do as follows:
- [ ] Create a script (or multiple scripts) that will serve you for running the verifications of the system's buggy versions. +- [ ] Alternatively, create a new empty job in the VSCode IDE or upload an existing file. > :bulb: >
> Script Hint -> Craft your script wisely - use the `--rule` to filter out information that isn't of your interest. +> Craft your script wisely - use the `--rule` to filter out information that isn't of your interest ('Rules' is under 'Certora Spec' in the IDE's settings form). >

diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md b/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md index 5bd30fc0..a291f62e 100644 --- a/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/README.md @@ -34,7 +34,9 @@ You can read about the catch in the following [blog post](https://blog.makerdao. - [ ] Run the script [runBroken.sh](runBroken.sh) and get a violation. Investigate the reason for the fail and see that you understand it. +- [ ] Alternatively, run the job [run_broken](run_broken.conf) and get a violation. Investigate the reason for the fail and see that you understand it. + - [ ] Try to suggest a solution that will mitigate the wrongful behavior. -- [ ] Compare the 2 contracts - [Auction Broken](AuctionBroken.sol) and [Auction Fixed](AuctionFixed.sol) to find the fix. Run the script [runFixed.sh](runFixed.sh) and see that it is indeed solving the problem. +- [ ] Compare the 2 contracts - [Auction Broken](AuctionBroken.sol) and [Auction Fixed](AuctionFixed.sol) to find the fix. Run the script [runFixed.sh](runFixed.sh) or the job [run_fixed](run_fixed.conf) and see that it is indeed solving the problem. Were you thinking of the same solution or did you think of another one? There could be more than 1 correct answer. diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf new file mode 100644 index 00000000..3c1ab793 --- /dev/null +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_broken.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "AuctionBroken.sol:System" + ], + "verify": [ + "System:Auction.spec" + ], + "solc": "solc5.12", + "msg": "06 run broken", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true +} \ No newline at end of file diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf new file mode 100644 index 00000000..9cda34c9 --- /dev/null +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/certora/conf/06_run_fixed.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "AuctionFixed.sol:System" + ], + "verify": [ + "System:Auction.spec" + ], + "solc": "solc5.12", + "msg": "06 run fixed", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf b/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf new file mode 100644 index 00000000..aa803b19 --- /dev/null +++ b/06.Lesson_ThinkingProperties/ThinkingPropertiesExercise/TicketDepot/certora/conf/06_ticket_depot_sanity.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "TicketDepot.sol:TicketDepot" + ], + "verify": [ + "TicketDepot:sanity.spec" + ], + "solc": "solc6.12", + "msg": "06 ticket depot sanity", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf new file mode 100644 index 00000000..9b6fdcd0 --- /dev/null +++ b/07.Lesson_InductiveReasoning/InductionLesson/BallGame/certora/conf/07_ball_game.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "BallGame.sol:BallGame" + ], + "verify": [ + "BallGame:BallGame.spec" + ], + "solc": "solc8.6", + "msg": "07 ball game", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true, + "process": "emv" +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf new file mode 100644 index 00000000..336cb175 --- /dev/null +++ b/07.Lesson_InductiveReasoning/InductionLesson/Manager/certora/conf/07_manager.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "Manager.sol:Manager" + ], + "verify": [ + "Manager:Manager.spec" + ], + "solc": "solc8.6", + "msg": "07 manager", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "smt_timeout": "600", + "loop_iter": "1", + "disableLocalTypeChecking": false +} \ No newline at end of file diff --git a/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf new file mode 100644 index 00000000..7611b96f --- /dev/null +++ b/07.Lesson_InductiveReasoning/Invariants/Bank/certora/conf/07_bank_invariant.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "BankFixed.sol:Bank" + ], + "verify": [ + "Bank:invariant.spec" + ], + "solc": "solc7.6", + "msg": "07 bank invariant", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true +} \ No newline at end of file diff --git a/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf b/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf new file mode 100644 index 00000000..229970ec --- /dev/null +++ b/08.Lesson_WorkingWithInvariants/InvariantsConcepts/Manager/certora/conf/08_managet_invariant.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "Manager.sol:Manager" + ], + "verify": [ + "Manager:ManagerFullSolution.spec" + ], + "solc": "solc8.6", + "msg": "08 managet invariant", + "optimistic_loop": false, + "multi_assert_check": false, + "send_only": true, + "disableLocalTypeChecking": true +} \ No newline at end of file