Sys

Author: Junming Liu

Date: October 13, 2024

#tutorial #stack #haskell #paper

Code

Main.hs

在Main.hs中 import Lib , 在Lib.hs中定义了实际import的Checker以及函数。

main :: IO ()
main = withStdOutLogger $ do
  argv <- getArgs
  case getOpt Permute options argv of
    (flags,_,[]) -> case sort flags of
                      flist | length flist < 3 -> ioError $ userError $ "Not enough flags" ++
                                              usageInfo header options
                      flist -> do
                        let dir      = dirOpt $ flist !! 0
                            extns    = makeExtns $ extnOpt $ flist !! 1
                            check    = checkFunction extns $ ckerOpt $ flist !! 2
                        check dir
    (_,_,errs) -> ioError $ userError $ concat errs ++ usageInfo header options
  where header = "Usage: "

Lib.hs

concrOOB

--
-- Concrete out of bounds checker
--

-- | Run the concrete out of bounds checker
concrOOB :: FilePath
         -> [String]
         -> IO ()
concrOOB fpath extns = do
  candidates <- checkFiles concroobConfig fpath extns
  candidateGroup <- new
  forM_ candidates $ \ bug ->
    void $ forkIO candidateGroup $ E.handle printHandler $ do
    attackResult <- doConcrOOBCheck bug
    showNegBug bug attackResult
  wait candidateGroup

doConcrOOBCheck :: COOBBug -> IO SolverResult
doConcrOOBCheck (COOBBug _ negIdx negAmt path fname fp) = do
  modInfo <- makeModuleInfo fp
  let staticPath = makeIntraproStaticPath modInfo fname path
  symexPath (SymConfigs.concroobSymexConfig negIdx negAmt) [fname] [modInfo] staticPath

candidates

使用checkFiles，根据concroobConfig中的设置，进行静态分析，生成candidates。其中，candidates是一组可能存在错误的候选点。

candidates <- checkFiles concroobConfig fpath extns

An example of candidates:

COOBBug {
  negVar = Name "_ZN5media9WebmMuxer13AddAudioTrackERKNS_15AudioParametersE_38", 
  negIndex = Right 19, 
  negAmount = 19, 
  negPath = [UnName 2,UnName 15,UnName 21,UnName 37], 
  negFunction = Name "_ZN5media9WebmMuxer13AddAudioTrackERKNS_15AudioParametersE", 
  negFile = "/home/user/src/sys/test/Bugs/Concrete/webm_muxer.ll-O2_p"}
  • 在函数_ZN5media9WebmMuxer13AddAudioTrackERKNS_15AudioParametersE中，通过基本块路径2-><label>:15-><label>:21-><label>:37，最终在块37处由于访问了%38变量而导致潜在OOB。
  • negVar: 变量名, 其中_ZN5media9WebmMuxer13AddAudioTrackERKNS_15AudioParametersE为函数名，38为变量名指%38。
  • negPath: 基本块路径, 2-><label>:15-><label>:21-><label>:37
  • negIndex: 导致越界的索引, 19
    • Left Name: variable index
    • Right Integer：constant index
  • negAmount: 索引大小(The size of the OOB index), 19
; <label>:37:                                     ; preds = %21
  store i8 1, i8* %36, align 2
  %38 = getelementptr inbounds [19 x i8], [19 x i8]* %3, i64 0, i64 19
  store i8 %26, i8* %38, align 1

通过查看上述LLVM代码可以看到，在块37中，代码试图通过%38 = getelementptr inbounds [19 x i8], [19 x i8]* %3, i64 0, i64 19访问数组%3的第19个元素，而数组大小为19，因此存在潜在OOB。

doConcrOOBCheck

