Let's start with the winner lists:

And the winners are ...

• #1 2019/06/22 11:16 Nicolas Iooss, winning the HummingBoard Edge
• #2 2019/06/22 18:21 Frederic Perriot, winning the ChipWhisperer
• #3 2019/07/02 01:27 Vincent Dehors, winning the Diva IOT

Congratulation to them!

What was it about?

The challenge is a very plain x64 Linux ELF binary. When executed, its true nature is revealed:

$ ./challenge
Usage: ./challenge SERIAL

A crackme! A quick look reveals the following:

• There is a large ASCII string made of ones and zeroes
• The program is small, and does not appear to be obfuscated or hardened
• The user input is concatenated with the aforementionned string (01 + large string + user input)

That resulting string is then passed to a function that apparently parses it into a tree-like structure, where there are three type of nodes:

• one or more 1s, followed by a zero, which is a leaf of the tree. The number of ones is stored.
• 00, which is followed by a child
• 01, which is followed by two children

The tree is then passed to a function that alters it repeatedly, checks its shape, and print some string if it is happy with the shape. This is where it either starts to get harder, or when the reverser reads the challenge introduction again!

The names Dana and Alonzo were not randomly selected, and searching them with other terms (like scientists, computer science, computation, etc.) should shed some light on the real nature of this challenge. The names belong to Dana Scott and Alonzo Church. The goal here was to nudge the attentive contestant towards the lambda calculus. From here, he is just a step away from discovering the binary lambda calculus, which is what this challenge is about.

Note that this was an optional hint, two of the winners managed to identify the lambda calculus and reverse the program without it!

Binary, untyped, lambda calculus!

The lambda calculus is a universal way to represent computations, just like the Turing machine. It is however much higher level and easier to program with, and many languages are just syntactic sugar over one of the many flavors of lambda calculus.

The untyped (vanilla) lambda calculus is used in this challenge, and is made of three components:

In this challenge, the calculus has been enriched with an extra component: character strings. It is never used in the actual challenge logic, and is merely there at the end to print either Alonzo! or Invalid solution.

It might be really surprising that there are none of the things one usually finds in programming languages : primitive data types, (number, strings, arrays, etc.), control flow operators (if, for, etc.), variable assignment, and so on. What might be even more surprising is that it is not particularly hard to program in this paradigm. But, just like Perl or regexes, reading a program can be much harder than writing it!

A note on reading and reducing lambda calculus expressions

We will describe how the following expression is read, and evaluated:

(\x.\y. y x) a b

This means that the (\x.\y. y x) function is applied to arguments a and b. This works by performing substitution on the lambda expressions, as described here:

(\x.\y. y x) a b     -- initial expression
((\x.(\y. y x)) a) b -- rewrite with explicit parens
(\y. y a) b          -- substitute x in the function with a
b a                  -- substitute y in the function with b

When no substitution can take place, the evaluation stops (there are actually a few more rules and subtleties, but this should suffice to follow this article). Note that the equivalent Python of the previous expression would be:

f = (lambda x: lambda y: y(x))
f(a)(b)

Or, more concisely:

(lambda x: lambda y: y(x))(a)(b)

Armed with this knowledge, it is possible to convert the huge binary string, into the De Bruijn notation, and then in standard lambda calculus notation.

Reversing the lambda calculus

Once decoded, one can observe the expression is, at the top node, a function application of a (large) function to a (large) argument.

The challenge binary applies this whole expression to the user input. It means that the function really takes two arguments: the hardcoded argument and the user input.

Let's look at the function.

Reversing the function

Here is the function, in standard lambda calculus notation:

