State Copy?

[bannsec]

It's not clear if it's possible to copy a given state. The examples I'm seeing are single traces through an application.

For instance, take state1 and return state1.copy that have the same information but are separate so that changes in one do not affect changes in the other.

[JonathanSalwan]

It's currently not really possible (takeSnapshot into the pintool module is a hack). But! we will add this feature for sure into the new API (dev-pb). For example, we could do something like this:

ctx = TritonContext()
# ...
bck = TritonContext(ctx) # do the state copy.

What do you think @pbrunet?

[bannsec]

Hmm... How much different is this dev-pb API going to be? Is it still using the core API now and adding to it or are those calls changing?

[JonathanSalwan]

All methods are kept the same. The main difference is that you need to instance a context.

[illera88]

Hey, are you still gonna pursue this?
Why is the takesnapshot a hack?

[JonathanSalwan]

Hey, are you still gonna pursue this?

Yep, I should...

Why is the takesnapshot a hack?

takesnapshot starts to record all modifications on memory and restoresnapshot undo all these modifications. This is a hack compared to what I've in mind with bck = TritonContext(ctx). In this case, we have to make copy of every object so that contexts are independent of each others.

[dvcrn]

Are there news on copying a context/state? For example I'd like to create a base context, load a binary and some memory, and then branch off for individual functions

[DarkaMaul]

I'm working on it but no ETA yet ;)

[dvcrn]

I've been wondering if there is a hacky solution that is usable from the python binding (snapshot isn't exposed)?

I wanted to ship my own, but getting all internal state such as all concretized memory to copy to a new state is not easy

[JonathanSalwan]

Note to myself: See #1012

[namreeb]

Just came here to say this would be useful to me as well when conducting recursive branch exploration to prove basic blocks and identify compounded opaque predicates.

[JonathanSalwan]

It's not an easy task, especially copying all shared_ptr (AbstractNode and SymbolicExpression). However, you can easily snapshot a state if you do not care about that states share pointers. Below an example of a snapshot function.

void SymbolicExplorator::snapshotContext(triton::Context* dst, triton::Context* src) {
  /* Synch concrete state */
  switch (src->getArchitecture()) {
    case triton::arch::ARCH_X86_64:
      *static_cast<triton::arch::x86::x8664Cpu*>(dst->getCpuInstance()) = *static_cast<triton::arch::x86::x8664Cpu*>(src->getCpuInstance());
      break;
    case triton::arch::ARCH_X86:
      *static_cast<triton::arch::x86::x86Cpu*>(dst->getCpuInstance()) = *static_cast<triton::arch::x86::x86Cpu*>(src->getCpuInstance());
      break;
    case triton::arch::ARCH_ARM32:
      *static_cast<triton::arch::arm::arm32::Arm32Cpu*>(dst->getCpuInstance()) = *static_cast<triton::arch::arm::arm32::Arm32Cpu*>(src->getCpuInstance());
      break;
    case triton::arch::ARCH_AARCH64:
      *static_cast<triton::arch::arm::aarch64::AArch64Cpu*>(dst->getCpuInstance()) = *static_cast<triton::arch::arm::aarch64::AArch64Cpu*>(src->getCpuInstance());
      break;
    default:
      throw triton::exceptions::Engines("SymbolicExplorator::snapshotContext(): Invalid architecture");
  }

  /* Synch symbolic register */
  dst->concretizeAllRegister();
  for (const auto& item : src->getSymbolicRegisters()) {
    dst->assignSymbolicExpressionToRegister(item.second, dst->getRegister(item.first));
  }

  /* Synch symbolic memory */
  dst->concretizeAllMemory();
  for (const auto& item : src->getSymbolicMemory()) {
    dst->assignSymbolicExpressionToMemory(item.second, triton::arch::MemoryAccess(item.first, triton::size::byte));
  }

  /* Synch path predicate */
  dst->clearPathConstraints();
  for (const auto& pc : src->getPathConstraints()) {
    dst->pushPathConstraint(pc);
  }
}

Then, you can do something like this:

/* backup the current context */
this->bck_ctx = new triton::Context(this->cur_ctx->getArchitecture());
this->snapshotContext(this->bck_ctx, this->cur_ctx);

/* do what you want */

/* restore the context */
this->snapshotContext(this->cur_ctx, this->bck_ctx);

The main point you have to keep in mind with this method is that if you modify an AST from a state (like in cur_ctx), it will affect all the others state (like bck_ctx).

[jmm14304]

I was wondering, is it possible the method Context::processing could change an AST from a state and affect the others?
I'm just trying to follow the registers state in a recursive branch exploration and processing instructions is pretty much the only thing I need. I'm not sure if there is something that could mess the snapshots (such as the mode AST_OPTIMIZATIONS) while processing instructions.

[JonathanSalwan]

Yes, AST will be shared between context (they are shared_ptr).

[MellowNight]

Does anyone know of any other symex libraries with a C++ API that allow you to fork the symbolic execution context along with AST state?

Exploring all code paths and forking context using Angr is very easy, however Angr does everything in python.

[bannsec]

S2E comes to mind: https://s2e.systems/docs/

However, note it will likely be a lot heavier as it does not summarize the environment, but rather integrates symbolic execution into a full virtual machine.

[ZehMatt]

I would also like to see this feature, I'll give it a shot and see how far I can get.

[ZehMatt]

I definitely did not anticipate to how convoluted everything is, the fact that the AST nodes store the Context makes this a bit harder than I initially thought, I will continue to pursue this but I might have to put a stop to it as the better course of action would be to first do some major cleaning up. I think it would be better to pass the Context to the individual functions as parameters for when its really needed, but I'll see what can be done.

Edit: Nope, not gonna do it.