doConcrOOBCheck :: COOBBug -> IO SolverResult
doConcrOOBCheck (COOBBug _ negIdx negAmt path fname fp) = do
  modInfo <- makeModuleInfo fp
  let staticPath = makeIntraproStaticPath modInfo fname path
  symexPath (SymConfigs.concroobSymexConfig negIdx negAmt) [fname] [modInfo] staticPath
  • symexPath: 符号执行函数
    • Parameters:
      • SymConfig.Config a：每种漏洞类型的相应配置，例如OOB的negIdx和negAmt (SymConfigs.concroobSymexConfig negIdx negAmt)。
      • [Name]：函数名
      • [ModuleInfo]：模块信息，通过makeModuleInfo获取
      • StaticPath：静态路径，通过makeIntraproStaticPath获取
    • Return: SolverResult

Log setting

  • Control/Log.hs: Log Module
  • Set log level by setting environment variable LOG_LEVEL
    • debug, info, warn, error 
      export LOG_LEVEL=debug

#

safeUses

指令涉及到 Load 或 Store 操作，通常这些操作可能会涉及到对数组或内存的读写，因此被认为是不安全的（返回 False）。 其他指令默认是安全的（返回 True）。

concreteOOBCheck

  • 遍历指令ninstr，如果存在name := GetElementPtr，则进行一系列检查：

External Static Analysis Integration

  1. 对于每种漏洞类型，提供一组潜在漏洞点candidates
    • Note: candidates格式需要根据漏洞类型来进行调整，具体格式在各漏洞类型的静态分析检查器中进行定义。e.g., ConcreteOOBStatic.hs中定义了data COOBBug。 
        candidates <- checkFiles concroobConfig fpath extns

        data COOBBug = COOBBug { negVar      :: Name
                -- ^ Name of the result of the OOB operation
                -- For example, if the following is OOB, x is the name:
                -- x = GEP y OOB indecies
                , negIndex    :: (Either Name Integer)
                -- ^ Either the name of the variable causing the OOB or
                -- the value of the constant causing the OOB
                , negAmount   :: Integer
                -- ^ The size of the OOB index
                , negPath     :: Path
                , negFunction :: Name
                , negFile     :: String
                }
        deriving (Eq, Ord, Show)
  2. 对于每个潜在漏洞点bug，通过doConcrOOBCheck中的symexPath进行symbolic execution
    • Note: 每种漏洞类型的symexPath配置不同，例如ConcreteOOB需要提供的negIdx（访问的index）和negAmt（The size of the OOB index） 
        attackResult <- doConcrOOBCheck bug

        modInfo <- makeModuleInfo fp
  symexPath (SymConfigs.concroobSymexConfig negIdx negAmt) [fname] [modInfo] staticPath

Haskell语法

函数签名

  • haskell: 函数名
  • FilePath, [String]: 参数类型
  • IO (): 返回类型
heapOOB :: FilePath
        -> [String]
        -> IO ()

do

  • do: 定义函数体
  • <-: 从IO Monad中取出值，赋给变量。

在这个例子中，通过checkFiles这个IO操作，返回给candidates的赋值。

heapOOB fpath extns = do
  candidates <- checkFiles heapoobConfig fpath extns
  candidateGroup <- new

for循环

  • forM_：for函数，_ 后缀表示忽略函数返回值。
    • 这里遍历 candidates 列表，并对每个元素 bug 执行给定的操作。
  • forM_ candidates $ \bug ->

void & forkIO & wait

  • void：丢弃某个操作的结果，将其转化为 IO () 类型。通常用于忽略一个有返回值的操作。
  • forkIO & wait：forkIO - 创建并发线程, wait - 等待线程结束。
    • 这里 forkIO 并发执行 candidateGroup 函数，wait等待所有线程结束。
  • E.handle：handle - 异常处理函数, E - 异常模块
void $ forkIO candidateGroup $ E.handle printHandler $ do
    ...
    wait candidateGroup

doHeapOOBCheck

  • MOOBBug：自定义数据类型，表示堆越界错误的候选点。
  • let定义局部变量
  • symexPath: 符号执行函数

LLVM IR Syntax

  • Offical documentation: LLVM Language Reference Manual

  • label: 基本块标签

    ; <label>:15:                                     ; preds = %2

    从前驱基本块%2到当前基本块15的跳转