NSEC21 rules - Sun, May 23, 2021 - Jean Privat & al.
One single point can make the whole difference
Rules are a set of constraints that people or things should follow.
In this challenge, we are given a piece of lore about an infrastructure, a code of conduct and some other things. However, one element is more prominent.
* DO NOT attack other teams. * DO NOT attack the scoring system (ask-god). * DO NOT attack anything outside of *.ctf (or 9000::/16). * DO NOT steal or/and exchange flags between teams. * DO NOT not submit this flag
flag is blue, it’s possible that it is some kind of hint, as we may show later.
What we have is not some random sentences, but something that looks like a formal system, i.e. sentences with meaning.
Fist, we need to translate the sentences into something more parsable by the computer. You can use sed for instance and get the following:
(declare-const attack-other-teams Bool) (declare-const attack-the-scoring-system Bool) (declare-const attack-anything-outside-of-ctf Bool) (declare-const steal Bool) (declare-const exchange-flags-between-teams Bool) (declare-const submit-this-flag Bool) (assert (and (not attack-other-teams) (not attack-the-scoring-system) (not attack-anything-outside-of-ctf) (not (or steal exchange-flags-between-teams)) (not (and steal exchange-flags-between-teams)) (not (not submit-this-flag)))) (check-sat) (get-model)
We had some doubts about what the
or/and was. We just duplicate the rule: one with
or and one with
Now, we can solve the logical system with a solver, that is some kind of computer program that can directly give an answer without previously training it (unlike machine learning).
In order to run a computer program, we need to install an operating system.
TODO. steps to install Debian, choose Greek at the language selection screen because it should help solving logical problems.
Now we have an operating system, just install some solver.
$ sudo apt install z3
We can run z3 on the formal system to knows what what the hidden meaning; go grab a bottle of Mata, computation can be extensive.
$ z3 rules.z3 sat (model (define-fun attack-other-teams () Bool false) (define-fun exchange-flags-between-teams () Bool false) (define-fun attack-the-scoring-system () Bool false) (define-fun attack-anything-outside-of-ctf () Bool false) (define-fun steal () Bool false) (define-fun submit-this-flag () Bool true) )
So, what we have do now is a lot more clear than at the begin of the challenge.
- Attack other teams? No, don’t!
- Exchange flags between teams? No, don’t!
- Attack the scoring system? No, don’t!
- Attack anything outside of
*.ctf? No, don’t!
- Steal? No, don’t!
- Submit this flag? Yes, do it!
So we did.