(\a.(\b.(\c.(\d.(\e.(\f.(\g.(\h.(\i.(\j.(\k.(\l.(\m.(\n.(\o.(\p.(\q.(\r.(\s.(\t.(\u.(\v.(\w.(\x.(\y.(\z.(\aa.(\ab.(\ac.(\ad.(\ae.(\af.(\ag.(\ah.(\ai.(\aj.(\ak.(\al.(\am.(\an.(\ao.(\ap.(\aq.(\ar.(\as.(\at.(\au.(\av.(\aw.(\ax.(\ay.ay) (\ay.\az.q (q (q (q (ag a (ae av ay az)) (ag ao az)) (ag ao (ap az))) (ag ao (at az))) (as az))) (ac i c)) (\aw.\ax.ag ao ax)) (\av.\aw.ag a (ae au av aw))) (\au.\av.q (q (s (d av)) (l av n)) (r (d au) (t au av)))) (\at.aa ad (ad (aa aq (ap (aa aq at)))))) (\as.q (ar as) (ag ar as))) (\ar.t (z ar) n)) ((\aq.(\ar.ar ar) (\ar.aq (ar ar))) (\aq.\ar.ar (\as.\at.at (\au.\av.av (\aw.\ax.v (v as (v au (v aw u))) (aq ax)) (v (v as (v au u)) u)) (v (v as u) u)) u))) (\ap.ac (ae v) (af (z (w ap u)) u) ap)) (am ah)) ((\an.(\ao.ao ao) (\ao.an (ao ao))) (\an.\ao.\ap.ap (\aq.\ar.ak aq ao ao (an (aj aq ao) ar)) ao))) ((\am.(\an.an an) (\an.am (an an))) (\am.\an.\ao.ao (\ap.\aq.ak ap an p (am (aj ap an) aq)) (t (al an) n)))) ((\al.(\am.am am) (\am.al (am am))) (\al.\am.am (\an.\ao.\ap.e (i (al an) (al ap))) c))) ((\ak.(\al.al al) (\al.ak (al al))) (\ak.\al.\am.am (\an.\ao.\ap.t al ao o (l al ao (ak al an) (ak al ap))) p))) ((\aj.(\ak.ak ak) (\ak.aj (ak ak))) (\aj.\ak.\al.al (\am.\an.\ao.l ak an (ai (aj ak am) an ao) (ai am an (aj ak ao))) (ai ah ak ah)))) (\ai.\aj.\ak.\al.\am.al ai aj ak)) (\ah.\ai.ai)) (\ag.ac (\ah.\ai.q (ag ah) ai) o)) (\af.\ag.af (v ag) u)) ((\ae.(\af.af af) (\af.ae (af af))) (\ae.\af.\ag.\ah.ag (\ai.\aj.ah (\ak.\al.v (af ai ak) (ae af aj al)) u) u))) (ac ab u)) ((\ac.(\ad.ad ad) (\ad.ac (ad ad))) (\ac.\ad.\ae.\af.af (\ag.\ah.ad ag (ac ad ae ah)) ae))) ((\ab.(\ac.ac ac) (\ac.ab (ac ac))) (\ab.\ac.\ad.ac (\ae.\af.v ae (ab af ad)) ad))) ((\aa.(\ab.ab ab) (\ab.aa (ab ab))) (\aa.\ab.\ac.ac (\ad.\ae.v (ab ad) (aa ab ae)) u))) ((\z.(\aa.aa aa) (\aa.z (aa aa))) (\z.\aa.aa (\ab.\ac.e (z ac)) c))) (\y.y (\z.\aa.p) o)) (\x.x (\y.\z.z) u)) (\w.w b)) (\v.\w.\x.\y.x v w)) (\u.\v.v)) (\t.\u.q (l t u) (l u t))) (\s.\t.\u.s u t)) (\r.\s.\t.\u.r t (s t u))) (\q.\r.\s.\t.q (r s t) t)) (\p.\q.q)) (\o.\p.o)) (m h h)) (\m.\n.\o.m (n o))) (\l.\m.d (k l m))) (\k.\l.l j k)) (\j.\k.\l.j (\m.\n.n (m k)) (b l) a)) (\i.\j.\k.\l.i k (j k l))) (e g)) (e f)) (e c)) (\e.\f.\g.f (e f g))) (\d.\e.\f.d (b f) e)) (\c.a)) (\b.\c.b)) (\a.a)

This might look completely unreadable at first, but it has a structure: it is made of nested (\function_name. program) function_body expressions. This is the canonical way of introducing subfunctions, for example:

(\4. (\5. (\plus. plus 4 5) (plus function body)) (number 5)) (number 4)

The preceding expression introduces 4, 5 and plus in the scope of the inner function that then adds 4 to 5. This pattern is so common that most functional languages have syntactic sugar for it, usually using the let keyword:

let 4 = "number 4"
    5 = "number 5"
    plus = "plus function body"
in  plus 4 5

If we apply the same transformation to previous expression, we get the following:

