Getting CRC polynomial and other CRC generator parameters using Z3

Sometimes CRC implementations are incompatible with each other: polynomial and other parameters can be different. Aside of polynomial, initial state can be either 0 or -1, final value can be inverted or not, endianness of the final value can be changed or not. Trying all these parameters by hand to match with someone's else implementation can be a real pain. Also, you can bruteforce 32-bit polynomial, but 64-bit polynomials is too much.

Deducing all these parameters is surprisingly simple using Z3, just get two values for 01 byte and 02, or any other bytes.

#!/usr/bin/env python

from z3 import *
import struct

# knobs:

# CRC-16 on https://www.lammertbies.nl/comm/info/crc-calculation.html
#width=16
#samples=["\x01", "\x02"]
#must_be=[0xC0C1, 0xC181]
#sample_len=1

# CRC-16 (Modbus) on https://www.lammertbies.nl/comm/info/crc-calculation.html
#width=16
#samples=["\x01", "\x02"]
#must_be=[0x807E, 0x813E]
#sample_len=1

# CRC-16-CCITT, Kermit on https://www.lammertbies.nl/comm/info/crc-calculation.html
#width=16
#samples=["\x01", "\x02"]
#must_be=[0x8911, 0x1223]
#sample_len=1

width=32
samples=["\x01", "\x02"]
must_be=[0xA505DF1B, 0x3C0C8EA1]
sample_len=1

# crc64_1.c:
#width=64
#samples=["\x01", "\x02"]
#must_be=[0x28d250b0f0900abe, 0x6c9fd98969f81a9d]
#sample_len=1

# crc64_2.c (redis):
#width=64
#samples=["\x01", "\x02"]
#must_be=[0x7ad870c830358979, 0xf5b0e190606b12f2]
#sample_len=1

# crc64_3.c:
#width=64
#samples=["\x01", "\x02"]
#must_be=[0xb32e4cbe03a75f6f, 0xf4843657a840a05b]
#sample_len=1

# http://www.unit-conversion.info/texttools/crc/
#width=32
#samples=["0","1"]
#must_be=[0xf4dbdf21, 0x83dcefb7]
#sample_len=1

# recipe-259177-1.py, CRC-64-ISO
#width=64
#samples=["\x01", "\x02"]
#must_be=[0x01B0000000000000, 0x0360000000000000]
#sample_len=1

# recipe-259177-1.py, CRC-64-ISO
#width=64
#samples=["\x01"]
#must_be=[0x01B0000000000000]
#sample_len=1

def swap_endianness_16(val):
    return struct.unpack("H", val))[0]

def swap_endianness_32(val):
    return struct.unpack("I", val))[0]

def swap_endianness_64(val):
    return struct.unpack("Q", val))[0]

def swap_endianness(width, val):
    if width==64:
        return swap_endianness_64(val)
    if width==32:
        return swap_endianness_32(val)
    if width==16:
        return swap_endianness_16(val)
    raise AssertionError

mask=2**width-1
poly=BitVec('poly', width)

# states[sample][0][8] is an initial state
# ...
# states[sample][i][0] is a state where it was already XORed with input bit
# states[sample][i][1] ... where the 1th shift/XOR operation has been done
# states[sample][i][8] ... where the 8th shift/XOR operation has been done
# ...
# states[sample][sample_len][8] - final state

states=[[[BitVec('state_%d_%d_%d' % (sample, i, bit), width) for bit in range(8+1)] for i in range(sample_len+1)] for sample in range(len(samples))]
s=Solver()

def invert(val):
    return ~val & mask

for sample in range(len(samples)):
    # initial state can be either zero or -1:
    s.add(Or(states[sample][0][8]==mask, states[sample][0][8]==0))

    # implement basic CRC algorithm
    for i in range(sample_len):
        s.add(states[sample][i+1][0] == states[sample][i][8] ^ ord(samples[sample][i]))

        for bit in range(8):
            # LShR() is logical shift, while >> is arithmetical shift, we use the first:
            s.add(states[sample][i+1][bit+1] == LShR(states[sample][i+1][bit],1) ^ If(states[sample][i+1][bit]&1==1, poly, 0))

    # final state must be equial to one of these:
    s.add(Or(
	states[sample][sample_len][8]==must_be[sample],
	states[sample][sample_len][8]==invert(must_be[sample]),
	states[sample][sample_len][8]==swap_endianness(width, must_be[sample]),
	states[sample][sample_len][8]==invert(swap_endianness(width, must_be[sample]))))

# get all possible results:
results=[]
while True:
    if s.check() == sat:
        m = s.model()
        # what final state was?
        if m[states[0][sample_len][8]].as_long()==must_be[0]:
            outparams="XORout=0"
        elif invert(m[states[0][sample_len][8]].as_long())==must_be[0]:
            outparams="XORout=-1"
        elif m[states[0][sample_len][8]].as_long()==swap_endianness(width, must_be[0]):
            outparams="XORout==0, ReflectOut=true"
        elif invert(m[states[0][sample_len][8]].as_long())==swap_endianness(width, must_be[0]):
            outparams="XORout=-1, ReflectOut=true"
        else:
            raise AssertionError

        print "poly=0x%x, init=0x%x, %s" % (m[poly].as_long(), m[states[0][0][8]].as_long(), outparams)

        results.append(m)
        block = []
        for d in m:
            c=d()
            block.append(c != m[d])
        s.add(Or(block))
    else:
        print "total results", len(results)
        break


This is for CRC-16:

poly=0xa001, init=0x0, XORout=0

Sometimes, we have no enough information, but still can get something. This is for CRC-16-CCITT

poly=0xb30f, init=0x0, XORout=-1
poly=0x7c07, init=0x0, XORout==0, ReflectOut=true
poly=0x8408, init=0x0, XORout==0, ReflectOut=true

One of these results is correct.

We can get something even if we have only one result for one input byte:

# recipe-259177-1.py, CRC-64-ISO
width=64
samples=["\x01"]
must_be=[0x01B0000000000000]
sample_len=1
poly=0x1fb12, init=0x0, XORout==0, ReflectOut=true
poly=0x1d24924924924924, init=0xffffffffffffffff, XORout=0
poly=0x86a9466cbb890d53, init=0x0, XORout=-1, ReflectOut=true
poly=0x580080, init=0x0, XORout==0, ReflectOut=true
poly=0xce9ce, init=0x0, XORout==0, ReflectOut=true
poly=0x53ffffffffffffff, init=0xffffffffffffffff, XORout=0
poly=0xd800000000000000, init=0x0, XORout=0
poly=0x38ad6, init=0x0, XORout==0, ReflectOut=true
poly=0x131e56e82623cae, init=0xffffffffffffffff, XORout==0, ReflectOut=true
poly=0x3fffffffffd3ffbf, init=0xffffffffffffffff, XORout==0, ReflectOut=true
poly=0x461861861861861, init=0xffffffffffffffff, XORout=0
total results 11

The files: https://github.com/dennis714/yurichev.com/tree/master/blog/CRC_cracker_Z3.

The shortcoming: longer samples slows down everything significantly. I had luck with samples up to 4 bytes, but no larger.

Further reading I've found interesting/helpful:


→ [list of blog posts, my twitter/facebook]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.