Blogs

Software is a Scam

Description: Why use software when hardware gets the job done just fine?

Solved by: Vitruvian

Provided with an image of a circuit, which looked less like a CTF challenge and more like my electronics homework.

auth.png

The final aim of the circuit is to give a HIGH output from the final comparator.

Components used:

How do you derive an equation ?

Our main objective is to get this LED to glow, therefore, we need all comparator outputs to be high.

Let us consider the highlighted circuit:

highlighted

We want the value of Y to be 0x87 for the comparator to give a HIGH output.

The highlighted part is what we visually traced back to get the value of Y.

If we follow the yellow and green lines(which lead to c1 and c3), we see that they are inputs for the AND gate. So the output of the AND will be c1 & c3.

w = c1 & c3

Similarly, for x

x = c2 ^ c4

Tracing forward, we can see, w and x are inputs for the NOR gate.

Therefore,

~(w || x) = Y = 0x87

Final equation will be:

~((c1 & c3) || (c2 ^ c4)) = 0x87

Lets do this section by section.

As Section 1 and Section 2 were independent, we solved their set of equations already. The final script combines the solution for all 3 section, so we directly get the flag in the end.

Section 1

Writing all equations related to this section:

~(((c1*c4) + c1) ^ (c2)) = 0x5c
~((c1 & c3) || (c2 ^ c4)) = 0x87
(c3 ^ c4) = 0x0a 
(c2 - c1) = 0xe7
(c3 - c1) > 0xf4

Solving this set of equations using z3, gave us L3AK.

All the scripts have been combined into a final script which is given at the end of the writeup

Section 2

(c5 - c20) = 0xfe
(c10 & c20) ^ (~c5) = 0xd9
(c5 & c10) & (~(c15 ^ c20)) = 0x59
(c15 + c10) < 0xd6 
(c15 + c10) > 0xbd

Solving this set of equations gives us the position of _ and {, }

Using this we got the L3AK{} wrapper and the positions of the underscores.

Stuff known till now:

c1 = 0x4c  # L
c2 = 0x33  # 3
c3 = 0x41  # A
c4 = 0x4b  # K
c5 = 0x7b  # {
c10 = 0x5f # _
c15 = 0x5f # _
c20 = 0x7d # }

Section 3

(c13 - c8) = 0x2e 
((c17 - c18) & c9) = 0x33
c18 + (c9 ^ c19) = 0xab
(c17 - c8) = 0xef
(c6 ^ c8) = 0x2c
(c13 + c6) = 0xb5 
~((c6 << 2) ^ c11 ^ c13) + c19 = 0x0d
(((~(c9 & c16))&c17)^c12) ^ c14 = 0x51
t = ~((c6 << 2) ^ c11 ^ c13)
((~(c14 & t)) ^ t) || (c18) = 0x37
c7 = ~(((c9 & c13) ^ (~(c9 & c16)))^c16^c12)
c7 - (~(c12 & (c6 << 2))) = 0x74

XNOR issue

We verified the equations multiple times and the solve script but we were getting non-ASCII each time and came to the conclusion that it must be an issue with how the logic blocks are working.

The comparator by default was signed (2’s complement), even after that, everything still added up.

Comparator

A magnitude comparator is a combinational circuit that compares two numbers, A and B, and determines their relative magnitudes. The outcome of the comparison is specified by three binary variables that indicate whether A > B, A = B or A < B

Signed VS Unsigned Comparison

Lets take

A = 1000 # 8(unsigned)/-8(signed)
B = 0111 # 7
Signed Unsigned
A signed comparator interprets the most significant bit (MSB) as a positive/negative sign (via two’s complement), meaning a negative number with an MSB of 1 is correctly evaluated as less than a positive number with an MSB of 0. An unsigned comparator treats that same MSB as a high positional magnitude value, viewing the bit pattern as a large positive integer.
Here, -8 < 7 , A < B Here, 8 > 7, A > B

2’s Complement Comparison

Lets take the following equation as an example

c5 - c20 = 0xfe

