Go Solve Some Puzzles …

Go Solve Some Puzzles …

It seems that every second research paper I review these days applies machine learning to some cybersecurity problem, and it feels like sometimes that we are losing our ability to solve problems with a solid mathematical base, and to use a formal proof that our answer is right or not. Our brain needs exercise, and to throw some data at a machine, and get it to make sense of it, is only exercising your fingers. We need to make sure our brain builds new connections, and find new routes, and we need to solve things.

A bit of Sudoku

I recently was on a flight, and the person sitting next had a Sudoku puzzle book. And so I pull up my Z3 Python script, and ran a few tests, and my little puzzle solver seemed to work okay. “Can I give it a try?”, I said. “Yes, of course”. The person then nodded off, and I set out to test out a few of the puzzles. With Python, it was so easy, and it was a matter of carefully typing in the values, and then running the script. In an instance the solution was there. And so for those puzzle, we get the answer of [here]:

When the person woke up, they picked up their puzzle book, and I could see they looked puzzle in having a full page of solutions. Unfortunately they didn’t ask me what had happened, so there are probably still wondering how it happened. The key to the solve is the great little Z3 library from Microsoft, and it just loves solving puzzles and proving things.

A power of 2?

A great example is when we want to prove that a value is to the power of 2, such as with 16 and 64. One way is to use the logical operation of:

And(x != 0, x & (x — 1) == 0)

which is, for a power of 2, if x is not equal to zero, and then we bitwise x with x-1, we should get zero. How do we prove that this is always the case?

In the following code we prove this, and compare it against creating all the power for 32 bit values and seeing if our value is in there [here]:

from z3 import *

eq = 'And(x != 0, x & (x - 1) == 0)'

if (len(sys.argv)>1):
	eq=str(sys.argv[1])

x      = BitVec('x', 32)
powers = [ 2**i for i in range(32) ]
fast   = eval(eq)
slow   = Or([ x == p for p in powers ])
print "Is it proven?",prove(fast == slow)
print powers

The following a sample run [here]:

Equ01:  And(x != 0, x & (x - 1) == 0)
Equ02:  Or([ x == p for p in powers ])

Is it proven? proved
None
[1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648L]

Writing your name in crypto

It can be used in many crypto applications, too. And so here is a puzzle for you to solve. How did I use Z3 to generate my own name in a random number generator [here]:

Conclusions

The skills of the future are in solving puzzles, so get learn how to solve things. For any PhD student out there in computer science … along with machine learning, go learn some maths, too. Some things are proven with a pen and paper, other things need the power of a library such as Z3. It is fun to solve things … that is what makes us human. As we have evolved as a human race, we have been faced with puzzles, and we have solved them, and moved on. As we see the rise of the machine, we have got to watch that we do not rely on our every thought on the power of the machine.

If you want to exercise your brain, go do some of my cipher challenges: