From 045c19175b396d1edde3eed30246c982376e174c Mon Sep 17 00:00:00 2001 From: Thierry Marianne Date: Mon, 22 Nov 2021 16:05:24 +0100 Subject: [PATCH] Add erc20-based Smart Contract project example failing klee-based verification --- Cargo.lock | 22 ++--- Cargo.toml | 2 +- README.md | 14 ++-- examples/buggy-erc20.rs | 180 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 201 insertions(+), 17 deletions(-) create mode 100644 examples/buggy-erc20.rs diff --git a/Cargo.lock b/Cargo.lock index acd4135..0479307 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -37,9 +37,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.45" +version = "1.0.47" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ee10e43ae4a853c0a3591d4e2ada1719e553be18199d9da9d4a83f5927c2f5c7" +checksum = "38d9ff5d688f1c13395289f67db01d4826b46dd694e7580accdc3e8430f2d98e" [[package]] name = "async-attributes" @@ -856,15 +856,15 @@ checksum = "acd94fdbe1d4ff688b67b04eee2e17bd50995534a61539e45adfefb45e5e5503" [[package]] name = "httpdate" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6456b8a6c8f33fee7d958fcd1b60d55b11940a79e63ae87013e6d22e26034440" +checksum = "c4a1e36c821dbe04574f602848a19f742f4fb3c98d40449f11bcad18d6b17421" [[package]] name = "hyper" -version = "0.14.14" +version = "0.14.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b91bb1f221b6ea1f1e4371216b70f40748774c2fb5971b450c07773fb92d26b" +checksum = "436ec0091e4f20e655156a30a0df3770fe2900aa301e548e08446ec794b6953c" dependencies = [ "bytes", "futures-channel", @@ -971,9 +971,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.107" +version = "0.2.108" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fbe5e23404da5b4f555ef85ebed98fb4083e55a00c317800bc2a50ede9f3d219" +checksum = "8521a1b57e76b1ec69af7599e75e38e7b7fad6610f037db8c79b127201b5d119" [[package]] name = "lock_api" @@ -1413,7 +1413,7 @@ checksum = "71d301d4193d031abdd79ff7e3dd721168a9572ef3fe51a1517aba235bd8f86e" [[package]] name = "safepkt-backend" -version = "0.2.12" +version = "0.2.15" dependencies = [ "anyhow", "async-std", @@ -1478,9 +1478,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.70" +version = "1.0.71" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e277c495ac6cd1a01a58d0a0c574568b4d1ddf14f59965c6a58b8d96400b54f3" +checksum = "063bf466a64011ac24040a49009724ee60a57da1b437617ceb32e53ad61bfb19" dependencies = [ "itoa", "ryu", diff --git a/Cargo.toml b/Cargo.toml index 5b0ba2d..c220b3c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "safepkt-backend" -version = "0.2.12" +version = "0.2.15" authors = ["Caleb James Delisle ", "Thierry Marianne "] edition = "2018" license = "MIT OR Apache-2.0" diff --git a/README.md b/README.md index a146f63..dc8e9f3 100644 --- a/README.md +++ b/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). diff --git a/examples/buggy-erc20.rs b/examples/buggy-erc20.rs new file mode 100644 index 0000000..73ea9a2 --- /dev/null +++ b/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, + balances: storage::HashMap, + allowances: storage::HashMap<(AccountId, AccountId), Balance>, + } + + #[ink(event)] + struct Transfer { + #[ink(topic)] + from: Option, + #[ink(topic)] + to: Option, + #[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::() + .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); + } + } +}