We computed c5 = 0x7b and c20 = 0x7d.

So,

0x7b - 0x7d = -0x2

Now doing 2’s complement

-0x2 & 0xff = 0xfe

We get 0xfe which is the required output.

In signed comparison, -0x2 < 0xfe and the comparator will result in LOW output.

We didn’t look through the gates because we assumed the standard outputs.

After going through gate outputs and conversation with the author JAGIC, they told that we had “misinterpreted a certain logic gate”.

After testing all the gates, we found the 3 input XNOR (~(A ^ B ^ C)) did not match the standard truth table.

Standard truth table:

Logism:

Truth table for 3 input XNOR gate in Logism:

a b c output
0 0 0 1
0 0 1 0
0 1 0 0
0 1 1 1
1 0 0 0
1 0 1 1
1 1 0 1
1 1 1 1

Why this behaviour?

So, we decided to look through the source code of Logism and we found the exact issue on their github page.

Exact issue on Github: Issue 36

GateFunctions.java -> In this file of the source code, the computeOddParity function cascades XNOR outputs and relies on any odd number of 1s or “not exactly one” logic in Logism config. Shown here:

In XnorGate.java there is computeOutput function which defines two the two XNOR implementation types :

@Override
    protected Value computeOutput(Value[] inputs, int numInputs, InstanceState state) {
        Object behavior = state.getAttributeValue(GateAttributes.ATTR_XOR);
        if (behavior == GateAttributes.XOR_ODD) {
            return GateFunctions.computeOddParity(inputs, numInputs).not();
        } else {
            return GateFunctions.computeExactlyOne(inputs, numInputs).not();
        }
    }

On selecting When an odd number are on as Multiple-Input Behaviour we got the behaviour that we were looking for.

Here’s a video depicting the behaviour of the XNOR gate: XNOR in Logism

But by default, Logism selects When one input is on , so in our final script, we had to take that into consideration.

We created the following function in our script to mimic the default behaviour of Logism:

def XNOR3(a, b, c):
    r = BitVecVal(0, 8)
    for i in range(8):
        ai = Extract(i, i, a)
        bi = Extract(i, i, b)
        ci = Extract(i, i, c)

        bit = If(
            Or(
                And(ai == BitVecVal(1,1), bi == BitVecVal(0,1), ci == BitVecVal(0,1)),
                And(ai == BitVecVal(0,1), bi == BitVecVal(1,1), ci == BitVecVal(0,1)),
                And(ai == BitVecVal(0,1), bi == BitVecVal(0,1), ci == BitVecVal(1,1))
            ),
            BitVecVal(0,1),
            BitVecVal(1,1)
        )

        r = r | (ZeroExt(7, bit) << i)
    return r

This is the final script, that was made after taking updated values of output of 3 input XNOR into consideration.

from z3 import *

NAND = lambda a, b: ~(a & b)
NOR = lambda a, b: ~(a | b)
XNOR2 = lambda a, b: ~(a ^ b)
SHL2 = lambda x: (x << 2) & BitVecVal(0xff, 8)

def XNOR3(a, b, c):
    r = BitVecVal(0, 8)
    for i in range(8):
        ai = Extract(i, i, a)
        bi = Extract(i, i, b)
        ci = Extract(i, i, c)

        bit = If(
            Or(
                And(ai == BitVecVal(1,1), bi == BitVecVal(0,1), ci == BitVecVal(0,1)),
                And(ai == BitVecVal(0,1), bi == BitVecVal(1,1), ci == BitVecVal(0,1)),
                And(ai == BitVecVal(0,1), bi == BitVecVal(0,1), ci == BitVecVal(1,1))
            ),
            BitVecVal(0,1),
            BitVecVal(1,1)
        )

        r = r | (ZeroExt(7, bit) << i)
    return r

c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c20 = [
    BitVec(f"c{i}",8)
    for i in [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]
]

v=[c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c20]
s=Solver()

t1 = XNOR3(
    (c9 & c13) ^ NAND(c9,c16),
    c16,
    c12
)

