[Question] Does radius support under-constrained symbolic execution? about radius2 HOT 6 OPEN

Just read the paper and yes based on this description

An alternative to whole-program symbolic execution
is under-constrained symbolic execution [18, 42, 43],
which directly executes an arbitrary function within the
program, effectively skipping the costly path prefix from
main to this function. This approach reduces the number
and length of execution paths that must be explored. In
addition, it allows library and OS kernel code without a
main function to be checked easily and thoroughly

radius2 can begin symbolic execution from any address specified with call_state(addr) or with the -a option in the command line tool. However unlike other tools like angr where the default behaviour is to make uninitialized memory symbolic, anything not manually set to a symbolic value will generally be filled with 0x00 or 0xff so care needs to be taken to set up the state properly for whatever function you are executing

from radius2.

In contrast UC-KLEE automatically fills with unconstrained symbolic values. And it sounds like it does it in a cleverer way. radius2 has a blank_state(addr) which fills uninitialized mem with symbolic values but ima be honest it doesn't work well atm

from radius2.

Hey - Sorry for my delayed response and thank you taking the time to read the paper and provide a response!

I will have a go this week at getting a small PoC up and running. Interesting you mention the state setup - I think this was what I was missing when I have been experimenting but knowing I need to explicitly setup the state is a great pointer.

I'll report back once I have had a go at the PoC. I am fairly newbie at rust but I might be able to fix any issues as I go along and will PR if necessary!

from radius2.

going to keep this issue open as a reminder to fix blank_state and hopefully do something more intelligent for unconstrained pointer derefs

from radius2.

Hey @aemmitt-ns, That would be awesome! I did have a go at implementing something a while ago but honestly didn't get very far. The biggest hurdle I ran into was the state setup as well as reasoning about how to setup the state dynamically if we come across something that has no symbolic variable yet (as you say, mostly empty memory addresses). I did however find accessing the branch constraints really easy which is something that is a bit difficult in other frameworks some of the time.

from radius2.

@aemmitt-ns what do you think would be the first few things to do to get this added? I'm much more familiar with rust now and think I could have a crack at implementing it!

from radius2.