**TL;DR:** Obfuscated Python code using lambda-calculus.
**Description:** Mary had a flagchecker, its fleece was white as snow.
## Introduction
We are given a Python script, consisting in a single line of ~26k characters,
with lots of lambda-functions. The full script is available
[here](https://github.com/ret2school/ctf/blob/master/2023/imaginaryctf/reverse/sheepish/src/sheepish.py)
, see the beginning and the end of the file below.
```python
print((((lambda _____________:((lambda ___:_____________(lambda
_______:___(___)(_______)))(lambda ___:_____________(lambda
_______:___(___)(_______)))))(lambda _____________:lambda ___________:lambda
______:(lambda ____:(lambda _:_(lambda __________:lambda
_____:__________))(____))(___________)(lambda _:(lambda __________:lambda
_____:__________))(lambda _:(lambda __________:lambda
_____:__________(_____)(lambda __________:lambda _____:_____))((lambda
__________:lambda _____:(lambda __________:lambda
_____:__________(_____)(lambda __________:lambda _____:_____))((lambda
__________:lambda _____:(lambda __________:__________(lambda _:(lambda
__________:lambda _____:_____))(lambda __________:lambda _____:__________))
[...]
(lambda _____________:(lambda ________:(((lambda ____:lambda ___:(lambda
__________:lambda _____:lambda
______________:______________(__________)(_____))(lambda __________:lambda
_____:_____)((lambda __________:lambda _____:lambda
______________:______________(__________)(_____))(___)(____)))(_____________(________[1:]))(((lambda
_____________:((lambda ___:_____________(lambda
_______:___(___)(_______)))(lambda ___:_____________(lambda
_______:___(___)(_______)))))(lambda _____________:(lambda __:(((lambda
__:lambda __________:lambda
_____:__________(__(__________)(_____)))(_____________(__-1))) if __ else
(lambda __________:lambda _____:_____)))))(________[0]))) if len(________)
else ((lambda __________:lambda _____:lambda
______________:______________(__________)(_____))(lambda __________:lambda
_____:__________)(lambda __________:lambda _____:__________))))))(input(">>>
").encode())))("Well done!")("Try again..."))
```
In order to make the code more "readable", we can replace the variable names
(`_`, `__`, `___`, ...) with more readable names (`x1`, `x2`, `x3`, ...)
## A bit of culture
In theoretical computer science, it is known that [lambda-
calculus](https://en.wikipedia.org/wiki/Lambda_calculus) is Turing-complete.
In other words, any program can be simulated with "lambda-terms", namely,
terms similar to `lambda` functions in Python.
For instance, the constant "true" can be simulated with the lambda-term
λx.λy.x, and "false" with λx.λy.y. Integers can be represented as [Church
numerals](https://en.wikipedia.org/wiki/Church_encoding).
The website provides a good summary of "common
lambda-terms" used to simulate common operations in programming.
## Deobfuscation, and solve
When looking closer at the code, we can observe such terms.
For instance, the constants true and false:
```python
tru = (lambda x10:lambda x5:x10)
fls = (lambda x10:lambda x5:x5)
```
as well as the Church numerals and their arithmetic operations:
```python
power = (lambda x10:lambda x5:x5(x10))
is0 = (lambda x10:x10(lambda x01:(fls))(tru))
succ = (lambda x2:lambda x10:lambda x5:x10(x2(x10)(x5)))
pred = (lambda x2:lambda x13:lambda x3:x2(lambda x12:lambda
x9:x9(x12(x13)))(lambda x01:x3)(lambda x10:x10))
plus = (lambda x10:lambda x5:x10(succ)(x5))
minus = (lambda x10:lambda x5:x5(pred)(x10))
le = (lambda x10:lambda x5:is0(minus(x10)(x5)))
ge = (lambda x10:lambda x5:is0(minus(x5)(x10)))
mult = (lambda x10:lambda x5:lambda x14:x10(x5(x14)))
two = (lambda x10:lambda x5:x10(x10(x5)))
three = (lambda x10:lambda x5:x10(x10(x10(x5))))
four = (succ)(three)
```
The script is now way shorter, and a bit understandable (see
[here](https://github.com/ret2school/ctf/blob/master/2023/imaginaryctf/reverse/sheepish/src/sheepish_deobf2.py)).
We can recognize a sequence of arithmetic expressions, such as:
```
((plus)(mult((power)(two)(four))(succ(mult(two)(three))))((plus)(mult(two)(three))(succ(mult(two)(three)))))
```
The characters of the flag, maybe?
To solve the chall, I took the expressions, and I reimplemented the operators
(full script
[here](https://github.com/ret2school/ctf/blob/master/2023/imaginaryctf/reverse/sheepish/src/sheepish_arith.py)):
```python
def plus(x):
return lambda y: x + y
def mult(x):
return lambda y: x * y
def power(x):
return lambda y: x ** y
def succ(x):
return x+1
zero = 0
two = 2
three = 3
four = 4
flag = ""
flag +=
chr(((plus)(mult((power)(two)(four))(succ(mult(two)(three))))((plus)(mult(two)(three))(succ(mult(two)(three))))))
flag +=
chr(((plus)(mult((power)(two)(four))(three))(mult((plus)(two)(three))(three))))
[...]
flag += chr(((plus)(mult((power)(two)(four))(mult(two)(three)))(three)))
flag +=
chr(((plus)(mult((power)(two)(four))(mult(two)(three)))((power)(three)(two))))
print(flag[::-1])
```
**FLAG:** ictf{d0_sh33p_b@@@?}
## Upsolve
Even if identifying the arithmetic expressions was enough to solve the
challenge, I was curious to understand the rest of the script.
In particular, the first lambda-term is very strange:
```python
(lambda x13:((lambda x3:x13(lambda x7:x3(x3)(x7)))(lambda x3:x13(lambda
x7:x3(x3)(x7)))))
```
`x3` is applied to itself!
This term is a fixed-point combinator, more precisely a Z combinator: see
theoretical details [here](https://en.wikipedia.org/wiki/Fixed-
point_combinator). Roughly, it's a term that can be used to simulate
recursion.
Moreover, a long sequence of "chained" pairs appears at the beginning:
```python
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4))) ((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4))) (pair(tru)(tru)) [...]) [...])
[...])
```
This term actually represents a linked list, whose elements are the
susmentionned arithmetic expressions.
After further deobfuscation/understanding, we can conclude that the script
performs successive comparisons on the chars of the input, in reverse order,
with the chars in the linked list.
## Conclusion
As a functional programming lover, I enjoyed a lot solving this chall. A big
thanks to the author!
I know it was possible to side-channel it, but it was funnier with lambda-
calculus :)
Original writeup (https://ret2school.github.io/post/sheepish/).**TL;DR:** Obfuscated Python code using lambda-calculus.
**Description:** Mary had a flagchecker, its fleece was white as snow.
## Introduction
We are given a Python script, consisting in a single line of ~26k characters,
with lots of lambda-functions. The full script is available
[here](https://github.com/ret2school/ctf/blob/master/2023/imaginaryctf/reverse/sheepish/src/sheepish.py)
, see the beginning and the end of the file below.
```python
print((((lambda _____________:((lambda ___:_____________(lambda
_______:___(___)(_______)))(lambda ___:_____________(lambda
_______:___(___)(_______)))))(lambda _____________:lambda ___________:lambda
______:(lambda ____:(lambda _:_(lambda __________:lambda
_____:__________))(____))(___________)(lambda _:(lambda __________:lambda
_____:__________))(lambda _:(lambda __________:lambda
_____:__________(_____)(lambda __________:lambda _____:_____))((lambda
__________:lambda _____:(lambda __________:lambda
_____:__________(_____)(lambda __________:lambda _____:_____))((lambda
__________:lambda _____:(lambda __________:__________(lambda _:(lambda
__________:lambda _____:_____))(lambda __________:lambda _____:__________))
[...]
(lambda _____________:(lambda ________:(((lambda ____:lambda ___:(lambda
__________:lambda _____:lambda
______________:______________(__________)(_____))(lambda __________:lambda
_____:_____)((lambda __________:lambda _____:lambda
______________:______________(__________)(_____))(___)(____)))(_____________(________[1:]))(((lambda
_____________:((lambda ___:_____________(lambda
_______:___(___)(_______)))(lambda ___:_____________(lambda
_______:___(___)(_______)))))(lambda _____________:(lambda __:(((lambda
__:lambda __________:lambda
_____:__________(__(__________)(_____)))(_____________(__-1))) if __ else
(lambda __________:lambda _____:_____)))))(________[0]))) if len(________)
else ((lambda __________:lambda _____:lambda
______________:______________(__________)(_____))(lambda __________:lambda
_____:__________)(lambda __________:lambda _____:__________))))))(input(">>>
").encode())))("Well done!")("Try again..."))
```
In order to make the code more "readable", we can replace the variable names
(`_`, `__`, `___`, ...) with more readable names (`x1`, `x2`, `x3`, ...)
## A bit of culture
In theoretical computer science, it is known that [lambda-
calculus](https://en.wikipedia.org/wiki/Lambda_calculus) is Turing-complete.
In other words, any program can be simulated with "lambda-terms", namely,
terms similar to `lambda` functions in Python.
For instance, the constant "true" can be simulated with the lambda-term
λx.λy.x, and "false" with λx.λy.y. Integers can be represented as [Church
numerals](https://en.wikipedia.org/wiki/Church_encoding).
The website provides a good summary of "common
lambda-terms" used to simulate common operations in programming.
## Deobfuscation, and solve
When looking closer at the code, we can observe such terms.
For instance, the constants true and false:
```python
tru = (lambda x10:lambda x5:x10)
fls = (lambda x10:lambda x5:x5)
```
as well as the Church numerals and their arithmetic operations:
```python
power = (lambda x10:lambda x5:x5(x10))
is0 = (lambda x10:x10(lambda x01:(fls))(tru))
succ = (lambda x2:lambda x10:lambda x5:x10(x2(x10)(x5)))
pred = (lambda x2:lambda x13:lambda x3:x2(lambda x12:lambda
x9:x9(x12(x13)))(lambda x01:x3)(lambda x10:x10))
plus = (lambda x10:lambda x5:x10(succ)(x5))
minus = (lambda x10:lambda x5:x5(pred)(x10))
le = (lambda x10:lambda x5:is0(minus(x10)(x5)))
ge = (lambda x10:lambda x5:is0(minus(x5)(x10)))
mult = (lambda x10:lambda x5:lambda x14:x10(x5(x14)))
two = (lambda x10:lambda x5:x10(x10(x5)))
three = (lambda x10:lambda x5:x10(x10(x10(x5))))
four = (succ)(three)
```
The script is now way shorter, and a bit understandable (see
[here](https://github.com/ret2school/ctf/blob/master/2023/imaginaryctf/reverse/sheepish/src/sheepish_deobf2.py)).
We can recognize a sequence of arithmetic expressions, such as:
```
((plus)(mult((power)(two)(four))(succ(mult(two)(three))))((plus)(mult(two)(three))(succ(mult(two)(three)))))
```
The characters of the flag, maybe?
To solve the chall, I took the expressions, and I reimplemented the operators
(full script
[here](https://github.com/ret2school/ctf/blob/master/2023/imaginaryctf/reverse/sheepish/src/sheepish_arith.py)):
```python
def plus(x):
return lambda y: x + y
def mult(x):
return lambda y: x * y
def power(x):
return lambda y: x ** y
def succ(x):
return x+1
zero = 0
two = 2
three = 3
four = 4
flag = ""
flag +=
chr(((plus)(mult((power)(two)(four))(succ(mult(two)(three))))((plus)(mult(two)(three))(succ(mult(two)(three))))))
flag +=
chr(((plus)(mult((power)(two)(four))(three))(mult((plus)(two)(three))(three))))
[...]
flag += chr(((plus)(mult((power)(two)(four))(mult(two)(three)))(three)))
flag +=
chr(((plus)(mult((power)(two)(four))(mult(two)(three)))((power)(three)(two))))
print(flag[::-1])
```
**FLAG:** ictf{d0_sh33p_b@@@?}
## Upsolve
Even if identifying the arithmetic expressions was enough to solve the
challenge, I was curious to understand the rest of the script.
In particular, the first lambda-term is very strange:
```python
(lambda x13:((lambda x3:x13(lambda x7:x3(x3)(x7)))(lambda x3:x13(lambda
x7:x3(x3)(x7)))))
```
`x3` is applied to itself!
This term is a fixed-point combinator, more precisely a Z combinator: see
theoretical details [here](https://en.wikipedia.org/wiki/Fixed-
point_combinator). Roughly, it's a term that can be used to simulate
recursion.
Moreover, a long sequence of "chained" pairs appears at the beginning:
```python
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4))) ((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda
x3:pair(fls)(pair(x3)(x4)))((lambda x4:lambda x3:pair(fls)(pair(x3)(x4)))
((lambda x4:lambda x3:pair(fls)(pair(x3)(x4))) (pair(tru)(tru)) [...]) [...])
[...])
```
This term actually represents a linked list, whose elements are the
susmentionned arithmetic expressions.
After further deobfuscation/understanding, we can conclude that the script
performs successive comparisons on the chars of the input, in reverse order,
with the chars in the linked list.
## Conclusion
As a functional programming lover, I enjoyed a lot solving this chall. A big
thanks to the author!
I know it was possible to side-channel it, but it was funnier with lambda-
calculus :)
Original writeup (https://ret2school.github.io/post/sheepish/).