Bits-Downing (English)

Description

Challenge is running on qual-challs.rtfm.re:10003

Français
Auteur : SIben

Attache-moi une fois, honte sur toi ; attache-moi deux fois...

English
Author: SIben

Bind me once, shame on you; bind me twice...

An archive is available for download. This contains the sources of the challenge. This will allow us to solve it locally.

Directory: Bits-Downing

Mode                LastWriteTime         Length Name
----                -------------         ------ ----
-a----        06/10/2019    00:50           3645 LambdaCalculator.hs
-a----        06/10/2019    01:13            778 LambdaParser.hs
-a----        25/09/2019    05:13            147 LambdaSyntax.hs
-a----        05/10/2019    22:30            184 Main.hs
-a----        05/10/2019    23:23           2662 SimpleParserLibrary.hs

In view of the files, we have to deal with Haskell and lambda computation.

My beautiful Haskell, King of the Haskells!

5 files. An unknown syntax (except for connoisseurs) and a language that is not really user friendly.

Main and SimpleParserLibrairy

Let’s start with the analysis of Main.hs:

module Main where

import System.Environment 
import Data.List

import LambdaParser
import LambdaCalculator

main = getLine >>= getFlag . runParser lambda

So far, nothing too esoteric. The program retrieves the user’s input and transmits it to runParser with the lambda parameter and the user input.
Which is equivalent to:

main = getFlag ( runParser lambda "x" )

The SimpleParserLibrary.hs file contains functions to define a string parser. There’s not much of interest for the challenge. The only useful thing is that we can use parentheses as usual.

parens p = token (char '(') >> p <* token (char ')')

Lamda<*>.hs

The last 3 files are the most interesting.
We know, the challenge parse in our answer. We need to find the syntax to use and what kind of problem we are facing.

The Syntax

Let’s start with the syntax (LambdaSyntax.hs):

module LambdaSyntax where

import Data.List (intercalate)

data E = Var String
       | App E E
       | Abs String E
         deriving (Eq, Show)

We have here the classic definition of the 3 categories of the lambda calculation. For more information, here is the link to Wikipedia https://fr.wikipedia.org/wiki/Lambda-calcul.
As a reminder, here are the 3 possible categories (inspired by Wikipedia):

Translated with www.DeepL.com/Translator

The Parser

Then let’s move on to the definition of the parser (LambdaParser.hs)

lambda = top application
  
application :: StringParser E
application = do
  ls <- many1 notapplication
  return $ foldl1 App ls

notapplication :: StringParser E
notapplication = variable <|>
                 abstraction <|>
                 parens application

variable :: StringParser E
variable = identifier >>= \v -> return $ Var v

abstraction :: StringParser E
abstraction = do
  token (char '\\')
  v <- identifier
  token (char '.')
  e <- application
  return $ Abs v e

We have the syntax to use the lambda calculation. An abstraction is defined as such \x.x or \x.y (here, y is a variable and the ‘function’ that takes x as input will give the variable y as output), but we can also write \x.x x which is an abstraction that allows from x to have the couple composed of x only.

The Challenge

And finally, let’s end with the file LambdaCalculator.hs.
We will look at the end of the file with the functions getFlag and dupAbsName:

dupAbsName :: E -> Bool
dupAbsName = dupAbsNameAux Set.empty
  where
    dupAbsNameAux ns (App f a) =  (dupAbsNameAux ns f) || (dupAbsNameAux ns a)
    dupAbsNameAux ns (Var _)   =  False
    dupAbsNameAux ns (Abs x b)
      | Set.member x ns = True
      | otherwise       = let newNs = ns `Set.union` (Set.singleton x) in
                            dupAbsNameAux newNs b

getFlag :: E -> IO ()
getFlag e | dupAbsName e  = error "No duplicate abstraction name allowed!"
          | dupAbsName e' = putStrLn $ "Congratulations! Flag: " ++ Secret.flag
          | otherwise     = putStrLn "No flag for you!"
  where
    e' = eval e

Considering the character strings used, we must therefore generate a lambda calcul formula that will generate a lambda formula that has 2 abstractions with the same name. However, we cannot use an answer such as (\x.\x.\x.x) to validate the test since the challenge checks the names of the abstractions before applying the reductions specific to the calculation lambda (example of reduction (\x.x)(y) gives y).

The debug in Haskell

To facilitate analysis, I will explain how to print debug displays.
First of all, you must import the Debug.Trace module: import Debug.Trace
Then just add the trace method preceded by the string of characters you want to display just before the place where you want the debug.
Example :

