Symbolic-length reads from symbolic sockets #1786

ekilmer · 2020-08-03T20:38:22Z

A read doesn't have to always return the number of bytes provided in the size argument. This is especially true for network sockets that may receive only partial bytes of data at a time.

This PR adds a feature to allow Manticore to fork when a receive is called on a SymbolicSocket and to more precisely emulate network data transmissions that may be sent in chunks less than what is requested.

Currently, we choose symbolic values from [1, remaining_bytes] to avoid too much state explosion.

Check coverage and add an example binary program

ekilmer · 2020-08-03T22:31:04Z

The uncovered paths seem acceptable to me, but I can spend more time writing tests if anyone thinks it's important enough to do so.

sschriner

LGTM! 🎉

manticore/platforms/linux.py

* master: Change the default to threading (#1779) Coveralls Take 2 (#1784)

ehennenfent · 2020-08-06T00:09:26Z

manticore/platforms/linux.py


    def __getstate__(self):
        state = super().__getstate__()
        state["inputs_recvd"] = self.inputs_recvd
        state["symb_name"] = self.symb_name
        state["recv_pos"] = self.recv_pos
        state["max_recv_symbolic"] = self.max_recv_symbolic
-        state["constraints"] = self._constraints


Why'd you remove the constraint set from the pickled state? It seems to me like you'd want it to persist.

Good question. I believe this should be taken care of during the SLinux __setstate__ here

manticore/manticore/platforms/linux.py

Lines 3278 to 3282 in 8989185

# Add constraints to symbolic sockets

for fd_entry in self.fd_table.entries():

symb_socket_entry = fd_entry.fdlike

if isinstance(symb_socket_entry, SymbolicSocket):

symb_socket_entry._constraints = self._constraints

We also initialize a SymbolicSocket with a reference to the ConstraintSet in SLinux here

manticore/manticore/platforms/linux.py

Line 3413 in 8989185

sock = SymbolicSocket(self.constraints, f"SymbSocket_{self.net_accepts}", net=True)

I'm open to suggestions for redesigning how/where the constraints are added. However, without removing this line, I think we are duplicating serialization of the constraint set, right?

The problem with keeping links to the constraintset is forking.

This all needs a refactor/simplification. But currently we fork using a context manager:

manticore/manticore/core/manticore.py

Lines 504 to 515 in 8989185

with state as new_state:

new_state.constrain(expression == new_value)

# and set the PC of the new state to the concrete pc-dest

# (or other register or memory address to concrete)

setstate(new_state, new_value)

# enqueue new_state, assign new state id

new_state_id = self._put_state(new_state)

# maintain a list of children for logging purpose

children.append(new_state_id)

Note that there the State is spawned into a child state using the width statement. Supposedly modifying anything of the child state would not affect the parent. (This is a lie except for constraints)

Note that the child constraints reference/references are updated when spawning a child from a parent:

manticore/manticore/core/state.py

Line 150 in 8989185

self.platform.constraints = new_state.constraints

If you keep a new reference to a constraintset it should be updated there.

@feliam Can you check out this commit aeb4a31 if it would work as a fix for this? Thank you!

Yes it looks like the new reference to the constraints are correctly propagated with that.

@ehennenfent Anything else you're wondering about this after the latest commits?

Nope, looks good to me! All this constraint set stuff is tricky...

Co-authored-by: sschriner <60201678+sschriner@users.noreply.github.com>

* master: Linux: Add stat method for FdLike (#1780) Use default handler for symbolic system call arguments (#1785)

* master: Add Manticore native State-specific hooks (#1777)

* master: Removing Thread unsafe global caching (#1788)

* master: Change types.FunctionType=<class 'function'> (#1803) Fix test regressions (#1804) State Introspection API (#1775) Fix EVM account existence checks for selfdestruct and call (#1801) Add partial implementation of sendto syscall (#1791) crytic-compile: use latest release (#1795) Update gas metering for calls to empty accounts (#1774) Fix BitVec with symbolic offset and fix TranslatorSmtlib.unique thread safety (#1792) Fix Coveralls for external PRs (#1794) Convert plugin list to dict (#1781) Symbolic-length reads from symbolic sockets (#1786) Removing Thread unsafe global caching (#1788) Add Manticore native State-specific hooks (#1777)

ekilmer added 2 commits August 3, 2020 16:16

Symbolic-length reads from symbolic sockets

cf5b9c0

Add native binary test

7b323df

ekilmer requested review from ehennenfent and feliam August 3, 2020 22:31

ekilmer marked this pull request as ready for review August 3, 2020 22:31

Merge branch 'master' into multi-symbolic-socket-accept

0dcfe06

sschriner approved these changes Aug 5, 2020

View reviewed changes

manticore/platforms/linux.py Show resolved Hide resolved

manticore/platforms/linux.py Show resolved Hide resolved

manticore/platforms/linux.py Outdated Show resolved Hide resolved

Merge branch 'master' into multi-symbolic-socket-accept

8989185

* master: Change the default to threading (#1779) Coveralls Take 2 (#1784)

ehennenfent reviewed Aug 6, 2020

View reviewed changes

ekilmer and others added 6 commits August 6, 2020 09:15

Add type hints to recvfrom

f509066

Co-authored-by: sschriner <60201678+sschriner@users.noreply.github.com>

Fixup type hints for recvfrom

8b25940

Update SymbolicSocket constraints pointers on fork

aeb4a31

Merge branch 'master' into multi-symbolic-socket-accept

5b3465f

* master: Linux: Add stat method for FdLike (#1780) Use default handler for symbolic system call arguments (#1785)

Merge branch 'master' into multi-symbolic-socket-accept

b33d8bb

* master: Add Manticore native State-specific hooks (#1777)

Merge branch 'master' into multi-symbolic-socket-accept

cc3d7a3

* master: Removing Thread unsafe global caching (#1788)

ekilmer requested a review from ehennenfent August 12, 2020 21:39

ehennenfent approved these changes Aug 13, 2020

View reviewed changes

ekilmer merged commit 85aa9ee into master Aug 14, 2020

ekilmer deleted the multi-symbolic-socket-accept branch August 14, 2020 16:15

ehennenfent added this to the Manticore 0.3.5 milestone Sep 3, 2020

ehennenfent mentioned this pull request Oct 6, 2020

Manticore 0.3.5 #1808

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Symbolic-length reads from symbolic sockets #1786

Symbolic-length reads from symbolic sockets #1786

Uh oh!

ekilmer commented Aug 3, 2020 •

edited

Loading

Uh oh!

ekilmer commented Aug 3, 2020

Uh oh!

sschriner left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ehennenfent Aug 6, 2020

Uh oh!

ekilmer Aug 6, 2020

Uh oh!

feliam Aug 6, 2020

Uh oh!

ekilmer Aug 11, 2020

Uh oh!

feliam Aug 11, 2020

Uh oh!

ekilmer Aug 12, 2020

Uh oh!

ehennenfent Aug 13, 2020

Uh oh!

Uh oh!

	# Add constraints to symbolic sockets
	for fd_entry in self.fd_table.entries():
	symb_socket_entry = fd_entry.fdlike
	if isinstance(symb_socket_entry, SymbolicSocket):
	symb_socket_entry._constraints = self._constraints

	with state as new_state:
	new_state.constrain(expression == new_value)

	# and set the PC of the new state to the concrete pc-dest
	# (or other register or memory address to concrete)
	setstate(new_state, new_value)

	# enqueue new_state, assign new state id
	new_state_id = self._put_state(new_state)

	# maintain a list of children for logging purpose
	children.append(new_state_id)

Symbolic-length reads from symbolic sockets #1786

Symbolic-length reads from symbolic sockets #1786

Uh oh!

Conversation

ekilmer commented Aug 3, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ekilmer commented Aug 3, 2020

Uh oh!

sschriner left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ehennenfent Aug 6, 2020

Choose a reason for hiding this comment

Uh oh!

ekilmer Aug 6, 2020

Choose a reason for hiding this comment

Uh oh!

feliam Aug 6, 2020

Choose a reason for hiding this comment

Uh oh!

ekilmer Aug 11, 2020

Choose a reason for hiding this comment

Uh oh!

feliam Aug 11, 2020

Choose a reason for hiding this comment

Uh oh!

ekilmer Aug 12, 2020

Choose a reason for hiding this comment

Uh oh!

ehennenfent Aug 13, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

ekilmer commented Aug 3, 2020 •

edited

Loading