Symbolic-length reads from symbolic sockets

[ekilmer]

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]

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! 🎉

[ehennenfent]

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

[ekilmer]

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?

[feliam]

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.

[ekilmer]

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

[feliam]

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

[ekilmer]

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

[ehennenfent]

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