Z3

Isso é um writeup de 2 challenges do PlaidCTF 2025 que podiam ser resolvidos usando Z3! O primeiro challenge é um de criptografia chamado excav8. O segundo é um challenge de engenharia reversa chamado Fool's Gulch. Excav8 Como o próprio nome diz, ele tem sim algo relacionado com V8. Esse é o arquivo chall.py fornecido pelo desafio: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 import subprocess secret = open('secret....