Question about state fork in s2e

[forwo...@gmail.com]

Hello, I am using s2e to test a CTF problem, and I found that s2e did not fork a new state as expected in a certain branch. As shown in the figure, I created a symbol variable v1 in pickTigerType (b) and then stored it on the heap in makeTiger(a). When the program is executed at the IF branch of pwnMe (d), there is no new state being forked. It is reasonable to say that the data taken from the heap should be the symbol variable v1 just passed in.

Specifically, when makeTiger copied data to the memory, I tested that their source operands EAX and EDX are both symbolic data (c), but when executed to the CMP instruction of pwnMe, I tested that EAX is not a symbolic value.

I want to know why this happens? Maybe you can provide me with an idea to solve it. 

Expecting your reply.

[Vitaly Chipounov]

Hi,

Could you please run s2e export_project and attach the resulting archive? It will be easier for us to see what's wrong.

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/93f71f38-4fde-43a6-a707-a9eaa7e6117bn%40googlegroups.com.

[forwo...@gmail.com]

Thank you for your reply. I have figured it out. Since I read the data in that heap memory, the value at that location has been concreted.

KLEE: WARNING: silently concretizing (reason: memory access from concrete code) to value 0x1

[Vitaly Chipounov]

Hi,

S2E does not concretize data in the heap. Symbolic data can be stored anywhere in RAM. Concretizations occur when writing symbolic data to devices (e.g., printing symbolic data on the screen) or to control registers of the CPU.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/4f139469-d6c7-43fe-9624-717369623717n%40googlegroups.com.

[forwo...@gmail.com]

I found this function in S2EExecutionStateMemory.cpp and it seems to write this value to object_offset + i after concrete. Did I understand it wrong?
```

void S2EExecutionStateMemory::transferRamInternal(const klee::ObjectStateConstPtr &os_, uint64_t object_offset,

uint8_t *buf, uint64_t size, bool write, bool exitOnSymbolicRead) {

klee::ObjectStateConstPtr os = os_;

if (os->isSharedConcrete()) {

assert(!exitOnSymbolicRead);

/* This can happen in case of access to device memory */

uint8_t *concreteStore = (uint8_t *) os->getAddress();

if (write) {

memcpy(concreteStore + object_offset, buf, size);

} else {

memcpy(buf, concreteStore + object_offset, size);

}

return;

}

if (write) {

auto wos = m_addressSpace->getWriteable(os);

bool oldAllConcrete = wos->isAllConcrete();

for (uint64_t i = 0; i < size; ++i) {

wos->write8(object_offset + i, buf[i]);

}

bool newAllConcrete = wos->isAllConcrete();

if ((oldAllConcrete != newAllConcrete) && (wos->notifyOnConcretenessChange())) {

m_notification->addressSpaceSymbolicStatusChange(wos, newAllConcrete);

}

} else {

ObjectStatePtr wos = nullptr;

for (uint64_t i = 0; i < size; ++i) {

if (!os->readConcrete8(object_offset + i, buf + i)) {

if (exitOnSymbolicRead) {

// m_startSymbexAtPC = getPc();

// XXX: what about regs_to_env ?

pabort("Check cpu_restore_state");

// fast_longjmp(env->jmp_env, 1);

}

if (!wos) {

os = wos = m_addressSpace->getWriteable(os);

}

buf[i] = m_concretizer->concretize(wos->read8(object_offset + i), "memory access from concrete code");

wos->write8(object_offset + i, buf[i]);

}

}

}

}

```

[Vitaly Chipounov]

Yes, this function concretizes any symbolic data it reads.

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/fc642c34-8091-465a-b773-833d2fbbe1e8n%40googlegroups.com.

[forwo...@gmail.com]

So as long as I read the memory, the location of that memory will be written permanently, and it is no longer a symbolic value?

I tried to remove write8() but found that some of the constraints I originally added could not be added successfully. I have seen the function transferRamInternalSymbolic, but it doesn't seem to be called.

So I want to ask if there is a good way to read the value of the memory without affecting the symbol data, just like register reading ( Call regs()->read ), if it is a symbol value, it returns false.

Thank you for answering my question.

[Vitaly Chipounov]

I don't understand what you are trying to solve. If the problem is the unwanted concretization you mentioned earlier, we first need to understand why it happens. Please attach the project file as instructed earlier, so that we can help with debugging.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/f63fe220-77c3-48c0-8a8d-9245210cb5dcn%40googlegroups.com.