From f30112006a03858d54886a0c7ce711b2c57c8c89 Mon Sep 17 00:00:00 2001 From: victoryang00 Date: Thu, 2 May 2024 14:24:39 -0700 Subject: [PATCH] [feeat] td detection and updated usecase --- engine/src/lib.rs | 2 +- rust-toolchain | 1 + .../src/plugin/collections/td_detection.rs | 81 +++++++++++++----- symbolic_vm/src/types/values/values_impl.rs | 17 ++-- tests/verification.rs | 8 +- testsuites/td.mv | Bin 486 -> 449 bytes testsuites/td.mvir | 10 +-- testsuites/tod.mv | Bin 474 -> 284 bytes testsuites/tod.mvir | 12 --- 9 files changed, 78 insertions(+), 53 deletions(-) create mode 100644 rust-toolchain diff --git a/engine/src/lib.rs b/engine/src/lib.rs index 768ac53..dd41b97 100644 --- a/engine/src/lib.rs +++ b/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}, }; diff --git a/rust-toolchain b/rust-toolchain new file mode 100644 index 0000000..4934985 --- /dev/null +++ b/rust-toolchain @@ -0,0 +1 @@ +1.69.0 diff --git a/symbolic_vm/src/plugin/collections/td_detection.rs b/symbolic_vm/src/plugin/collections/td_detection.rs index 509a831..f343655 100644 --- a/symbolic_vm/src/plugin/collections/td_detection.rs +++ b/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, +} 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, ) -> PartialVMResult { - 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::()); + 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(()) } -} \ No newline at end of file +} diff --git a/symbolic_vm/src/types/values/values_impl.rs b/symbolic_vm/src/types/values/values_impl.rs index fb08898..54f01f7 100644 --- a/symbolic_vm/src/types/values/values_impl.rs +++ b/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, )?], )) } diff --git a/tests/verification.rs b/tests/verification.rs index 6330f29..0917137 100644 --- a/tests/verification.rs +++ b/tests/verification.rs @@ -345,7 +345,7 @@ 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); } @@ -353,7 +353,7 @@ fn td1() { 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); } @@ -361,6 +361,6 @@ fn td() { 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); } diff --git a/testsuites/td.mv b/testsuites/td.mv index 1c430a697de609a5c76433ec76aa0417706c0bc0..c43c1f8995933b49d4cfc077a9b0a98503be59f2 100644 GIT binary patch delta 286 zcmY+8J#NB45QXR8o81kP8w;#pR!SE|N$VmQIS@+SJx6yJMy!4z+J>QcQFr-mR;g+m~p(<~y$n9;b~ zY`bfF$R{3!fB-}R2s7|kNfB*~M4FH%)ETspJeeDUuPbSup~WbHJq7u!A_vOP{Hcnh n&SRh7l1J zWORba?9|^r#Fyv$_1*e%)4yHquq&zmfq(!+38):u64 { - let lastPayout:u64; let salt:u64; - let blockHash: vector; 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(&blockHash) && copy(count) < 8 ){ - index = Vector.pop_back(&mut blockHash); + while(!Vector.is_empty(&blockInfo) && copy(count) < 8 ){ + index = Vector.pop_back(&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); diff --git a/testsuites/tod.mv b/testsuites/tod.mv index 799c0f9367d5b8840d6f503eea0d3e8c6edd9043..870c4bdbc789e24fbae5f049b2c1875515128548 100644 GIT binary patch delta 128 zcmcb`Jcr3)q0DP;CI$uuHbw>xW)6NY5S_2x+uK`0l1hl6QAs68tZaknElkkvIM0ZOCKoO%(SKoKr;UHXzh&c3 za8E)AB2Mv`d2ikhynWyPOb7sC1VhGfb4QLy^$())E1ECd)z2jEh29VV5eXS10U`kq z2%M@x69XC*h&VzNw1Oa-onlZymfy863V(ZDWy{lSo?R99g@5Wy9(@(8>2f8d z`C2pc>?yse%4w$x=gVsH*HXx2qi}y?s9UsDM-pOi4QR3B1}B(M1QDD-!YxJkpIDpC zVeFKSK0+JHX&c_`%AOVdLj>qbBPOe)9Z+<+qI(&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(&with_cap, move(receiver), move(reward),h"", h""); - DiemAccount.restore_withdraw_capability(move(with_cap)); - return; }