t2 = XNOR3(
    SHL2(c6),
    c11,
    c13
)

#section1
s.add(XNOR2(((c1*c4) + c1) , c2)==0x5c)
s.add(NOR((c1 & c3), (c2 ^ c4))==0x87)
s.add((c3 ^ c4)==0x0a)
s.add((c2 - c1)==0xe7)
s.add(UGT(c3 - c1, 0xf4))


#section2 
s.add((c5 - c20) == 0xfe)
s.add(((c10 & c20) ^ (~c5)) == 0xd9)
s.add(((c5 & c10) & (~(c15 ^ c20))) == 0x59)
s.add(UGT(c15 + c10, 0xbd))
s.add(ULT(c15 + c10, 0xd6))


#section3 
s.add(t1 == c7)
s.add((((NAND(c9,c16)&c17)^c12)^c14)==0x51)
s.add(c13+c6==0xb5)
s.add(t1 - NAND(c12,SHL2(c6)) == 0x74)
s.add((c16^c8)==0x2c)
s.add((c17-c8)==0xef)
s.add(((NAND(t2,c14)^t2)|c18)==0x37)
s.add(t2+c19==0x0d)
s.add((c13-c8)==0x2e)
s.add(((c17-c18)&c9)==0x33)
s.add((c18+(c9^c19))==0xab)


i = 1

while s.check() == sat:
    m = s.model()
    vals = [m.eval(x).as_long() for x in v]

    print(f"\n{i}")
    for var, val in zip(v, vals):
        print(f"{var.decl().name()}={val:02x}", end=" ")
    print("")
    
    chars = ''.join(chr(x) if 32 <= x <= 126 else '.' for x in vals)
    print(f"chars: {chars}")

    if '.' not in chars:
        break

    s.add(Or(*[
        var != BitVecVal(val, 8)
        for var, val in zip(v, vals)
    ]))

    i += 1

print(f"\nTotal: {i-1}")

Output:

.
..
...
....
75
c1=4c c2=33 c3=41 c4=4b c5=7b c6=10 c7=73 c8=77 c9=3b c10=df c11=d0 c12=12 c13=a5 c14=27 c15=df c16=5b c17=66 c18=33 c19=43 c20=7d
chars: L3AK{.sw;....'.[f3C}

76
c1=4c c2=33 c3=41 c4=4b c5=7b c6=10 c7=73 c8=77 c9=3b c10=df c11=d0 c12=13 c13=a5 c14=26 c15=df c16=5b c17=66 c18=33 c19=43 c20=7d
chars: L3AK{.sw;....&.[f3C}

77
c1=4c c2=33 c3=41 c4=4b c5=7b c6=43 c7=6f c8=44 c9=33 c10=5f c11=48 c12=55 c13=72 c14=17 c15=5f c16=68 c17=33 c18=34 c19=44 c20=7d
chars: L3AK{CoD3_HUr._h34D}

78
c1=4c c2=33 c3=41 c4=4b c5=7b c6=43 c7=6f c8=44 c9=33 c10=df c11=48 c12=55 c13=72 c14=17 c15=df c16=68 c17=33 c18=34 c19=44 c20=7d
chars: L3AK{CoD3.HUr..h34D}

79
c1=4c c2=33 c3=41 c4=4b c5=7b c6=43 c7=6f c8=44 c9=33 c10=df c11=48 c12=75 c13=72 c14=37 c15=df c16=68 c17=33 c18=34 c19=44 c20=7d
chars: L3AK{CoD3.Hur7.h34D}

80
c1=4c c2=33 c3=41 c4=4b c5=7b c6=43 c7=6f c8=44 c9=33 c10=5f c11=48 c12=75 c13=72 c14=37 c15=5f c16=68 c17=33 c18=34 c19=44 c20=7d
chars: L3AK{CoD3_Hur7_h34D}

Total: 79

Final flag:

L3AK{CoD3_Hur7_h34D}

The revenge challenge for this was even more laborius, check out the writeup here.