本文为第二部分,第一部分见链接https://xz.aliyun.com/t/2641

本系列的第一部分介绍了Semmle QLMicrosoft安全响应中心(MSRC)如何使用它来调查威胁漏洞。本文讨论了如何利用此工具进行细节演示,其中包括如何使用其实例,并且演示中还包括Azure固件组件的安全审核模块。

这是Azure服务进行安全审查防御的一部分,我们从渗透的边界部分来考虑,并站在攻击者的角度进行攻击假象。之后我们将在后端服务中进行环境操作。

这次审查的目标之一是基于Linux的嵌入式设备,它与服务后端和管理后端连接并在两者之间传递操作数据。 该设备的主要攻击是面向两个接口使用管理协议。

之后我们对其硬件进行手动审查,之后发现其管理协议是基于消息的,其存在超过四百种不同的消息类型,每种类型具有其自己的处理功能。然而手动审计函数很容易产生错误,因此使用Semmle扩展我们的代码审查能降低我们的审计难度。我们使用本文中讨论的静态分析技术总共找到了33个易受攻击的消息处理函数。

攻击定义

我们的第一步是编写一些QL来模拟攻击者的数据。 管理协议在请求 响应的基础上工作,其中每个消息请求的类型都用类别和命令来进行编号标识,并在源代码中使用结构数组定义,例如:

MessageCategoryTable g_MessageCategoryTable[] =
{
    { CMD_CATEGORY_BASE,  g_CommandHandlers_Base },
    { CMD_CATEGORY_APP0,  g_CommandHandlers_App0 },
    …
    { NULL,               NULL                   }
};
CommandHandlerTable g_CommandHandlers_Base [] =
{
    { CMD_GET_COMPONENT_VER,  sizeof(ComponentVerReq),  GetComponentVer,  … },
    { CMD_GET_GLOBAL_CONFIG,  -1,                       GetGlobalConfig,  … },    
    …
    { NULL,                   NULL,                     NULL,             … }
};

在上面的示例中,类别类型为CMD_CATEGORY_BASE且命令类型为CMD_GET_COMPONENT_VER的消息将路由到GetComponentVer函数。 命令处理程序表还具有有关请求消息的预期大小信息,该信息在调用处理函数之前将得到验证。

我们使用以下QL定义了消息处理程序表:

class CommandHandlerTable extends Variable { 
  CommandHandlerTable() { 
    exists(Variable v | v.hasName("g_MessageCategoryTable")
      and this.getAnAccess() = v.getInitializer().getExpr().getAChild().getChild(1)
    ) 
  } 
}

这将获取名为g_MessageCategoryTable的变量,查找其初始化表达式并匹配此表达式的所有子项。而每个子表达式对应于消息类别表的一行。 对于每一行,它采用第二列(因为getChild谓词的参数是零索引的,所以使用getChild(1)),每个列都是对命令处理程序表的引用,并匹配引用的变量。 在上面的示例中是g_CommandHandlers_Baseg_CommandHandlers_App0

我们使用类似的方法定义了消息处理函数集:

class MessageHandlerFunction extends Function { 
  Expr tableEntry; 

  MessageHandlerFunction() { 
    exists(CommandHandlerTable table |
      tableEntry = table.getInitializer().getExpr().getAChild()
      )
    and this = tableEntry.getChild(2).(FunctionAccess).getTarget()
  }

  int getExpectedRequestLength() { 
    result = tableEntry.getChild(1).getValue().toInt() 
  } 
  …
}

此QL类使用成员变量tableEntry来保存所有用于处理程序表中的所有行的命令。这样就可以在特征谓词(MessageHandlerFunction(){...})和getExpectedRequestLength()并引用它,而不重复定义。

所有这些都映射到上面的代码结构,如下所示:

每个消息处理函数都具有相同的签名:

typedef unsigned char UINT8;
int ExampleMessageHandler(UINT8 *pRequest, int RequestLength, UINT8 *pResponse);

此处遵循一般模式,其中请求数据被强制转换为表示消息布局的结构,并并通过其字段访问:

int ExampleMessageHandler(UINT8 *pRequest, int RequestLength, UINT8 *pResponse)
{
    ExampleMessageRequest* pMsgReq = (ExampleMessageRequest *)pRequest;
    …

    someFunction(pMsgReq->aaa.bbb)

    …
}

