Bits-Downing (Français)

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

Une archive est à télécharger. Celle-ci contient les sources du challenge. Nous pourrons ainsi le résoudre en local.

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

Au vu des fichiers, nous avons à faire à du Haskell et du lambda calcul.

Mon beau Haskell, Roi des Haskell !!!

5 fichiers. Une syntaxe inconnue (sauf pour les connaisseurs) et un langage pas franchement user friendly.

Main et SimpleParserLibrairy

Commençons par l’analyse de Main.hs :

module Main where

import System.Environment 
import Data.List

import LambdaParser
import LambdaCalculator

main = getLine >>= getFlag . runParser lambda

Pour l’instant rien de trop ésotérique. Le programme récupère l’input de l’utilisateur pour le transmettre à runParser avec comme paramètre lambda et l’entrée utilisateur.
Ce qui équivaut à :

main = getFlag ( runParser lambda "x" )

Le fichier SimpleParserLibrary.hs contient des fonctions permettant de définir un parseur de chaine de caractères. Il n’y a pas grand-chose d’intéressant pour le challenge. La seule chose utile, c’est que nous pouvons utiliser les parenthèses comme à notre habitude.

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

Lamda<*>.hs

Les 3 derniers fichiers sont les plus intéressants.
Nous savons, le challenge parse notre réponse. Nous devons trouver la syntaxe à utiliser et quelle est le type de problème auxquels nous faisons face.

La syntaxe

Commençons par la syntaxe (LambdaSyntax.hs):

module LambdaSyntax where

import Data.List (intercalate)

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

Nous avons ici la définition classique des 3 catégories du lambda calcul. Pour plus d’informations, voici le lien vers Wikipédia https://fr.wikipedia.org/wiki/Lambda-calcul.
Pour rappel, voici les 3 catégories possibles (inspiré de Wikipédia):

Le parseur

Passons ensuite à la définition du parseur (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

Nous avons la syntaxe à utiliser le lambda calcul. Une abstraction est défini tel quel \x.x ou encore \x.y (ici, y est une variable et la ‘fonction’ qui prend x en entrée donnera la variable y en sortie), mais on peut aussi écrire \x.x x qui est une abstraction qui permet à partir de x d’avoir le couple composé de x uniquement.

Le challenge

Et enfin, terminons par le fichier LambdaCalculator.hs.
On va s’intéresser à la fin du fichier avec les fonctions getFlag et 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

Au vu des chaines de caractères utilisés, nous devons donc générer une formule lambda calcul qui va générer une abstraction lambda qui est composé de 2 abstractions portant le même nom. Cependant, nous ne pouvons pas utiliser une réponse telle que (\x.\x.x) pour valider l’épreuve étant donné que le challenge vérifie les noms des abstractions avant d’appliquer les réductions propres au lambda calcul (exemple de réduction (\x.x)(y) donne y).

Le debug en haskell

Pour faciliter l’analyse, Je vais vous expliquer comment afficher des affichages de debug.
Tout d’abord, vous devez importer le module Debug.Trace : import Debug.Trace
Ensuite il suffit d’ajouter la méthode trace précédée par la chaine de caractères que vous voulez afficher juste avant l’endroit où vous voulez le debug.
exemple :

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

Ensuite il suffit de compiler le projet avec haskell (haskell-plateform sous linux) : ghc -o main Main.hs
Et voilà le résultat (avec un peu pus de debug) :

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

Maintenant que nous avons tout ce qu’il faut pour trouver la bonne formule.

Regardons le comportement du 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!

Dans ce cas, nous n’avons pas eu d’erreur, ainsi nous devons trouver une fonction qui génère une fonction comportant 2 abstractions avec le même nom.
Nous remarquons aussi que nous pouvons très bien appliquer une abstraction x à une abstraction x.

Essayons de générer une 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!

Cela fonctionne très bien et la liste servant à détecter les doubles abstractions est égale à : ["x","y"]
Parfait, tentons maintenant d’appliquer \y.x au lieu de \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 !!, nous avons le flag. Plus qu’à donner notre réponse au serveur pour avoir le véritable flag.

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