2023 Cyber Apocalypse: Cave System

Challenge Information

Summary

This challenge requires reverse engineering a binary that implements a complex multi-condition validation system. The binary checks an input string against hundreds of constraints involving arithmetic and bitwise operations on different byte offsets. Success requires understanding the constraints and finding an input that satisfies all conditions.

Analysis

The binary implements a validation function with an enormous if statement containing hundreds of conditions combined with AND operators. Each condition performs operations like:

• Byte comparisons: local_78._5_1_ * (char)local_58 == '\x14'
• XOR operations: local_68._2_1_ ^ local_70._4_1_ == 0x55
• Arithmetic: (byte)((byte)local_68 - local_68._4_1_) == -6

The input string is parsed into different variables representing different byte offsets, and all conditions must be satisfied simultaneously.

Solution

The approach to solve this:

1. Identify all conditions by analyzing the decompiled code
2. Extract key constraints for analysis
3. Use constraint satisfaction to find valid input
4. Implement brute force or SMT solver if needed

def check_conditions(input_string):
    # Parse input into chunks
    local_88 = input_string[0:8]
    local_80 = input_string[8:16]
    local_78 = input_string[16:24]
    local_70 = input_string[24:32]
    local_68 = input_string[32:40]
    local_60 = input_string[40:48]
    local_58 = input_string[48:56]
    local_50 = input_string[56:64]

    # Check all conditions
    # This would include all the byte-level conditions from the binary
    # For a real solution, extract all conditions from Ghidra decompilation

    return all_conditions_satisfied

For complex binaries, SMT solvers like Z3 can automatically find inputs that satisfy all constraints:

from z3 import *

# Define solver
s = Solver()

# Define variables for input bytes
input_bytes = [BitVec(f'b{i}', 8) for i in range(64)]

# Add constraints
s.add(input_bytes[0] == ord('F'))  # Example: first byte must be 'F'
# ... add all other constraints from binary ...

# Solve
if s.check() == sat:
    model = s.model()
    solution = ''.join(chr(model[b].as_long()) for b in input_bytes)
    print(f"Solution: {solution}")

Key Takeaways

• Complex constraint systems can have multiple solutions
• Binary analysis requires careful constraint extraction
• Automated tools (SMT solvers) help with constraint satisfaction
• Understanding bitwise and arithmetic operations is essential
• Large if statements can be decomposed into individual constraints
• Systematic constraint analysis is more efficient than random guessing