[feeat] td detection and updated usecase

engine/src/lib.rs

@@ -14,7 +14,7 @@ use z3::{
 };
 
 use symbolic_vm::{
-  plugin::{IntegerArithmeticPlugin, Plugin, PluginManager, VerificationPlugin},
+  plugin::{IntegerArithmeticPlugin, TDDetectionPlugin, TODDetectionPlugin, Plugin, PluginManager, VerificationPlugin},
   runtime::vm::SymbolicVM,
   types::values::{SymValue, VMSymValueCast, SymU64, SymBool},
 };

rust-toolchain

@@ -0,0 +1 @@
+1.69.0

symbolic_vm/src/plugin/collections/td_detection.rs

@@ -1,44 +1,85 @@
-use move_vm_types::loaded_data::runtime_types::Type;
-use vm::{errors::{PartialVMResult, VMResult}, file_format::Bytecode};
 use crate::{
-    plugin::{Plugin, PluginContext, collections::verification::specification::*},
+    plugin::{collections::verification::specification::*, Plugin, PluginContext},
     runtime::{
         context::TypeContext,
-        loader::{Loader, Function}}, types::values::{SymValue}, types::values::SymIntegerValue,
+        loader::{Function, Loader},
+    },
+    types::values::SymIntegerValue,
+    types::values::SymValue,
 };
 use move_core_types::identifier::Identifier;
-use crate::types::memory::SymMemory;
-
-pub struct TDDetectionPlugin();
+use move_vm_types::loaded_data::runtime_types::Type;
+use vm::{
+    errors::{PartialVMResult, VMResult},
+};
+use z3::{
+    ast::{exists_const, forall_const, Ast, Bool, Datatype, Dynamic},
+    Context, Goal, SatResult, Solver, Tactic,
+};
+pub struct TDDetectionPlugin {
+    now_microseconds_used: bool,
+    timestamp_symbol: Option<u64>,
+}
 
 impl TDDetectionPlugin {
     pub fn new() -> Self {
-        Self {}
+        Self {
+            now_microseconds_used: false,
+            timestamp_symbol: None,
+        }
     }
 }
 
 impl Plugin for TDDetectionPlugin {
-    /** Get the initial change set and insert into SymMemory one by one */
     fn on_before_call<'ctx>(
         &self,
         plugin_ctx: &mut dyn PluginContext<'ctx>,
         func: &Function,
         _ty_args: Vec<Type>,
     ) -> PartialVMResult<bool> {
-        println!("[TD]: Change Set into SymMemory {:?}", func.name());
-        let args = plugin_ctx.data_store();
-        let z3_ctx = plugin_ctx.z3_ctx();
-        let ty_ctx = plugin_ctx.ty_ctx();
-
-        let memory = plugin_ctx.memory_mut();
-        let solver = plugin_ctx.solver();
-        Ok(true)
+        if func.name() == "now_microseconds" {
+            self.now_microseconds_used = true;
+            let ty_ctx = plugin_ctx.ty_ctx();
+            let z3_ctx = plugin_ctx.z3_ctx();
+            self.timestamp_symbol = Some(rand::random::<u64>());
+            let model = plugin_ctx.solver();
+            let mem_key_sort = ty_ctx.memory_key_sort();
+            let timestamp_val = Datatype::fresh_const(z3_ctx, "timestamp", &mem_key_sort.sort);
+            plugin_ctx
+                .memory_mut()
+                .write_resource(z3_ctx, ty_ctx, timestamp_val);
+            Ok(true)
+        }
+        Ok(false)
     }
+
     fn on_after_execute<'ctx>(
         &self,
-        _plugin_context: &mut dyn PluginContext<'ctx>,
-        _return_values: &[SymValue<'ctx>],
+        plugin_ctx: &mut dyn PluginContext<'ctx>,
+        return_values: &[SymValue<'ctx>],
     ) -> VMResult<()> {
+        if self.now_microseconds_used {
+            if let Some(timestamp_symbol) = self.timestamp_symbol {
+                let solver = plugin_ctx.solver();
+                let model = solver.get_model().unwrap();
+                let ty_ctx = plugin_ctx.ty_ctx();
+                let z3_ctx = plugin_ctx.z3_ctx();
+                let timestamp_val =
+                    plugin_ctx
+                        .memory_mut()
+                        .load_resource(z3_ctx, ty_ctx, &model, "timestamp").unwrap();
+                let bv_r = SymIntegerValue::U64();
+                let manipulation_cond = timestamp_val.gt(bv_r);
+                solver.assert(&manipulation_cond.not());
+
+                match solver.check() {
+                    SatResult::Sat => {
+                        println!("Block Timestamp Manipulation detected!");
+                    }
+                    _ => {}
+                }
+            }
+        }
         Ok(())
     }
-}
+}

symbolic_vm/src/types/values/values_impl.rs

