diff --git a/README b/README index 7dbe364..71e8735 100644 --- a/README +++ b/README @@ -1,10 +1,14 @@ For usage on the LA Time's powerball simulator. Careful about clicking the page. +Blog post: https://blog.securityevaluators.com/hacking-the-javascript-lottery-80cc437e3b7f + Run the following snippet in your browser's console. _ = []; for(var i=0; i<5; ++i) { _.push(Math.random()) } ; console.log(_) -Paste at least 3 of those values into the dubs array in main(). +Paste at least 3 of those (5 for Chrome) values into the dubs array in main(). + +It will warn you if the model is too "loose" and has multiple solutions. Set the browser in main() to Chrome or Firefox. (Safari hasn't updated yet.) diff --git a/xs128p.py b/xs128p.py index 1216750..aededa9 100644 --- a/xs128p.py +++ b/xs128p.py @@ -2,20 +2,24 @@ import sys import math import struct import random -sys.path.append('/home/dgoddard/tools/z3/build') from z3 import * +MASK = 0xFFFFFFFFFFFFFFFF + # xor_shift_128_plus algorithm -def xs128p(state0, state1): - s1 = state0 & 0xFFFFFFFFFFFFFFFF - s0 = state1 & 0xFFFFFFFFFFFFFFFF - s1 ^= (s1 << 23) & 0xFFFFFFFFFFFFFFFF - s1 ^= (s1 >> 17) & 0xFFFFFFFFFFFFFFFF - s1 ^= s0 & 0xFFFFFFFFFFFFFFFF - s1 ^= (s0 >> 26) & 0xFFFFFFFFFFFFFFFF - state0 = state1 & 0xFFFFFFFFFFFFFFFF - state1 = s1 & 0xFFFFFFFFFFFFFFFF - generated = (state0 + state1) & 0xFFFFFFFFFFFFFFFF +def xs128p(state0, state1, browser): + s1 = state0 & MASK + s0 = state1 & MASK + s1 ^= (s1 << 23) & MASK + s1 ^= (s1 >> 17) & MASK + s1 ^= s0 & MASK + s1 ^= (s0 >> 26) & MASK + state0 = state1 & MASK + state1 = s1 & MASK + if browser == 'chrome': + generated = state0 & MASK + else: + generated = (state0 + state1) & MASK return state0, state1, generated @@ -29,11 +33,14 @@ def sym_xs128p(slvr, sym_state0, sym_state1, generated, browser): s1 ^= LShR(s0, 26) sym_state0 = sym_state1 sym_state1 = s1 - calc = (sym_state0 + sym_state1) + if browser == 'chrome': + calc = sym_state0 + else: + calc = (sym_state0 + sym_state1) condition = Bool('c%d' % int(generated * random.random())) if browser == 'chrome': - impl = Implies(condition, (calc & 0xFFFFFFFFFFFFF) == int(generated)) + impl = Implies(condition, LShR(calc, 12) == int(generated)) elif browser == 'firefox' or browser == 'safari': # Firefox and Safari save an extra bit impl = Implies(condition, (calc & 0x1FFFFFFFFFFFFF) == int(generated)) @@ -45,15 +52,20 @@ def reverse17(val): return val ^ (val >> 17) ^ (val >> 34) ^ (val >> 51) def reverse23(val): - return (val ^ (val << 23) ^ (val << 46)) & 0xFFFFFFFFFFFFFFFF + return (val ^ (val << 23) ^ (val << 46)) & MASK -def xs128p_backward(state0, state1): +def xs128p_backward(state0, state1, browser): prev_state1 = state0 prev_state0 = state1 ^ (state0 >> 26) prev_state0 = prev_state0 ^ state0 prev_state0 = reverse17(prev_state0) prev_state0 = reverse23(prev_state0) - generated = (prev_state0 + prev_state1) & 0xFFFFFFFFFFFFFFFF + # this is only called from an if chrome + # but let's be safe in case someone copies it out + if browser == 'chrome': + generated = prev_state0 + else: + generated = (prev_state0 + prev_state1) & MASK return prev_state0, prev_state1, generated # Print 'last seen' random number @@ -66,9 +78,9 @@ def xs128p_backward(state0, state1): # with an arrow. def power_ball(generated, browser): # for each random number (skip 4 of 5 that we generated) - for idx in xrange(len(generated[4:])): + for idx in range(len(generated[4:])): # powerball range is 1 to 69 - poss = range(1, 70) + poss = list(range(1, 70)) # base index 4 to skip gen = generated[4+idx:] # get 'last seen' number @@ -77,11 +89,11 @@ def power_ball(generated, browser): # make sure we have enough numbers if len(gen) < 6: break - print g0 + print(g0) # generate 5 winning numbers nums = [] - for jdx in xrange(5): + for jdx in range(5): index = int(gen[jdx] * len(poss)) val = poss[index] poss = poss[:index] + poss[index+1:] @@ -89,28 +101,28 @@ def power_ball(generated, browser): # print indicator if idx == 0 and browser == 'chrome': - print '--->', + print('--->', end='') elif idx == 2 and browser == 'firefox': - print '--->', + print('--->', end='') else: - print ' ', + print(' ', end='') # print winning numbers - print sorted(nums), + print(sorted(nums), end='') # generate / print power number or w/e it's called double = gen[5] val = int(math.floor(double * 26) + 1) - print val + print(val) # Firefox nextDouble(): # (rand_uint64 & ((1 << 53) - 1)) / (1 << 53) # Chrome nextDouble(): - # ((rand_uint64 & ((1 << 52) - 1)) | 0x3FF0000000000000) - 1.0 + # (state0 | 0x3FF0000000000000) - 1.0 # Safari weakRandom.get(): # (rand_uint64 & ((1 << 53) - 1) * (1.0 / (1 << 53))) def to_double(browser, out): if browser == 'chrome': - double_bits = (out & 0xFFFFFFFFFFFFF) | 0x3FF0000000000000 + double_bits = (out >> 12) | 0x3FF0000000000000 double = struct.unpack('d', struct.pack('> 12) elif browser == 'firefox': recovered = dubs[idx] * (0x1 << 53) elif browser == 'safari': @@ -157,7 +172,7 @@ def main(): # run symbolic xorshift128+ algorithm for three iterations # using the recovered numbers as constraints - for ea in xrange(3): + for ea in range(len(dubs)): sym_state0, sym_state1, ret_conditions = sym_xs128p(slvr, sym_state0, sym_state1, generated[ea], browser) conditions += ret_conditions @@ -166,21 +181,27 @@ def main(): m = slvr.model() state0 = m[ostate0].as_long() state1 = m[ostate1].as_long() + slvr.add(Or(ostate0 != m[ostate0], ostate1 != m[ostate1])) + if slvr.check(conditions) == sat: + print('WARNING: multiple solutions found! use more dubs!') + print('state', state0, state1) generated = [] # generate random numbers from recovered state - for idx in xrange(15): + for idx in range(15): if browser == 'chrome': - state0, state1, out = xs128p_backward(state0, state1) + state0, state1, out = xs128p_backward(state0, state1, browser) + out = state0 & MASK else: - state0, state1, out = xs128p(state0, state1) + state0, state1, out = xs128p(state0, state1, browser) double = to_double(browser, out) + print('gen', double) generated.append(double) # use generated numbers to predict powerball numbers power_ball(generated, browser) else: - print 'UNSAT' + print('UNSAT') main()