let a = \a.a
    b = \b.\c.b
    c = \c.a
    d = \d.\e.\f.d (b f) e
    e = \e.\f.\g.f (e f g)
    f = e c
    g = e f
    h = e g
    i = \i.\j.\k.\l.i k (j k l)
    j = \j.\k.\l.j (\m.\n.n (m k)) (b l) a
    k = \k.\l.l j k
    l = \l.\m.d (k l m)
    m = \m.\n.\o.m (n o)
    n = m h h
    o = \o.\p.o
    p = \p.\q.q
    q = \q.\r.\s.\t.q (r s t) t
    r = \r.\s.\t.\u.r t (s t u)
    s = \s.\t.\u.s u t
    t = \t.\u.q (l t u) (l u t)
    u = \u.\v.v
    v = \v.\w.\x.\y.x v w
    w = \w.w b
    x = \x.x (\y.\z.z) u
    y = \y.y (\z.\aa.p) o
    z = (\z.(\aa.aa aa) (\aa.z (aa aa))) (\z.\aa.aa (\ab.\ac.e (z ac)) c)
    aa = (\aa.(\ab.ab ab) (\ab.aa (ab ab))) (\aa.\ab.\ac.ac (\ad.\ae.v (ab ad) (aa ab ae)) u)
    ab = (\ab.(\ac.ac ac) (\ac.ab (ac ac))) (\ab.\ac.\ad.ac (\ae.\af.v ae (ab af ad)) ad)
    ac = (\ac.(\ad.ad ad) (\ad.ac (ad ad))) (\ac.\ad.\ae.\af.af (\ag.\ah.ad ag (ac ad ae ah)) ae)
    ad = ac ab u
    ae = (\ae.(\af.af af) (\af.ae (af af))) (\ae.\af.\ag.\ah.ag (\ai.\aj.ah (\ak.\al.v (af ai ak) (ae af aj al)) u) u)
    af = \af.\ag.af (v ag) u
    ag = \ag.ac (\ah.\ai.q (ag ah) ai) o
    ah = \ah.\ai.ai
    ai = \ai.\aj.\ak.\al.\am.al ai aj ak
    aj = (\aj.(\ak.ak ak) (\ak.aj (ak ak))) (\aj.\ak.\al.al (\am.\an.\ao.l ak an (ai (aj ak am) an ao) (ai am an (aj ak ao))) (ai ah ak ah))
    ak = (\ak.(\al.al al) (\al.ak (al al))) (\ak.\al.\am.am (\an.\ao.\ap.t al ao o (l al ao (ak al an) (ak al ap))) p)
    al = (\al.(\am.am am) (\am.al (am am))) (\al.\am.am (\an.\ao.\ap.e (i (al an) (al ap))) c)
    am = (\am.(\an.an an) (\an.am (an an))) (\am.\an.\ao.ao (\ap.\aq.ak ap an p (am (aj ap an) aq)) (t (al an) n))
    an = (\an.(\ao.ao ao) (\ao.an (ao ao))) (\an.\ao.\ap.ap (\aq.\ar.ak aq ao ao (an (aj aq ao) ar)) ao)
    ao = am ah
    ap = \ap.ac (ae v) (af (z (w ap u)) u) ap
    aq = (\aq.(\ar.ar ar) (\ar.aq (ar ar))) (\aq.\ar.ar (\as.\at.at (\au.\av.av (\aw.\ax.v (v as (v au (v aw u))) (aq ax)) (v (v as (v au u)) u)) (v (v as u) u)) u)
    ar = \ar.t (z ar) n
    as = \as.q (ar as) (ag ar as)
    at = \at.aa ad (ad (aa aq (ap (aa aq at))))
    au = \au.\av.q (q (s (d av)) (l av n)) (r (d au) (t au av))
    av = \av.\aw.ag a (ae au av aw)
    aw = \aw.\ax.ag ao ax
    ax = ac i c
    ay = \ay.\az.q (q (q (q (ag a (ae av ay az)) (ag ao az)) (ag ao (ap az))) (ag ao (at az))) (as az)
in  ay

Not all subfunctions are used in the final result, and the subfunctions were sorted in a way that should help beginners to the lambda calculus.

The first group of functions is indeed about Church-encoded naturals. As their name implies, they are used to encode natural numbers in the lambda calculus. But how is that possible, with only functions and variable names?

The usual way is to represent them as functions taking two arguments, the first argument being a function that increments a natural number (f), the second representing zero (z). As a result:

