One single point can make the whole difference | STEG Misc | Nsec21

Rules

Rules are a set of constraints that people or things should follow.

Setup

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

The word flag is blue, it’s possible that it is some kind of hint, as we may show later.

Aristotle

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 and.

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).

Installing Debian

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.

Using z3

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.

Back to Home