We are given the following challenge description:
I had a bit of problem with these logic gates. They seemed to get quite big. Can you get them to a more manageable size for me? I even made my own symbols for some of them!
An initial look at the provided constraints.txt file gives us 15 very long equations looking like something like this (simplified, the original lines have 20kb+ of characters per line):
((a[1] + 94) !& (224 - a[2])) && ((! (a[1] + 94)) !& (! (224 - a[2]))) == 143
(! ((! ((((4 + 150) - a[0]) + ((140 + 204) - a[1])) - (a[2] + ((55 + 43) ^ (126 + 107))))) == 40
((41 + 113) - a[1])) !& (((98 + 49) + (98 ^ 50)) - a[2])) !& (((217 - 72) - a[0]) - ((235 + 175) - a[1])) == 83
Looking at the equations, we can see some variables like a[2]. To find out how many variables there are, I used the follwing command:
cat constraints.txt | grep -oe "a\[[^]]*" | sort | uniq | wc -l
Now, we know that we are looking for 15 variables. Additionally, as pointed out by the challenge description, there are custom operators.
There are two unary operators, which apply directly to the following expression:
! ~
And there are binary operators, which can only be put between two expressions:
+ - ^ || && !& !| ==
We can also see that a minus or plus are never used as unary expressions, which makes our life easier.
After trying and failing to write a custom parser for the equations, I remembered EBNF from the compiler design course. So, I created a definition that allows me to parse the equations into named entities:
value: NUMBER
variable : "a[" NUMBER "]"
unary_operator: "!" -> not
| "~" -> inverse
binary_operator: "+" -> plus
| "-" -> minus
| "^" -> xor
| "&&" -> and
| "||" -> or
| "!&" -> nand
| "!|" -> nor
| "==" -> equals
unary_expression: unary_operator expression
binary_expression: expression binary_operator expression
expression: "(" expression ")"
| binary_expression
| unary_expression
| value
| variable
%import common.NUMBER
%import common.WS
%ignore WS
In the end, everything is an expression, that is a tree structure representing the equation. To create a parser from this EBNF definition and use the parser to actually parse the equations, I have used the Lark python library.
Once parsed, the goal now is to convert the parsed expressions into Z3 expressions that can be added as constraints to a solver.
Lark allows us to create a custom Transformer, that will walk the tree for us and allows us to transform and construct new objects along the way. In our case, we create Z3 objects and combine them.
Initially, we handle the two most basic cases: value and variable. For value, we can just create a new BitVecVal. For variable, we reference pre-created variables that are our target BitVec instances. As we expect the result to be single-byte characters of a flag, we set BITVEC_SIZE to 8.
BITVEC_SIZE = 8
A = [BitVec(f"a_{i}", BITVEC_SIZE) for i in range(15)]
class ExprTransformer(Transformer):
def value(self, items):
return BitVecVal(int(items[0]), BITVEC_SIZE)
def variable(self, items):
return A[int(items[0])]
def unary_expression(self, items):
if items[0].data == "not":
# What to do in this case?
return ~items[1]
if items[0].data == "inverse":
return ~items[1]
raise ValueError(f"Invalid unary data label: {items[0].data}")
def binary_expression(self, items):
if items[1].data == "plus":
return items[0] + items[2]
if items[1].data == "minus":
return items[0] - items[2]
if items[1].data == "xor":
return items[0] ^ items[2]
if items[1].data == "and":
return items[0] & items[2]
if items[1].data == "or":
return items[0] | items[2]
if items[1].data == "nand":
return BvNand(items[0], items[2])
if items[1].data == "nor":
return BvNor(items[0], items[2])
if items[1].data == "equals":
return items[0] == items[2]
raise ValueError(f"Invalid binary data label: {items[1].data}")
def expression(self, items):
if len(items) != 1:
raise ValueError(f"More than one item: {items}")
return items[0]
For the unary expressions, there really is no good way to perform a NOT operation on an 8 byte value. So, as a placeholder, I just did the same as the bitwise invert ~ operator.
For the binary expression, the special cases are !& and !|, which I interpreted as NAND and NOR respectively. Luckily for us, Z3 has a BvNand and BvNor function ready for us to use!
Running Z3 now already gives us sat and a solution, however the provided solution is not human readable. So, this seemed pretty simple to do, and I just added the following code (s is the Z3 solver object):
for a in A:
s.add(And(31 < a, a < 128))
However, as soon as I did that, the Z3 check() returned unsat, so I thought there was no solution for a fully human readable flag with my assumption of what the NOT unary operator should be. So I looked into alternatives that returned only 0 or 1, as the boolean NOT operator would, but this also returned unsat.
I spent a lot of time debugging and troubleshooting until I created the following equations to sanity check my solve script:
a[0] == 50
a[1] == 50
a[2] == 50
a[3] == 50
a[4] == 50
a[5] == 50
a[6] == 50
a[7] == 50
a[8] == 50
a[9] == 50
a[10] == 50
a[11] == 50
a[12] == 50
a[13] == 50
a[14] == 50
With my script, this still returned unsat. How could this be? This is the most simple equations to think of for this challenge!
After some back and forth, unsat only appeared after I added the constraints for the flag to be human readable.
And indeed, changing the constraints to the following code fixed the script and gave me a flag:
for a in A:
s.add(And(31 < a, a < 127))
Using 127 instead of 128 allowed a solution, because 128 = 0b1000_0000, and the < operator compares this to the 8-bit BitVec. However, this comparison assumes signed numbers, so the constraints of 31 < a, a < 128 could never be true, regardless of the constraints given by the equations.
Putting everything we have learnt above together, we get the following solve script:
from lark import Lark, Transformer
from z3 import *
expr_parser = Lark(r"""
value: NUMBER
variable : "a[" NUMBER "]"
unary_operator: "!" -> not
| "~" -> inverse
binary_operator: "+" -> plus
| "-" -> minus
| "^" -> xor
| "&&" -> and
| "||" -> or
| "!&" -> nand
| "!|" -> nor
| "==" -> equals
unary_expression: unary_operator expression
binary_expression: expression binary_operator expression
expression: "(" expression ")"
| binary_expression
| unary_expression
| value
| variable
%import common.NUMBER
%import common.WS
%ignore WS
""", start='expression', parser='lalr')
BITVEC_SIZE = 8
A = [BitVec(f"a_{i}", BITVEC_SIZE) for i in range(15)]
class ExprTransformer(Transformer):
def value(self, items):
return BitVecVal(int(items[0]), BITVEC_SIZE)
def variable(self, items):
return A[int(items[0])]
def unary_expression(self, items):
if items[0].data == "not":
return ~items[1]
if items[0].data == "inverse":
return ~items[1]
raise ValueError(f"Invalid unary data label: {items[0].data}")
def binary_expression(self, items):
if items[1].data == "plus":
return items[0] + items[2]
if items[1].data == "minus":
return items[0] - items[2]
if items[1].data == "xor":
return items[0] ^ items[2]
if items[1].data == "and":
return items[0] & items[2]
if items[1].data == "or":
return items[0] | items[2]
if items[1].data == "nand":
return BvNand(items[0], items[2])
if items[1].data == "nor":
return BvNor(items[0], items[2])
if items[1].data == "equals":
return items[0] == items[2]
raise ValueError(f"Invalid binary data label: {items[1].data}")
def expression(self, items):
if len(items) != 1:
raise ValueError(f"More than one item: {items}")
return items[0]
s = Solver()
for a in A:
s.add(And(31 < a, a < 127))
with(open("constraints.txt", "r") as f):
for line in f:
line = line.strip()
if line == "":
continue
tree = expr_parser.parse(line)
constraint = ExprTransformer().transform(tree)
s.add(constraint)
print("Added constraint")
if s.check() == sat:
m = s.model()
print("Result:")
r = "POTTLACK{"
for i, a in enumerate(A):
r += chr(int(str(m[a])))
r += "}"
print(r)
else:
print("unsat")
Running the solve script will get us the flag!
POTTLACK{gOiNg_Up_uP_Up!}