one   = \f.\z. f z
two   = \f.\z. f (f z)
three = \f.\z. f (f (f z))
...

A natural number n, when encoded this way, applies n times the function f to z. This encoding is not efficient at all, as the size of the term grows lineraly with the number, but is simple enough for our purpose.

The following functions could be easily identified using Wikipedia:

• natural number functions, such as plus, succ, mult the numbers 1, 2, 3 and 9, minus, == and <=.
• Scott encoded lists functions, such as nil, cons, head, tail, null
• recursive functions using the Y combinator
• boolean logic

The remaining functions can't be identified just by pattern-matching them with Wikipedia, and it was possible to solve the challenge at this point without reversing them. We will however describe how this could be done, for example with the following function:

(\z.(\aa.aa aa) (\aa.z (aa aa))) (\z.\aa.aa (\ab.\ac.e (z ac)) c)

The first part of the expression is the Y combinator, that is used for recursive functions. As previously found on Wikipedia, e and c are actually succ (short for successor, this is basically +1) and zero. We can rewrite the expression as a the following recursive function (note how the name f is used in the function body):

let f = \aa.aa (\ab.\ac.succ (f ac)) zero

Now, this function is in the middle of Scott encoded lists functions, and one can indeed find a list here:

let f = \list. list (\list_head. \list_tail. succ (f list_tail)) zero

So this function takes a list as its first parameter. If the list is empty, it returns zero. If the list is not empty, the first element of the list (named head) and the remaining of the list (named tail) are passed to this functions:

\list_head. \list_tail. succ (f list_tail)

In Python, this function could be written as:

def f(lst):
  if lst:
    head, *tail = lst
    return 1 + f(tail)
  else:
    return 0

This function computes the length of a list!

Another function:

(\aa.(\ab.ab ab) (\ab.aa (ab ab))) (\aa. \ab. \ac.ac (\ad. \ae.v (ab ad) (aa ab ae)) u)
-- recognize Y combinator, u is nil, v is cons
let unk = \ab. \ac.ac (\ad. \ae.cons (ab ad) (unk ab ae)) nil
-- recognize Scott list
let unk = \ab. \list. list (\head. \tail. cons (ab head) (unk ab tail)) nil
-- recognize that ab was a function
let unk = \f. \list. list (\head. \tail. cons (f head) (unk f tail)) nil

In python:

def unk(f, lst):
  if lst:
    head, *tail = lst
    new_head = f(head)
    new_tail = unk(f, tail)
    return [new_head] + new_tail
  else:
    return []

This is the map function!

Reversing the final check

The final check is:

\ay. \az.q (q (q (q (ag a (ae av ay az)) (ag ao az)) (ag ao (ap az))) (ag ao (at az))) (as az)

ay is the large hardcoded argument that was identified at the beginning (named hardcoded from now one), and az is the user input (named input). By looking Wikipedia up, it was possible to realize q was boolean and, a is the identity function, ae was zipWith, and ag was all, a function that checks that a property is true for all elements in a list:

\hardcoded. \input.  and (and (and (and
     (all id (zipWith av hardcoded input)) -- prop 1
     (all ao input))                       -- prop 2
     (all ao (ap input)))                  -- prop 3
     (all ao (at input)))                  -- prop 4
     (as input)                            -- prop 5

There are five distincts properties that must all be true to pass the check.

Most checks are about the user input (as expected), but the first is about both hardcoded and input. Not only that, but they are combined with zipWith.

zipWith takes a function and two lists. It zips both lists, and maps the function to the resulting pairs:

zipWith (+) [1,2,3] [6,6,6] = [7,8,9]
zipWith (++) ["a","b","c"] ["lo", "la", "li"] = ["alo","bla","cli"]

That means that both hardcoded and input are lists, but they also probably should be the same size!

Looking at that av function, after substitution of all known functions:

\b1. \b2.all id (zipWith au b1 b2)

This means that all elements of hardcoded and input are themselves lists, of the same size. The input and hardcoded are list of lists.

Reversing the argument

Armed with this knowledge, it is easy to decode hardcoded as a list of list of naturals:

[ [4, 0, 0, 0, 0, 0, 8, 0, 5]
, [0, 3, 0, 0, 0, 0, 0, 0, 0]
, [0, 0, 0, 7, 0, 0, 0, 0, 0]
, [0, 2, 0, 0, 0, 0, 0, 6, 0]
, [0, 0, 0, 0, 8, 0, 4, 0, 0]
, [0, 0, 0, 0, 1, 0, 0, 0, 0]
, [0, 0, 0, 6, 0, 3, 0, 7, 0]
, [5, 0, 0, 2, 0, 0, 0, 0, 0]
, [1, 0, 4, 0, 0, 0, 0, 0, 0]
]

This is a 9x9 grid of numbers. Yes, the crackme was actually asking for the solution of a Sudoku!

The winners managed to recognize this list after reversing parts of the main function. One of them even immediately recognized the list and did not bother looking at the code!

Behind the scenes

The first version of the challenge shipped with a missing piece: user input was not checked for free variables! That meant that one could reference variables that belonged to the "outer scope", and more specifically the Alonzo! variable. This was found quite quickly by Jérémy Jean, who ran a brute-forcer on the program before starting to reverse. A second version of the challenge was published, and after that it took 6 days for the first successful solution to be sent.

While the first verification failure was unfortunate, there were still ways to bypass the checks:

• one could find a vulnerability in the C interpreter;
• one could send user input that has not the expected type, getting the program to perform arbitrary computations.

While theorically possible, we thought that those flaws would be much harder to exploit than doing the actual reverse-engineering. It turned out we were wrong!

Not only did Paolo Montesel successfully craft an input that bypassed all the checking logic, he did so automatically. He reversed the interpreter, but did not recognize it was a lambda calculus interpreter. He wrote a genetic algorithm-based optimizer that would rate user input based on the number of cycles it ran during the reduction process while still having the Alonzo! string in the tree.

Conclusion

Congratulation to all the winners! We hope that all participants found this challenge interesting, and, if stumped by the unusual virtual machine, have now all the keys to finish reversing it on their own.

It was also an unusual introduction to the lambda calculus, so, if you missed the challenge and would like to try your hand at reversing some lambda calculus, here is a large function for you to play with:

01000100010001000100010001000100010001000100010001000100010000000101000000000101111100101111011010100101000000000101111100101111011010100101000000000101111100101111011010100101000000000101111100101111011010100101111111100010010101111111110000001011111111110001001010111111111110000001010000000001011111001011110110101000000101111000010101011111111111111111111111011110111111111111111111111011101101000000101111100001010101111111111111111111110111110111101110110110110101101001011111111011111101001011111111011111100111111010010111111110111111001011111111111101111111110011111111110010111111111111011110011111100101111111111110111101000000101011111101110010101011111111110111110111011010100001011111111111100111111111110101111111111110010001101000010000010110000001011000000101100000010100000000010111011110111000000101110111111110000001011101111111100000010111011111111000001001111111110100000010111000000101110111111110000001011101111111100000100000100000010111000000101110111111000001000001000001001101000010101111111001111100000000001011101111011100101011111111100101100000110000010000000010111000001011100000101001010001101000000001011000000101010101000110100001000000010110000000010101011111111111111111111011111011000001100101010111111111111111111111101111101100101111111011111011100101111111011111010000010011010110111100000100101011111101111100101010001101000010000000101100000000101010111111111111111111111101111101100101010000000000010101110111110111101110010111111101111101110110100000010101110111110111100101111111110111111101110000001010111000001011110000010011010110111101001011111111111001010001101000010000010110000000011111111111111111111100000010101111111101111101100101011111111011101101000001001101011011111111111000001000010111110000000000101011111101111001011110110101000001100100011010000100000000010111000000101111000000101000000000101110111101110010111111110111101100101011111111101111111011101000001000001001101001011001000110100000000101110000000000101110111100101011111111011111110111011111010000010010001101000000000010110000001011111101100101010111111101111110111110111101011001000110100000000101100000000001011100111111101111001010111111110111111101111110111000001001000110100000010110000001111111111001011111011110100000100000010100000000010111110010111101101010010111110110100101111101011000011110011110100000000001010101111000000001010111100000011001110111100011000101111000110110011001100110000010000000011100101111011010

This is actually the exact same function that is used in the real challenge, except in normal form. This is the same challenge in hard mode. Can you decode this string, convert the De Bruijn encoding into standard notation, and recognize any of the previously mentionned functions in there? How are sudoku solutions really verified? Have fun!