在此分析中,我们只对请求数据感兴趣。 我们在MessageHandlerFunction QL类中定义了两个额外的谓词来请求数据及其长度:

class MessageHandlerFunction extends Function {
  Expr tableEntry;
  …

  Parameter getRequestDataPointer() {
    result = this.getParameter(0)
  }

  Parameter getRequestLength() {
    result = this.getParameter(1)
  }
}

在这里我们抽象出消息处理函数,因为它可以像任何其他QL类一样使用。 例如,此查询按其复杂度的降序列出所有消息处理函数:

from MessageHandlerFunction mhf
select
  mhf, 
  mhf.getADeclarationEntry().getCyclomaticComplexity() as cc
order by cc desc

数据流分析

现在我们为不受信任的数据定义了一组入口点,下一步我们需要找到漏洞利用的位置。为此我们需要通过代码库来跟踪此类数据的流动。 QL提供了一个功能强大的全局数据流库,它可以抽象出语言的特定细节。

DataFlow库带入查询范围,包括:

import semmle.code.cpp.dataflow.DataFlow

它通过将DataFlow::Configuration设置为子类并覆盖其谓词来定义数据流,因为它应用于QL类DataFlow::Node以便表示数据可以流经的任何程序伪像:

大多数数据流查询如下所示:

class RequestDataFlowConfiguration extends DataFlow::Configuration { 
  RequestDataFlowConfiguration() { this = "RequestDataFlowConfiguration" } 

  override predicate isSource(DataFlow::Node source) { 
    …
  }

  override predicate isSink(DataFlow::Node sink) { 
    …
  }

  override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { 
    …
  }

  override predicate isBarrier(DataFlow::Node node) { 
    …
  }

}
from DataFlow::Node source, DataFlow::Node sink 
where any(RequestDataFlowConfiguration c).hasFlow(source, sink) 
select 
  "Data flow from $@ to $@", 
  source, sink

请注意,在QL数据流库执行过程中,除了检查函数本地的数据流之外还将包括流经函数调用参数的数据。 这是我们的安全审查的一个基本功能。尽管下面讨论的漏洞代码模式在简单的示例函数中显示以便于演示,但在我们的目标的实际源代码中,大多数结果都有跨越多个复杂函数的数据流。

内存安全漏洞

由于此组件是纯C代码,我们首先决定搜索与内存安全相关的代码模式。

引起这种错误的一个常见原因是数组索引不执行边界检查。 单独搜索此模式将提供很大的帮助,这些结果很可能不是安全漏洞。 因此,在这种情况下,我们正在寻找数据流中的接收器是数组索引表达式,数据源是消息处理程序函数的请求数据,并且在由相关边界检查保护的数据流节点上存在障碍。

例如,我们想要找到匹配代码的数据流,如下所示:

int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
    ExampleMessageRequest* pMsgReq(3) = (ExampleMessageRequest *) pRequest(2);
    int index1(6) = pMsgReq(4)->index1(5);
    pTable1[index1(7:sink)].field1 = pMsgReq->value1;
}

但我们也希望排除代码的数据流,如下所示:

int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
    ExampleMessageRequest* pMsgReq(3) = (ExampleMessageRequest *) pRequest(2);
    int index2(6) = pMsgReq(4)->index2(5);
    if (index2 >= 0 && index2 < PTABLE_SIZE)
    {
        pTable2[index2].field1 = pMsgReq->value2;
    }
}

使用前面讨论的MessageHandlerFunction类定义源代码,我们可以使用ArrayExprgetArrayOffset谓词来定义合适的接收器:

override predicate isSource(DataFlow::Node source) {
    any(MessageHandlerFunction mhf).getRequestDataPointer() = source.asParameter()
  }

  override predicate isSink(DataFlow::Node sink) { 
    exists(ArrayExpr ae | ae.getArrayOffset() = sink.asExpr())  
  }

默认情况下,DataFlow库仅保留每个节点的值,例如函数调用参数,赋值表达式等。 但是我们还需要数据从请求数据指针流向它所投射到的结构的字段。 我们使用如下操作:

override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2)
  {
    // any terminal field access on request packet
    //   e.g. in expression a->b.c the data flows from a to c
    exists(Expr e, FieldAccess fa |  
      node1.asExpr() = e and node2.asExpr() = fa |  
      fa.getQualifier*() = e and not (fa.getParent() instanceof FieldAccess)
    )
  }

要使用边界检查排除数据,我们需要在控制流图中较早的在某些条件语句中使用变量或字段,并放置一些屏障。

override predicate isBarrier(DataFlow::Node node) { 
    exists(ConditionalStmt condstmt |  
      // dataflow node variable is used in expression of conditional statement
      //   this includes fields (because FieldAccess extends VariableAccess)
      node.asExpr().(VariableAccess).getTarget().getAnAccess()
                                          = condstmt.getControllingExpr().getAChild*()
      // and that statement precedes the dataflow node in the control flow graph
      and condstmt.getASuccessor+() = node.asExpr()
      // and the dataflow node itself not part of the conditional statement expression
      and not (node.asExpr() = cs.getControllingExpr().getAChild*())
    ) 
  }

将此应用于上述两个示例,每个节点的数据流将是:

在我们的代码库中,此查询在15个消息处理程序函数中共定位了18个漏洞,这是一组攻击者所控制的越界读写操作。

我们应用了类似的分析来查找函数调用的参数,并不验证消息请求数据。 首先,我们定义了一个QL类来定义函数调的用和参数,包括调用memcpy的大小参数和类似的函数_fmemcpy,以及CalculateChecksum的长度参数。 CalculateChecksum是一个特定的代码库函数,它将返回缓冲区的CRC32部分,并且可能被用作信息泄露。其中消息处理函数将此值复制到其响应缓冲区中。

class ArgumentMustBeCheckedFunctionCall extends FunctionCall {
  int argToCheck;

  ArgumentMustBeCheckedFunctionCall() {
    ( this.getTarget().hasName("memcpy")            and argToCheck = 2 ) or
    ( this.getTarget().hasName("_fmemcpy")          and argToCheck = 2 ) or
    ( this.getTarget().hasName("CalculateChecksum") and argToCheck = 1 )
  }
  Expr getArgumentToCheck() { result = this.getArgument(argToCheck) }
}

接下来,我们修改了上一个查询的接收器以匹配ArgumentMustBeCheckedFunctionCall而不是数组索引:

override predicate isSink(DataFlow::Node sink) {
    // sink node is an argument to a function call that must be checked first
    exists (ArgumentMustBeCheckedFunctionCall fc | 
              fc.getArgumentToCheck() = sink.asExpr())
  }

这个查询暴露出另外17个漏洞,其中大多数是攻击者控制的超出边界读取(我们后来证实在响应消息中已经披露了这些漏洞),其中一个超出边界写入。

污点跟踪

在上面的查询中,我们覆盖了DataFlow库的isAdditionalFlowStep谓词以确保数据流向指向结构的指针,该结构的字段将作为数据流图中的节点被添加。 在默认情况下,数据流分析仅包括数据值保持不变的路径,但我们希望跟踪可能受影响的表达式集合。 也就是说,我们定义了一组被不受信任的数据污染表达式。

QL包含一个内置库,可以应用更通用的方法来进行污点跟踪。 在DataFlow库之上开发,它会覆盖isAdditionalFlowStep,并为值修改表达式提供更丰富的规则集。 这就是TaintTracking库,它以类似于DataFlow的方式被导入:

import semmle.code.cpp.dataflow.TaintTracking

它的使用方式与数据库几乎相同,只是要扩展的QL类是TaintTracking::Configuration,这些配置谓词:

我们重新运行了先前的查询,删除了isAdditionalFlowStep并且将isBarrier重命名为isSanitizer。 正如预期的那样,它返回了上面提到的所有结果,但也在数组索引中发现了一些额外的整数下溢缺陷。 例如:

int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
    ExampleMessageRequest* pMsgReq(3) = (ExampleMessageRequest *) pRequest(2);
    int index1(6) = pMsgReq(4)->index1(5);
    pTable1[(index1(7) - 2)(8:sink)].field1 = pMsgReq->value1;
}

对于每个漏洞类型的内部报告,我们将这些与早期查询结果分开进行分类。 这包括使用SubExpr QL类对接收器进行简单修改:

