Optimise forking when there is only 1 solution #2527

Boyan-MILANOV · 2022-01-26T16:32:14Z

This PR improves the forking process when there is only one possible solution for the symbolic expression upon which we fork. In that case, we re-use the same State instead of copying the entire state to create a new one.

I don't think that Manticore has many tests for forks except this one:

manticore/tests/native/test_models.py

Lines 227 to 263 in 9321100

    
           def test_symbolic_fork(self): 
        
               # This binary is compiled using gcc (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0 
        
               # with flags: -g -static -fno-builtin 
        
               BIN_PATH = os.path.join( 
        
                   os.path.dirname(__file__), "binaries/str_model_tests", "sym_strlen_test" 
        
               ) 
        
               tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_sym_") 
        
               m = Manticore(BIN_PATH, stdin_size=10, workspace_url=str(tmp_dir.name)) 
        
               addr_of_strlen = 0x04404D0 
        
               @m.hook(addr_of_strlen) 
        
               def strlen_model(state): 
        
                   state.invoke_model(strlen_exact) 
        
               m.run() 
        
               m.finalize() 
        
               # Expected stdout outputs 
        
               expected = { 
        
                   "Length of string is: 0", 
        
                   "Length of string is: 1", 
        
                   "Length of string is: 2", 
        
                   "Length of string is: 3", 
        
                   "Length of string is: 4", 
        
                   "Length of string is: 5", 
        
               } 
        
               # Make a list of the generated output states 
        
               outputs = f"{str(m.workspace)}/test_*.stdout" 
        
               stdouts = set() 
        
               for out in glob(outputs): 
        
                   with open(out) as f: 
        
                       stdouts.add(f.read()) 
        
               # Assert that every expected stdout has a matching output 
        
               self.assertEqual(expected, stdouts)

I did test this PR in CHESS, but we should add a Manticore testcase for forking on a single solution since it hits a rarer and slightly different code path than regular forking.

Boyan-MILANOV · 2022-01-27T18:09:41Z

I added a test for forking on a unique solution.
For the sake of simplicity I re-used the strcpy symbolic fork test and added a similar one with additional constraints on the input so that we trigger the case where there is only a unique solution when forking on a symbolic input byte.

tests/native/test_models.py

Kokokokoka · 2022-01-31T19:02:10Z

this PR helps with latest python3.9.9 on gentoo, one can successfully use manticore on a contract

Boyan-MILANOV · 2022-01-31T19:09:28Z

@Kokokokoka: would you mind elaborating on your comment? Does this PR fix an opened issue, or just a bug that you was running into but didn't report?

Kokokokoka · 2022-01-31T20:00:41Z

I've seen similar bug reports #2518 seems to be the same, maybe there were others (which had mac os in them). I had this bug both on mac m1 and on my gentoo pc. Now it works

ehennenfent · 2022-02-02T19:29:44Z

The implementation looks good to me! Once we clarify my final question on the model tests I'm happy to approve & merge.

ehennenfent

Hmm, submitting via github.dev dropped all my comments, so let's try that again

tests/native/test_models.py

manticore/core/manticore.py

ehennenfent · 2022-02-02T19:28:59Z

tests/native/test_models.py

+        m.finalize()
+
+        # Expected stdout outputs
+        expected = {"Length of string is: 0", "Length of string is: 1"}


Would we expect to see different results for this test before the changes to our forking strategy? If we're forking on the length of the string, and constrain the second byte to be zero, then it makes sense that valid strings would be of length zero or one. That's two possibilities, which doesn't seem like it would test the new forking policy.

Would it make more sense to inspect the fork events using a plugin, or inspect the state ID numbers to confirm that we aren't creating new states when we concretize a symbol with a single possible value?

Yeah that's spot on. I hadn't noticed that the strlen_exact callback doesn't concretise the individual bytes but uses the solver API to check whether a byte is null, avoiding any forks. Definitely an oversight on my part.

I will replace that test with one that creates a Manticore instance and then raises a ConcretizeException on a constrained symbolic variable, then just checks that no additional states were created using will_fork_state_callback.

I have replaced the test with another one here: https://github.com/trailofbits/manticore/blob/003ce0ad620046e9602e95c1eb2c763ba66cedf9/tests/other/test_fork.py

The new test executes the simple hello_world program and artificially concretises a symbolic variable (constrained to one unique value) from a hook, and finally asserts that no additional states were created when forking. Let me know what you think!

ehennenfent

The new test looks great!