step :: E -> Maybe E
step (App (Abs x b) a) = ("step (App (Abs x b) a) : " ++ show (App (Abs x b) a)) `trace` return $ subst a x b -- beta
step (App f a) | hasRedex f = ("step (App f a) | hasRedex f : " ++ show (App f a)) `trace` step f >>= \f' -> return $ App f' a
step (App f a) | hasRedex a = ("step (App f a) | hasRedex a : " ++ show (App f a)) `trace` step a >>= \a' -> return $ App f a'
step (Abs x b) | hasRedex b = ("step (Abs x b) | hasRedex b : " ++ show (Abs x b)) `trace`
                   step b >>= \b' -> return $ Abs x b'
step _ = ("step nothing") `trace` Nothing

eval :: E -> E
eval e = ("eval e : " ++ show (eval' e 10)) `trace` eval' e 10
  where
    eval' e 0 = error "Number of allowed steps exceeded"
    eval' e n = ("eval' e : " ++ show e ++ " | n : " ++ show n) `trace` case step e of
                  Nothing -> e
                  Just e' -> eval' e' (n - 1)

dupAbsName :: E -> Bool
dupAbsName = dupAbsNameAux Set.empty
  where
    dupAbsNameAux ns (App f a) = ("dupAbsNameAux app : " ++ show ns) `trace` ((dupAbsNameAux ns f) || (dupAbsNameAux ns a))
    dupAbsNameAux ns (Var _)   = ("dupAbsNameAux var : " ++ show ns) `trace` False
    dupAbsNameAux ns (Abs x b)
      | Set.member x ns = ("dupAbsNameAux abs1 : " ++ show ns) `trace` True
      | otherwise       = ("dupAbsNameAux abs2 : " ++ show ns) `trace` let newNs = ns `Set.union` (Set.singleton x) in
                            dupAbsNameAux newNs b

getFlag :: E -> IO ()
getFlag e | ("getFlag dupAbsName") `trace` dupAbsName e  = ("getFlag dupAbsName e : " ++ show e) `trace` error "No duplicate abstraction name allowed!"
          | dupAbsName e' = ("getFlag dupAbsName e': " ++ show e) `trace` putStrLn $ "Congratulations! Flag: " ++ "Flag !!!!"
          | otherwise     = ("getFlag otherwise : " ++ show e) `trace` putStrLn "No flag for you!"
  where
    e' = eval e

Then just compile the project with haskell (haskell-plateform under linux) : ghc -o main Main.hs
And here is the result (with a little more debugging):

getFlag dupAbsName
runParse
abstraction -
abstraction  id - "x"
abstraction app- Var "x"
runParse a : Abs "x" (Var "x")
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
eval' e : Abs "x" (Var "x") | n : 10
step nothing
eval e : Abs "x" (Var "x")
eval' e : Abs "x" (Var "x") | n : 10
step nothing
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
getFlag otherwise : Abs "x" (Var "x")
No flag for you!

Lambda Calculus

Now that we have everything we need to find the right formula.

Let’s look at the behaviour of the challenge:

\x.x \x.x
getFlag dupAbsName
runParse
abstraction -
abstraction  id - "x"
abstraction  id - "x"
abstraction app- Var "x"
abstraction app- App (Var "x") (Abs "x" (Var "x"))
runParse a : Abs "x" (App (Var "x") (Abs "x" (Var "x")))
dupAbsNameAux abs2 : fromList []
dupAbsNameAux app : fromList ["x"]
dupAbsNameAux var : fromList ["x"]
dupAbsNameAux abs1 : fromList ["x"]
getFlag dupAbsName e : Abs "x" (App (Var "x") (Abs "x" (Var "x")))
main: No duplicate abstraction name allowed!
(\x.x)y
getFlag dupAbsName
runParse
abstraction -
abstraction  id - "x"
abstraction app- Var "x"
runParse a : App (Abs "x" (Var "x")) (Var "y")
dupAbsNameAux app : fromList []
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
dupAbsNameAux var : fromList []
eval' e : App (Abs "x" (Var "x")) (Var "y") | n : 10
step (App (Abs x b) a) : App (Abs "x" (Var "x")) (Var "y")
eval' e : Var "y" | n : 9
step nothing
eval e : Var "y"
eval' e : App (Abs "x" (Var "x")) (Var "y") | n : 10
step (App (Abs x b) a) : App (Abs "x" (Var "x")) (Var "y")
eval' e : Var "y" | n : 9
step nothing
dupAbsNameAux var : fromList []
getFlag otherwise : App (Abs "x" (Var "x")) (Var "y")
No flag for you!
(\x.x)\x.x
getFlag dupAbsName
runParse
abstraction -
abstraction  id - "x"
abstraction app- Var "x"
abstraction  id - "x"
abstraction app- Var "x"
runParse a : App (Abs "x" (Var "x")) (Abs "x" (Var "x"))
dupAbsNameAux app : fromList []
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
eval' e : App (Abs "x" (Var "x")) (Abs "x" (Var "x")) | n : 10
step (App (Abs x b) a) : App (Abs "x" (Var "x")) (Abs "x" (Var "x"))
eval' e : Abs "x" (Var "x") | n : 9
step nothing
eval e : Abs "x" (Var "x")
eval' e : App (Abs "x" (Var "x")) (Abs "x" (Var "x")) | n : 10
step (App (Abs x b) a) : App (Abs "x" (Var "x")) (Abs "x" (Var "x"))
eval' e : Abs "x" (Var "x") | n : 9
step nothing
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
getFlag otherwise : App (Abs "x" (Var "x")) (Abs "x" (Var "x"))
No flag for you!

In this case, we didn’t have any errors, so we have to find a function that generates a function with 2 abstractions with the same name.
We also notice that we can very well apply an x abstraction to an x abstraction.

Let’s try to generate an abstraction: (\x.\y.x)(\x.x) -> \y.\x.x

(\x.\y.x)(\x.x)
getFlag dupAbsName
runParse
abstraction -
abstraction  id - "x"
abstraction  id - "y"
abstraction app- Var "x"
abstraction app- Abs "y" (Var "x")
abstraction  id - "x"
abstraction app- Var "x"
runParse a : App (Abs "x" (Abs "y" (Var "x"))) (Abs "x" (Var "x"))
dupAbsNameAux app : fromList []
dupAbsNameAux abs2 : fromList []
dupAbsNameAux abs2 : fromList ["x"]
dupAbsNameAux var : fromList ["x","y"]
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["x"]
eval' e : App (Abs "x" (Abs "y" (Var "x"))) (Abs "x" (Var "x")) | n : 10
step (App (Abs x b) a) : App (Abs "x" (Abs "y" (Var "x"))) (Abs "x" (Var "x"))
eval' e : Abs "y" (Abs "x" (Var "x")) | n : 9
step nothing
eval e : Abs "y" (Abs "x" (Var "x"))
eval' e : App (Abs "x" (Abs "y" (Var "x"))) (Abs "x" (Var "x")) | n : 10
step (App (Abs x b) a) : App (Abs "x" (Abs "y" (Var "x"))) (Abs "x" (Var "x"))
eval' e : Abs "y" (Abs "x" (Var "x")) | n : 9
step nothing
dupAbsNameAux abs2 : fromList []
dupAbsNameAux abs2 : fromList ["y"]
dupAbsNameAux var : fromList ["x","y"]
getFlag otherwise : App (Abs "x" (Abs "y" (Var "x"))) (Abs "x" (Var "x"))
No flag for you!

This works very well and the list used to detect double abstractions is equal to : ["x", "y"]
All right, now let’s try to apply \y.x instead of \x.x.

(\x.\y.x)(\y.x)
getFlag dupAbsName
runParse
abstraction -
abstraction  id - "x"
abstraction  id - "y"
abstraction app- Var "x"
abstraction app- Abs "y" (Var "x")
abstraction  id - "y"
abstraction app- Var "x"
runParse a : App (Abs "x" (Abs "y" (Var "x"))) (Abs "y" (Var "x"))
dupAbsNameAux app : fromList []
dupAbsNameAux abs2 : fromList []
dupAbsNameAux abs2 : fromList ["x"]
dupAbsNameAux var : fromList ["x","y"]
dupAbsNameAux abs2 : fromList []
dupAbsNameAux var : fromList ["y"]
eval' e : App (Abs "x" (Abs "y" (Var "x"))) (Abs "y" (Var "x")) | n : 10
step (App (Abs x b) a) : App (Abs "x" (Abs "y" (Var "x"))) (Abs "y" (Var "x"))
eval' e : Abs "y" (Abs "y" (Var "x")) | n : 9
step nothing
eval e : Abs "y" (Abs "y" (Var "x"))
eval' e : App (Abs "x" (Abs "y" (Var "x"))) (Abs "y" (Var "x")) | n : 10
step (App (Abs x b) a) : App (Abs "x" (Abs "y" (Var "x"))) (Abs "y" (Var "x"))
eval' e : Abs "y" (Abs "y" (Var "x")) | n : 9
step nothing
dupAbsNameAux abs2 : fromList []
dupAbsNameAux abs1 : fromList ["y"]
getFlag dupAbsName e': App (Abs "x" (Abs "y" (Var "x"))) (Abs "y" (Var "x"))
Congratulations! Flag: Flag !!!!

Bingo, we have the flag. Just give our answer to the server to get the real flag.

$ nc qual-challs.rtfm.re 10003
(\x.\y.x)(\y.x)
Congratulations! Flag: sigsegv{c4nt_h4v3_th0s3_tw0_b1nd1ngs}