mjtb49 / latticg

Reverses the internal seed(s) of JavaRandom given information on its output in the form of a system of inequalities on various Random calls. Works by reducing the problem to finding certain vectors in a lattice, which is then solved through a branch and bound algorithm using a reduced version of the lattice.

JavaRandomReverser

Reverses the possible internal seed(s) of Java's java.util.Random class given information on its output in the form of a system of inequalities on various Random calls. The algorithm works by reducing the problem to finding certain vectors in a lattice, which is then solved through a branch and bound algorithm using a reduced version of the lattice.

Use the repository

All the packages are uploaded here through Jenkins CI: https://maven.latticg.com

You can browse it by hands here : https://nexus.seedfinding.com/#browse/browse:maven-latticg

The javadocs can be seen here : https://latticg.com

To use the libs you need first to declare the maven maven { url "https://maven.latticg.com/"} :

Gradle Groovy DSL :

implementation 'com.seedfinding:latticg:1.07@jar'

Apache Maven:

<dependency>
  <groupId>com.seedfinding</groupId>
  <artifactId>latticg</artifactId>
  <version>1.07</version>
</dependency>

Scala SBT

libraryDependencies += "com.seedfinding" % "latticg" % "1.07"

latticg's Issues

Class generator potentially far more optimizable

For cracking 3 float calls the code generated by the class generator from my testing takes about 2ms. For the randar exploit this was able to be optimized to under 10ns making the class generator generate code about a million times slower than what it could be for this use case where we have plenty of bits.

https://github.com/spawnmason/randar-explanation
https://github.com/spawnmason/randar-explanation#worked-example

hello can you explain to me how I can use the libary

hello can you explain to me how I can use the libary
and do you think that in minecraft it is possible to calculate the movement of a dragon egg

Have you tried to apply the Z3 prover before?

Your seedfinding explanations made me think of this. Z3 is a quite powerful theorem prover with Python bindings. It can find solutions for many systems and types of constraints, and can work with many datatypes, including floats and bit vectors! Here is an excellent talk about it: https://www.youtube.com/watch?v=56IIrBZy9Rc

Below I implemented a program which tries to find an initial_seed that, after ROUNDS iterations of an LCG, generates sequential values which each satisfy some constraints.

I haven't tested yet how well this works with other sets of constraints/larger numbers or rounds, but for this example it finds a solution even for 10000 LCG iterations within 2 seconds.

pip install z3

from z3 import *

java = (25214903917, 11, 48)#a,c,m

def ilcg(seed, params, repeat):
	"""Computes *repeat* forward passes given a starting seed and LCG parameters"""
	for r in range(repeat):
		seed = (params[0]*seed+params[1])%2**params[2]
		print(f"LCG iteration:{str(r+1).rjust(5)}\tvalue:{str(seed).rjust(16)}")
	return seed

def create_expression(solver, seed, params, maxrounds=1000, constraints=None):
	"""Creates expression with the initial *seed* BitVec variable, and adds constraints for the last passes, depending on the number of constraints"""
	ncs = []
	
	# reverse constraints order
	constraints = constraints[::-1]

	if constraints is None:
		constraints = []
		
	expr = seed

	for thisround in range(maxrounds):

		expr = (params[0]*expr+params[1])%2**params[2]

		if maxrounds-thisround-1 < len(constraints):
			nc = BitVec(f"nc_{maxrounds-thisround-1}", 48)
			ncs.append(nc)
			print("adding constraint", nc)
			
			c1 = nc==expr
			s.add(c1)
			#print(c1)
			
			c2 = constraints[maxrounds-thisround-1][0] <= nc
			print(c2)
			s.add(c2)
			
			c3 = nc <= constraints[maxrounds-thisround-1][1]
			s.add(c3)
			print(c3)
			
			

	return expr, ncs

# Number of rounds - constraints will be created matching the last rounds in reverse order
ROUNDS = 10

initial_seed = BitVec("initial_seed", 48)

# List constraints, structure: first_value <= value_at_iteration <= second_value
# last constraint is made to the last iteration, second last to the second last etc.
# In this case we want to find an initial_seed, that, after both 9 and 10 rounds has 0 <= value <= 1000
# here, it finds the 107048004364969 -> 0 -> 11 sequence
constraints = [(0, 1000), (0,1000)]#for some reason this doesn't work yet when using (0,2**48-1) somewhere, might have something to do with signed representations

s = Solver()

expr, ncs = create_expression(s, initial_seed, java, maxrounds=ROUNDS, constraints=constraints)

# Check whether the problem is satisfiable
ch = s.check()
if str(ch) == "unsat":
	print("unsatisfiable")
else:
	print("satisfiable")
	m = s.model()
	print("Model assignments", m)
	initial_seed = m[initial_seed].as_long()
	print("initial_seed:", initial_seed)

	for ci, constraint in enumerate(constraints):
		print("values vs constraints", m[ncs[ci]], constraint)
	
	check = ilcg(initial_seed, java, ROUNDS)
	print("forward pass check", check)

	if m[ncs[-1]].as_long() == check:
		print("forward pass check passed")
	else:
		print("final results do not agree")

Edit: found a video where someone applies it to a different generator: https://www.youtube.com/watch?v=-h_rj2-HP2E