SMT Solvers and S-Boxes

Until somewhat recently, I thought that there was no good way to model a S-box in SMT solvers like Z3 and Boolector, and it seems like a lot of others are also under that impression. Turns out there’s a pretty nice way to do it though - just model the S-box as an arbitrary function mapping the input sort to itself.

Here’s some examples using the AES S-box and Python APIs:

Z3

from z3 import *
SBOX = [99, 124, 119, 123, 242, 107, 111, 197, 48, 1, 103, 43, 254, 215, 171, 118, 202, 130, 201, 125, 250, 89, 71, 240, 173, 212, 162, 175, 156, 164, 114, 192, 183, 253, 147, 38, 54, 63, 247, 204, 52, 165, 229, 241, 113, 216, 49, 21, 4, 199, 35, 195, 24, 150, 5, 154, 7, 18, 128, 226, 235, 39, 178, 117, 9, 131, 44, 26, 27, 110, 90, 160, 82, 59, 214, 179, 41, 227, 47, 132, 83, 209, 0, 237, 32, 252, 177, 91, 106, 203, 190, 57, 74, 76, 88, 207, 208, 239, 170, 251, 67, 77, 51, 133, 69, 249, 2, 127, 80, 60, 159, 168, 81, 163, 64, 143, 146, 157, 56, 245, 188, 182, 218, 33, 16, 255, 243, 210, 205, 12, 19, 236, 95, 151, 68, 23, 196, 167, 126, 61, 100, 93, 25, 115, 96, 129, 79, 220, 34, 42, 144, 136, 70, 238, 184, 20, 222, 94, 11, 219, 224, 50, 58, 10, 73, 6, 36, 92, 194, 211, 172, 98, 145, 149, 228, 121, 231, 200, 55, 109, 141, 213, 78, 169, 108, 86, 244, 234, 101, 122, 174, 8, 186, 120, 37, 46, 28, 166, 180, 198, 232, 221, 116, 31, 75, 189, 139, 138, 112, 62, 181, 102, 72, 3, 246, 14, 97, 53, 87, 185, 134, 193, 29, 158, 225, 248, 152, 17, 105, 217, 142, 148, 155, 30, 135, 233, 206, 85, 40, 223, 140, 161, 137, 13, 191, 230, 66, 104, 65, 153, 45, 15, 176, 84, 187, 22]

s = Solver()

#               function     1 byte to      1 byte
subF = Function('subByte_f', BitVecSort(8), BitVecSort(8))

for i in range(256):
    s.add(subF(i) == SBOX[i])

encoded = b' EM\xb7\x83n\xed\xb7\xed\xd8\xaa\xa8\xbc\xb7\xf9\x8f\xb7\x9f\xa8\x9fP\xf9\x9fM\xef@'
decoded = [BitVec("decoded_%d" % i, 8) for i in range(len(encoded))]
for a, b in zip(encoded, decoded):
    s.add(a == subF(b))

s.check()
m = s.model()
print(bytes(m[x].as_long() for x in decoded))
# output: b'The AES S-box is nonlinear'

Boolector

import pyboolector
btor = pyboolector.Boolector()

btor.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, True)

SBOX = [99, 124, 119, 123, 242, 107, 111, 197, 48, 1, 103, 43, 254, 215, 171, 118, 202, 130, 201, 125, 250, 89, 71, 240, 173, 212, 162, 175, 156, 164, 114, 192, 183, 253, 147, 38, 54, 63, 247, 204, 52, 165, 229, 241, 113, 216, 49, 21, 4, 199, 35, 195, 24, 150, 5, 154, 7, 18, 128, 226, 235, 39, 178, 117, 9, 131, 44, 26, 27, 110, 90, 160, 82, 59, 214, 179, 41, 227, 47, 132, 83, 209, 0, 237, 32, 252, 177, 91, 106, 203, 190, 57, 74, 76, 88, 207, 208, 239, 170, 251, 67, 77, 51, 133, 69, 249, 2, 127, 80, 60, 159, 168, 81, 163, 64, 143, 146, 157, 56, 245, 188, 182, 218, 33, 16, 255, 243, 210, 205, 12, 19, 236, 95, 151, 68, 23, 196, 167, 126, 61, 100, 93, 25, 115, 96, 129, 79, 220, 34, 42, 144, 136, 70, 238, 184, 20, 222, 94, 11, 219, 224, 50, 58, 10, 73, 6, 36, 92, 194, 211, 172, 98, 145, 149, 228, 121, 231, 200, 55, 109, 141, 213, 78, 169, 108, 86, 244, 234, 101, 122, 174, 8, 186, 120, 37, 46, 28, 166, 180, 198, 232, 221, 116, 31, 75, 189, 139, 138, 112, 62, 181, 102, 72, 3, 246, 14, 97, 53, 87, 185, 134, 193, 29, 158, 225, 248, 152, 17, 105, 217, 142, 148, 155, 30, 135, 233, 206, 85, 40, 223, 140, 161, 137, 13, 191, 230, 66, 104, 65, 153, 45, 15, 176, 84, 187, 22]

# bvs is 1 byte bitvec sort we're using
bvs = btor.BitVecSort(8)
#               1 input (bvs) -> 1 output (bvs)
subF = btor.UF(btor.FunSort([bvs], bvs))
for i in range(256):
    btor.Assert(subF(i) == SBOX[i])

encoded = b'\xef\x9fC\xb7\xf9\x92\xb7E\xef\x8f\xb7\xef\xb7E\xf9\x85E\xb7\xefP\x85M\xaa@\xef\xf9\xfb\xb7CM\x85@MM'
decoded = [btor.Var(bvs, "decoded_%d" % i) for i in range(len(encoded))]
for a, b in zip(encoded, decoded):
    btor.Assert(a == subF(b))

btor.Sat()
print(bytes(int(x.assignment, 2) for x in decoded))
# output: b'and it has a high algebraic degree'