override predicate isSink(DataFlow::Node sink) {
    // this sink is the left operand of a subtraction expression,
    //   which is part of an array offset expression, e.g. x in a[x - 1]
    exists(ArrayExpr ae, SubExpr s | sink.asExpr() instanceof FieldAccess
      and ae.getArrayOffset().getAChild*() = s
      and s.getLeftOperand().getAChild*() = sink.asExpr())
  }

这也暴露了其中2个消息处理函数中的另外3个漏洞。

查找路径遍历漏洞

为了找到潜在的路径来遍历漏洞,我们使用QL尝试识别文件所打开函数中的消息处理函数。

我们这次使用了不同的方法进行污点跟踪。此处我们定义了一些额外的污点步骤,这些步骤将流经各种字符串处理C库函数:

predicate isTaintedString(Expr expSrc, Expr expDest) {
  exists(FunctionCall fc, Function f |
    expSrc = fc.getArgument(1) and 
    expDest = fc.getArgument(0) and
    f = fc.getTarget() and (
      f.hasName("memcpy") or 
      f.hasName("_fmemcpy") or 
      f.hasName("memmove") or 
      f.hasName("strcpy") or 
      f.hasName("strncpy") or
      f.hasName("strcat") or
      f.hasName("strncat")
      )
  )
  or exists(FunctionCall fc, Function f, int n |
    expSrc = fc.getArgument(n) and 
    expDest = fc.getArgument(0) and
    f = fc.getTarget() and (
      (f.hasName("sprintf") and n >= 1) or 
      (f.hasName("snprintf") and n >= 2)
    )
  )
}
…

  override predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) {
    isTaintedString(node1.asExpr(), node2.asExpr())
  }

此处我们将接收器定义为文件打开功能的路径参数:

class FileOpenFunction extends Function {
  FileOpenFunction() {
    this.hasName("fopen") or this.hasName("open")
  }
  int getPathParameter() { result = 0 } // filename parameter index
}

…

  override predicate isSink(DataFlow::Node sink) {
    exists(FunctionCall fc, FileOpenFunction fof |
      fc.getTarget() = fof and fc.getArgument(fof.getPathParameter()) = sink.asExpr())
  }

在我们解决下一个排除数据验证流程的问题之前,我们对目标设备的工作模式进行了初步审查,我们发现其结果正如我们之前的查询的那样,查询根本没有返回任何内容。

由于没有检查的数据流路径,我们无法打开查询函数调用以搜索消息处理函数和调用文件打开函数之间的任何路径,不包括path参数为常量的调用:

// this recursive predicate defines a function call graph
predicate mayCallFunction(Function caller, FunctionCall fc) {
  fc.getEnclosingFunction() = caller or mayCallFunction(fc.getTarget(), fc)
}

from MessageHandlerFunction mhf, FunctionCall fc, FileOpenFunction fof
where mayCallFunction(mhf, fc)
  and fc.getTarget() = fof
  and not fc.getArgument(fof.getPathParameter()).isConstant()
select 
  mhf, "$@ may have a path to $@",
  mhf, mhf.toString(),
  fc, fc.toString()

这个查询提供了5个结果,从中我们发现了2个路径遍历漏洞,一个写入文件,另一个读取文件,两者都有攻击者提供的路径。 事实证明,污点跟踪没有标记这些,因为它需要发送两个单独的消息类型:第一个设置文件名,第二个读取或写入具有该名称的文件的数据。 然而QL足够灵活,可以提供另一种探索途径。

结论

在Microsoft,我们采取深度防御方法来保护云并保护客户的数据安全。 其中一个重要部分是对Azure内部攻击面进行全面的安全性审查。 在这个嵌入式设备的源代码审查中,我们应用Semmle QL的静态分析技术来查找基于消息的管理协议中的漏洞。 这在各种bug类中发现了总共33个易受攻击的消息处理程序。 使用QL使我们能够自动执行完全手动代码审查的重复部分,同时可以采用新型手段进行探测。

本文为翻译文章并来自:[https://blogs.technet.microsoft.com/srd/2019/03/19/vulnerability-hunting-with-semmle-ql-part-2/](https://blogs.technet.microsoft.com/srd/2019/03/19/vulnerability-hunting-with-semmle-ql-part-2/)
点击收藏 | 0 关注 | 1 打赏
  • 动动手指,沙发就是你的了!
登录 后跟帖