Add erc20-based Smart Contract project example failing klee-based ver…

…ification

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "safepkt-backend"
-version = "0.2.12"
+version = "0.2.15"
 authors = ["Caleb James Delisle <[email protected]>", "Thierry Marianne <[email protected]>"]
 edition = "2018"
 license = "MIT OR Apache-2.0"

README.md

@@ -90,20 +90,25 @@ make test
 # Run program verification in CLI (command-line interface)
 
 ```shell
-# Plain Multisig Wallet  
-# See https://github.com/paritytech/ink/tree/v2.1.0/examples/multisig_plain
+# Plain Multisig Wallet
+# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/multisig_plain.rs
 ./target/release/safepkt-cli verify_program --source ./examples/multisig_plain.rs
 
 # erc721
-# See https://github.com/paritytech/ink/tree/v2.1.0/examples/erc721
+# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/erc721.rs
 ./target/release/safepkt-cli verify_program --source ./examples/erc721.rs
+
+# erc20-based smart contract showcasing a bug,
+# which can be highlighted by running SafePKT CLI verifier
+# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/buggy-erc20.rs
+./target/release/safepkt-cli verify_program --source ./examples/buggy-erc20.rs
 ```
 
 # Run program fuzzing in CLI (command-line interface)
 
 ```shell
 # erc721
-# See https://github.com/paritytech/ink/tree/v2.1.0/examples/erc721
+# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/erc721.rs
 ./target/release/safepkt-cli verify_program --source ./examples/erc721.rs --fuzz
 ```
 
@@ -115,7 +120,6 @@ make test
 ./target/release/safepkt-backend
 ```
 
-
 ## Run nginx as reverse-proxy
 
 Configuration templates for `nginx` are available from [provisioning/web-server/nginx](../../blob/main/provisioning/web-server/nginx).

examples/buggy-erc20.rs

@@ -0,0 +1,180 @@
+// Copyright 2018-2019 Parity Technologies (UK) Ltd.
+// Copyright 2021 CJDNS SASU
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+
+
+// ATTENTION ATTENTION ATTENTION ATTENTION ATTENTION ATTENTION ATTENTION
+//
+// This smart contract has a CRITICAL BUG, it is to be used for
+// demonstration purposes ONLY. Do not use this in production, is is INSECURE.
+//
+// ATTENTION ATTENTION ATTENTION ATTENTION ATTENTION ATTENTION ATTENTION
+
+
+
+#![cfg_attr(not(feature = "std"), no_std)]
+
+use ink_lang as ink;
+
+#[ink::contract(version = "0.1.0")]
+mod erc20 {
+    use ink_core::storage;
+
+    #[ink(storage)]
+    struct Erc20 {
+        total_supply: storage::Value<Balance>,
+        balances: storage::HashMap<AccountId, Balance>,
+        allowances: storage::HashMap<(AccountId, AccountId), Balance>,
+    }
+
+    #[ink(event)]
+    struct Transfer {
+        #[ink(topic)]
+        from: Option<AccountId>,
+        #[ink(topic)]
+        to: Option<AccountId>,
+        #[ink(topic)]
+        value: Balance,
+    }
+
+    #[ink(event)]
+    struct Approval {
+        #[ink(topic)]
+        owner: AccountId,
+        #[ink(topic)]
+        spender: AccountId,
+        #[ink(topic)]
+        value: Balance,
+    }
+
+    impl Erc20 {
+        #[ink(constructor)]
+        fn new(&mut self, initial_supply: Balance) {
+            let caller = self.env().caller();
+            self.total_supply.set(initial_supply);
+            self.balances.insert(caller, initial_supply);
+            self.env().emit_event(Transfer {
+                from: None,
+                to: Some(caller),
+                value: initial_supply,
+            });
+        }
+
+        #[ink(message)]
+        fn total_supply(&self) -> Balance {
+            *self.total_supply
+        }
+
+        #[ink(message)]
+        fn balance_of(&self, owner: AccountId) -> Balance {
+            self.balance_of_or_zero(&owner)
+        }
+
+        #[ink(message)]
+        fn allowance(&self, owner: AccountId, spender: AccountId) -> Balance {
+            self.allowance_of_or_zero(&owner, &spender)
+        }
+
+        #[ink(message)]
+        fn transfer(&mut self, to: AccountId, value: i32) -> bool {
+            let from = self.env().caller();
+            self.transfer_from_to(from, to, value)
+        }
+
+        #[ink(message)]
+        fn approve(&mut self, spender: AccountId, value: Balance) -> bool {
+            let owner = self.env().caller();
+            self.allowances.insert((owner, spender), value);
+            self.env().emit_event(Approval {
+                owner,
+                spender,
+                value,
+            });
+            true
+        }
+
+        #[ink(message)]
+        fn transfer_from(
+            &mut self,
+            from: AccountId,
+            to: AccountId,
+            value: Balance,
+        ) -> bool {
+            let caller = self.env().caller();
+            let allowance = self.allowance_of_or_zero(&from, &caller);
+            if allowance < value {
+                return false
+            }
+            self.allowances.insert((from, caller), allowance - value);
+            self.transfer_from_to(from, to, value as i32)
+        }
+
+        fn transfer_from_to(
+            &mut self,
+            from: AccountId,
+            to: AccountId,
+            value: i32,
+        ) -> bool {
+            let from_balance = self.balance_of_or_zero(&from) as i32;
+            if from_balance < value {
+                return false
+            }
+            self.balances.insert(from.clone(), (from_balance - value) as Balance);
+            let to_balance = self.balance_of_or_zero(&to) as i32;
+            self.balances.insert(to.clone(), (to_balance + value) as Balance);
+            self.env().emit_event(Transfer {
+                from: Some(from),
+                to: Some(to),
+                value: value as Balance,
+            });
+            true
+        }
+
+        fn balance_of_or_zero(&self, owner: &AccountId) -> Balance {
+            *self.balances.get(owner).unwrap_or(&0)
+        }
+
+        fn allowance_of_or_zero(
+            &self,
+            owner: &AccountId,
+            spender: &AccountId,
+        ) -> Balance {
+            *self.allowances.get(&(*owner, *spender)).unwrap_or(&0)
+        }
+    }
+
+    /// Unit tests
+    #[cfg(test)]
+    mod tests {
+        /// Imports all the definitions from the outer scope so we can use them here.
+        use super::*;
+        use ink_core::env;
+        use safepkt_assert::symbolic_num;
+
+        #[test]
+        fn transfer_test() {
+            let accounts = env::test::default_accounts::<env::DefaultEnvTypes>()
+                .expect("Cannot get accounts");
+
+            let mut erc20 = Erc20::new(100);
+            assert_eq!(erc20.balance_of(accounts.alice), 100);
+
+            let transfer_amount = symbolic_num!(-5, 5, 1);
+            assert!(erc20.transfer(accounts.bob, transfer_amount));
+            assert!(erc20.balance_of(accounts.alice) <= 100);
+            assert!(erc20.balance_of(accounts.bob) <= 100);
+        }
+    }
+}