@@ -2293,14 +2293,13 @@ impl<'ctx> SymVectorRef<'ctx> {
     // if idx >= c.len() {
     //   return Ok(NativeResult::err(cost, INDEX_OUT_OF_BOUNDS));
     // }
-    let (res, vector) = match c {
-      VecU8(r)
-      | VecU64(r)
-      | VecU128(r)
-      | VecBool(r)
-      | VecAddress(r)
-      | Vec(r) => (r.borrow_mut().pop(context.get_ty_ctx()), r.borrow()),
-
+    let (res, element_type) = match c {
+      VecU8(r) | VecU64(r) | VecU128(r) | VecBool(r) | VecAddress(r) | Vec(r) => {
+        let mut cloned_r = r.clone();
+        let element_type = cloned_r.borrow().element_type.clone();
+        let res = cloned_r.borrow_mut().pop(context.get_ty_ctx());
+        (res,element_type)
+      }
       Locals(_) | Struct(_) => unreachable!(),
     };
 
@@ -2309,7 +2308,7 @@ impl<'ctx> SymVectorRef<'ctx> {
       vec![SymValue::from_runtime_ast_with_type(
         context.get_z3_ctx(),
         context.get_ty_ctx(),
-        res, &vector.element_type,
+        res, &element_type,
       )?],
     ))
   }

tests/verification.rs

@@ -345,22 +345,22 @@ fn alias_foo_opaque() {
 fn td1() {
   let z3_cfg = Config::new();
   let z3_ctx = Context::new(&z3_cfg);
-  let mut td_plugin = TDDetectionPlugin::new();
+  let td_plugin = TDDetectionPlugin::new();
   exec("testsuites/td1.mv", "theRun", &z3_ctx, td_plugin);
 }
 
 #[test]
 fn td() {
   let z3_cfg = Config::new();
   let z3_ctx = Context::new(&z3_cfg);
-  let mut td_plugin = TDDetectionPlugin::new();
+  let td_plugin = TDDetectionPlugin::new();
   exec("testsuites/td.mv", "theRun", &z3_ctx, td_plugin);
 }
 
 #[test]
 fn tod() {
   let z3_cfg = Config::new();
   let z3_ctx = Context::new(&z3_cfg);
-  let mut tod_plugin = TODDetectionPlugin::new();
-  exec("testsuites/td.mv", "theRun", &z3_ctx, tod_plugin);
+  let tod_plugin = TODDetectionPlugin::new();
+  exec("testsuites/tod.mv", "TOD_Attack", &z3_ctx, tod_plugin);
 }

testsuites/td.mvir

@@ -10,31 +10,27 @@ module Test{
     }
 
     public theRun(blockInfo: vector<u8>):u64 {
-        let lastPayout:u64;
         let salt:u64;
-        let blockHash: vector<u8>;
         let count:u64;
         let h:u64;
         let index:u8;
         let y:u64;
         let seed:u64;
 
-        lastPayout = 0;
         salt = DiemTimestamp.now_microseconds();
-        blockHash = Hash.sha2_256(copy(blockInfo));
         count = 0;
         h = 0;
         y = 0;
 
-        while(!Vector.is_empty<u8>(&blockHash) && copy(count) < 8 ){
-            index = Vector.pop_back<u8>(&mut blockHash);
+        while(!Vector.is_empty<u8>(&blockInfo) && copy(count) < 8 ){
+            index = Vector.pop_back<u8>(&mut blockInfo);
             h = move(h) + (copy(count) << move(index) );
             count = move(count) + 1;
         };
         y = copy(salt) * DiemBlock.get_current_block_height() / (copy(salt) % 5);
         seed = DiemBlock.get_current_block_height() / 3;
         seed = move(seed) + (move(salt) * 300);
-        seed = move(seed) + move(lastPayout) + move(y);
+        seed = move(seed) +  move(y);
         // Let h be the block hash of the number of seed last block, Do some hash here
         h = (move(seed) % 100) +1;
         return move(h);

testsuites/tod.mvir

@@ -9,22 +9,10 @@ module Test{
 
 
     public TOD_Transaction1(account: signer, receiver: address, reward: u64) {
-        let with_cap: DiemAccount.WithdrawCapability;
-
-        with_cap = DiemAccount.extract_withdraw_capability(&account);
-        DiemAccount.pay_from<XUS.XUS>(&with_cap, move(receiver), move(reward),h"",  h"");
-        DiemAccount.restore_withdraw_capability(move(with_cap));
-
         return;
     }
 
     public TOD_Transaction2(account: signer, receiver: address, reward: u64) {
-        let with_cap: DiemAccount.WithdrawCapability;
-
-        with_cap = DiemAccount.extract_withdraw_capability(&account);
-        DiemAccount.pay_from<XUS.XUS>(&with_cap, move(receiver), move(reward),h"",  h"");
-        DiemAccount.restore_withdraw_capability(move(with_cap));
-
         return;
     }