* master: (35 commits) Switch to stable Black (#2536) Fix typo in Manticore.linux constructor docstring (#2535) Revert CI changes made in #2526 Release Manticore 0.3.7 (#2526) Optimise forking when there is only 1 solution (#2527) Epoll Implementation (#2529) Split off ENDBR32/64 from CHESS branch (#2533) Update to crytic-compile 0.2.2 (#2530) Also ignore missing unicorn registers in the fallback emulator (#2531) x86 FXSAVE & FXRSTOR support (#2511) Fix `BitVecExtract` simplification for constant folding (#2524) Add pip-audit action workflow (#2513) Add EXPLICIT fork policy (#2514) Enforce crytic-compile==0.2.1 (#2512) Improve namedtuple definition (#2506) Add SMT simplifications for bitvec subtraction (#2504) Fix handling of the program base address in Linux (#2500) Bump Sphinx version to 4.3.0 (#2503) Solver Improvements (#2502) Improves `namedtuple` definition (#2501) ...

* master: Switch to stable Black (#2536) Fix typo in Manticore.linux constructor docstring (#2535) Revert CI changes made in #2526 Release Manticore 0.3.7 (#2526) Optimise forking when there is only 1 solution (#2527) Epoll Implementation (#2529) Split off ENDBR32/64 from CHESS branch (#2533) Update to crytic-compile 0.2.2 (#2530) Also ignore missing unicorn registers in the fallback emulator (#2531) x86 FXSAVE & FXRSTOR support (#2511) Fix `BitVecExtract` simplification for constant folding (#2524) Add pip-audit action workflow (#2513) Add EXPLICIT fork policy (#2514) Enforce crytic-compile==0.2.1 (#2512) Improve namedtuple definition (#2506) Add SMT simplifications for bitvec subtraction (#2504) Fix handling of the program base address in Linux (#2500)

Optimise forking when there is only 1 solution

892bf56

Boyan-MILANOV force-pushed the dev-fork-unique-solution branch 3 times, most recently from 5868f33 to 244844a Compare January 27, 2022 08:39

Update etherum test

f2548c9

Boyan-MILANOV force-pushed the dev-fork-unique-solution branch 5 times, most recently from bdad132 to 34850ea Compare January 27, 2022 16:59

Add test for forking on a unique solution

958bb80

Boyan-MILANOV force-pushed the dev-fork-unique-solution branch from 34850ea to 958bb80 Compare January 27, 2022 18:05

Boyan-MILANOV commented Jan 30, 2022

View reviewed changes

tests/native/test_models.py Outdated Show resolved Hide resolved

Boyan-MILANOV marked this pull request as ready for review January 30, 2022 11:51

ehennenfent reviewed Feb 2, 2022

View reviewed changes

Boyan-MILANOV added 3 commits February 16, 2022 11:16

Replace strlen test with dedicated fork test

6c2d7d5

Fix typo

5c43b99

Fix output filename in test

003ce0a

ehennenfent approved these changes Feb 16, 2022

View reviewed changes

ehennenfent merged commit 6212a7a into master Feb 17, 2022

ehennenfent deleted the dev-fork-unique-solution branch February 17, 2022 18:18

ehennenfent mentioned this pull request Feb 17, 2022

Release Manticore 0.3.7 #2526

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Optimise forking when there is only 1 solution #2527

Optimise forking when there is only 1 solution #2527

Boyan-MILANOV commented Jan 26, 2022 •

edited

Loading

Boyan-MILANOV commented Jan 27, 2022

Kokokokoka commented Jan 31, 2022

Boyan-MILANOV commented Jan 31, 2022

Kokokokoka commented Jan 31, 2022

ehennenfent commented Feb 2, 2022

ehennenfent left a comment

ehennenfent Feb 2, 2022

Boyan-MILANOV Feb 2, 2022

Boyan-MILANOV Feb 16, 2022

ehennenfent left a comment

	def test_symbolic_fork(self):
	# This binary is compiled using gcc (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0
	# with flags: -g -static -fno-builtin
	BIN_PATH = os.path.join(
	os.path.dirname(__file__), "binaries/str_model_tests", "sym_strlen_test"
	)
	tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_sym_")
	m = Manticore(BIN_PATH, stdin_size=10, workspace_url=str(tmp_dir.name))

	addr_of_strlen = 0x04404D0

	@m.hook(addr_of_strlen)
	def strlen_model(state):
	state.invoke_model(strlen_exact)

	m.run()
	m.finalize()

	# Expected stdout outputs
	expected = {
	"Length of string is: 0",
	"Length of string is: 1",
	"Length of string is: 2",
	"Length of string is: 3",
	"Length of string is: 4",
	"Length of string is: 5",
	}

	# Make a list of the generated output states
	outputs = f"{str(m.workspace)}/test_*.stdout"
	stdouts = set()
	for out in glob(outputs):
	with open(out) as f:
	stdouts.add(f.read())

	# Assert that every expected stdout has a matching output
	self.assertEqual(expected, stdouts)

Optimise forking when there is only 1 solution #2527

Optimise forking when there is only 1 solution #2527

Conversation

Boyan-MILANOV commented Jan 26, 2022 • edited Loading

Boyan-MILANOV commented Jan 27, 2022

Kokokokoka commented Jan 31, 2022

Boyan-MILANOV commented Jan 31, 2022

Kokokokoka commented Jan 31, 2022

ehennenfent commented Feb 2, 2022

ehennenfent left a comment

Choose a reason for hiding this comment

ehennenfent Feb 2, 2022

Choose a reason for hiding this comment

Boyan-MILANOV Feb 2, 2022

Choose a reason for hiding this comment

Boyan-MILANOV Feb 16, 2022

Choose a reason for hiding this comment

ehennenfent left a comment

Choose a reason for hiding this comment

Boyan-MILANOV commented Jan 26, 2022 •

edited

Loading