This is too brief to be called write-up. But I’m tired …

Introduction

I’ve participated in DEF CON CTF Qualifier 2018 as a member of a certain team, ignominious 40th place. But somehow I solved 3 tasks:

  • ELF Crumble
  • babypwn1805
  • elastic cloud compute (memory) corruption

I write down my impressions.

ELF Crumble

This is a task to combine and execute 8 binary fragments correctly. I wrote damn brute-force solver for this, 脳が死んでいるので.

babypwn1805

A blind pwn task. I accidentally found offset -0x38 to the GOT entry of read. Then I wrote the probabilistic solver.

elastic cloud compute (memory) corruption

A VM escape task.

We were given qemu-system-x86_64 binary with vulnerable PCI device namely ooo. Notable functions are as follows:

function description
sub_6E61F4 correspond to ooo_mmio_write
sub_6E613C correspond to ooo_mmio_read
sub_6E64A5 invokes system("cat ./flag")

What matters is use-after-free vulnerability in:

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
//----- (00000000006E61F4) ----------------------------------------------------
void __fastcall sub_6E61F4(__int64 opaque, __int64 addr, __int64 value, unsigned int size)
{
unsigned int cmd; // eax
...
*(_QWORD *)&n[4] = value;
cmd = ((unsigned int)addr & 0xF00000) >> 20;
switch ( cmd )
{
case 1u:
free(qword_1317940[((unsigned int)addr & 0xF0000) >> 16]);
break;
case 2u:
v12 = ((unsigned int)addr & 0xF0000) >> 16;
v8 = addr;
memcpy((char *)qword_1317940[v12] + (signed __int16)addr, &n[4], size);
break;
case 0u:
idx = ((unsigned int)addr & 0xF0000) >> 16;
if ( idx == 15 )
{
for ( i = 0; i <= 14; ++i )
qword_1317940[i] = malloc(8LL * *(_QWORD *)&n[4]);
}
else
{
qword_1317940[idx] = malloc(8LL * *(_QWORD *)&n[4]);
}
break;
}
}

With the clue of the chunk offset on 0x1317940, now we can overwrite malloc@GOT to sub_6E64A5 by fastbin attack, in particular using devmem.

I stayed up all night for this. I was tired but it was fun. I used these past write-ups as a reference when solving this task:

Thanks authors!

Final Words

Other tasks I had wanted to solve are:

  • flagsifier
  • TechSupport
  • smcauth

This year DEFCON’s organizer has changed from LegitBS to OOO (Order of the-Overflow). OOO seems to have the purpose of connecting academic research and CTF. I support this philosophy, but this competition was not perfect. My impressions are summarized as follows:

Pros Cons
Meritocratic rev/pwn. Brand-new topics i.e. blockchain, neural network, reversing of Rust binary. Many guessing tasks. Some incredible, old-fashioned tasks. In particular, sbva and ghettohackers: Throwback are quite bad.

Anyway, I’m looking forward to that next year.

HAI DOMO. This post is for 武蔵野 Advent Calendar 2017.

Introduction

In May this year, I just started my career as an apprentice security researcher at 武蔵野某所.One of my job responsibilities is to write a “good” paper that enough to be accepted to top-tier (non-crypto) security conferences like following:

  • IEEE S&P (Oakland)
  • ACM CCS
  • NDSS
  • USENIX Security

However, I am profoundly ignorant of cardinal rules of “good” security research and technical writing. ぜんぜんわからない.俺たちは雰囲気で研究をやっている.I thought I got to do something.

The joke paper entitled Paper Gestalt, distributed in CVPR’10, gave me a suggestion.

The key idea of the paper is that “good” paper might be distinguished by image recognition. だるくなってきた.時間がないので日本語で書きます.このジョーク論文では,論文を画像に変換,局所特徴量を抽出し,論文がトップカンファレンスにacceptされるかどうか判定する分類器が提案されている.仔細はPaper Gestalt - n_hidekeyの日記を参照されたい.かっこいい数式や図がある論文はそれっぽく見えてしまうよね,という話.

 そういうわけで,本稿ではPaper Gestaltを参考に,論文がセキュリティ系トップカンファレンスにacceptされるか判定する分類器を作成する.元論文ではAdaBoostを用いていたが,ここでは畳み込みニューラルネットを試す.

Dataset

 上述のカンファレンスにacceptされた論文4年分を正例,併設ワークショップにacceptされた論文同じく4年分をトップカンファレンスにrejectされた論文とみなして負例とする.負例には諸先輩方の論文が含まれていて,すみません,でもわかってくれると思うんです.

 さて一通りスクレイピングしたのち,ポスターやショートペーパーなど,4ページに満たないものを削除.キーノートやスライドも取り除く.重要なのはフルペーパーだからだ.結果,それぞれの論文数は以下の通り:

accepted rejected
1,266 794

 正例のワードクラウド:

 負例:

 なんもわからん.

Pre-processing

 論文PDFを画像化する.

 論文PDFの各ページを横に並べ,20ページに満たない場合は白紙で埋める処理を施した.例:

 見ての通り,USENIX系の本会議に通った論文にはかっこいい表紙が付いてくる.他の論文と体裁を合わせるため削除:

 3時間ほどかけて全PDFをImageMagickで画像化,訓練用・検証用に半々で分割.

Training

 今回はベンチマークということでLeNet-5をほぼそのまま使う.いつもいつも手書き文字を認識させられるなど過酷な拷問を受けているやつ.

 フレームワークはkeras. データが少数かつclass imbalancedであることを考慮して,Building powerful image classification models using very little dataに倣い,augmentationをかけながら訓練することにした.具体的にはズームと水平方向への反転.その他各種パラメータについてはありがちな構成を雰囲気で決めている:

活性化関数 損失関数 最適化手法 Dropout バッチサイズ エポック Early stopping
ReLU クロスエントロピー RMSProp 50% 64 100 validation accuracy

 本来ならネットワーク構成含め細かくチューニングすべきだが,手元のショボい計算機では投稿日までに計算が終わらなさそうだったため,hyperopt/hyperoptやそのkeras連携機能であるmaxpumperla/hyperasとか,そういったかっこいいテクニックは使っていない.すみません2.

Results

 Early stoppingが効いて16エポックで学習打ち止め.学習曲線:


 微妙.しかし自分が学生時代に国内研究会に投げた論文を投入したところ,

accepted rejected predict
7.3411% 92.6589% rejected

とまあ正しく判定できているっぽいのでよしとしましょう.なにが正しく判定だ.俺を,馬鹿にしているのか.いま,様々なものに対して害意を抱いています.Saliency mapの可視化とかは気が向いたら.

Final Words

 ACM CCS’17のWelcome Slidesにありがたいことばが載っている:

 つまりはそういうことです.小手先の浅知恵に逃げるものはなにをやってもだめ.やるぞ〜.

HAI DOMO. This post is for 武蔵野 Advent Calendar 2017 and also for CTF Advent Calendar 2017.

Introduction

In May this year, I participated in DEF CON CTF Qualifier 2017 as a member of a certain 武蔵野-related team. Actually, I’m not a top-tier CTF player, but I did my best and solved 4 challenges:

  • crackme1
  • beatmeonthedl
  • enlightenment
  • Pepperidge Farm

Write-ups already exist except for Pepperidge Farm. So I decided to write about it. FYI: The binaries are available at legitbs/quals-2017.

Pepperidge Farm

Pepperidge Farm is categorized into Reverse Engineering. The problem statement is below:

Remember when the first CTF was run with a custom architecture? Pepperidge Farm remembers:
https://github.com/JonathanSalwan/VMNDH-2k12

pepperidge-farm_edb4ad2f103a9efde038346d2cd86a1e.quals.shallweplayaga.me:2012

Files
https://2017.notmalware.ru/8a45cf7171e89594cfd1d51671fef0bec3f24d9d/pepperidge_farm

It seems like a keygenning challenge on the custom virtual machine–VMNDH-2k12.

1
2
3
$ ./vmndh -file pepperidge_farm
Enter your registration code: 31337
Code does not match any known registered users

VMNDH-2k12

VMNDH-2k12 is the VM built for Nuit du Hack CTF Quals 2012 as its name suggests. The architecture is described in shell-storm | Useless emulator for fun (VMNDH-2k12). This VM parses given serialized binary and repeats fetch, decode and execution.

Writing IDA loader/processor module is a common way to analyze VM-based obfuscated binary. The modules for VMNDH-2k12 and for modified version VMNDH-2k13 already exist:

Note that when you try to solve this challenge with above-mentioned processor modules with IDA Pro 7.0, the backward-compatibility issue will occur. For example, you have to change self.regFirstSreg toself.reg_first_sreg in a module.

Also, the Binary Ninja plugin has been released after quals:

But in this post, I describe a solution without both IDA Pro and Binary Ninja. Because VMNDH-2k12 is open-sourced and easy to modify.

Surface Analysis

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
$ ./vmndh -debug -file pepperidge_farm
[Console]#> help
<enter> Execute next instruction
run Run program
bp <addr> Set breakpoint
info bp Display info breakpoint
info reg Display registers
show sp Display SP memory
show pc Display PC memory
dis <addr>:<size> Disassembly X bytes from ADDR
x/x <addr>:<size> Print X bytes from ADDR
x/s <addr> Print string addr
set reg=value Set value in register
syscall Execute 'syscall' instruction
help Display this help
quit Quit console debugging
[Console]#> dis
Error: Set addr between 0x8000 and 0x882a
[Console]#> dis 0x8000:82a
0x8000: jmpl 0x0720
0x8003: push r2
0x8007: .byte 0x00
0x8008: nop
...

Yes, the VM has own debugger and disassembler.

Modifying The Disassembler

However, there are pitfalls here.

Because it is a unique architecture, the destination of the control flow instructions are different from it shown on the disassembly dump. For example, take a look at src_vm/op_call.c:

1
2
3
4
5
6
7
8
9
10
11
12
static void op_call_dir16(void)
{
uint16_t operande;
operande = *(uint16_t *)(core.memory.vmem + core.memory.pc + 2);
if (core.flagmode.noverbose == 0)
fprintf(stdout, "%s0x%4.x%s > call 0x%.2x\n", RED, core.memory.pc, ENDC, operande);
core.memory.sp -= 2; /* sub sp */
*(uint16_t *)(core.memory.vmem + core.memory.sp) = core.memory.pc + 4;
core.memory.pc = core.memory.pc + operande + 4;
}

Acording to this, I modified the dissassembler in src_vm/disass.c:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
@@ -532,6 +537,7 @@
uint16_t operande;
uint8_t reg;
char flag;
+ uint16_t dst;
flag = *(core.memory.vmem + addr + 1);
switch (flag)
@@ -543,7 +549,8 @@
case OP_FLAG_DIRECT16:
operande = *(uint16_t *)(core.memory.vmem + addr + 2);
- fprintf(stdout, "%s0x%.4x%s: call 0x%.4x\n", RED, addr, ENDC, operande);
+ dst = addr + operande + 4;
+ fprintf(stdout, "%s0x%.4x%s: call 0x%.4x\n", RED, addr, ENDC, dst);
return (addr + 4);
default:

This makes it possible to correctly display the address of the call destination in the disassembly dump. In addition, jump instructions need to be modified. In the case of jnz:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
@@ -463,10 +470,11 @@
static uint16_t dis_jnz(uint16_t addr)
{
- uint16_t operande;
+ uint16_t operande, dst;
operande = *(uint16_t *)(core.memory.vmem + addr + 1);
- fprintf(stdout, "%s0x%.4x%s: jnz 0x%.4x\n", RED, addr, ENDC, operande);
+ dst = addr + operande + 3;
+ fprintf(stdout, "%s0x%.4x%s: jnz 0x%.4x\n", RED, addr, ENDC, dst);
return (addr + 3);
}

Herewith,

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
0x86a1: jnz 0x0076
0x86a4: mov r0, r2
0x86a8: call 0xfdc5
0x86ac: test r0, r0
0x86af: jnz 0x0068
0x86b2: mov r0, r2
0x86b6: call 0xfddf
0x86ba: test r0, r0
0x86bd: jnz 0x005a
0x86c0: mov r0, r2
0x86c4: call 0xfe17
0x86c8: test r0, r0
0x86cb: jnz 0x004c
0x86ce: mov r0, r2
0x86d2: call 0xfe2c
0x86d6: test r0, r0
...

becomes:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
0x86a1: jnz 0x871a
0x86a4: mov r0, r2
0x86a8: call 0x8471
0x86ac: test r0, r0
0x86af: jnz 0x871a
0x86b2: mov r0, r2
0x86b6: call 0x8499
0x86ba: test r0, r0
0x86bd: jnz 0x871a
0x86c0: mov r0, r2
0x86c4: call 0x84df
0x86c8: test r0, r0
0x86cb: jnz 0x871a
0x86ce: mov r0, r2
0x86d2: call 0x8502
0x86d6: test r0, r0
...

Good.

Also, after 0x8759 it looks like a data section.

1
2
3
4
5
6
0x8759: .byte 0x45 (E)
0x875a: .byte 0x6e (n)
0x875b: .byte 0x74 (t)
0x875c: .byte 0x65 (e)
0x875d: .byte 0x72 (r)
...

However, parts such as 0x87e8 are misinterpreted as codes.

1
0x87e8: inc r82

The data section was not obfuscated.

1
2
3
4
5
00007e0: 6c61 6700 3ce3 5a9e 9113 8c05 e42e 0a52 lag.<.Z........R
00007f0: 3dd8 7cf5 9f4b 9f06 d7a8 e9a0 a636 a649 =.|..K.......6.I
0000800: 3136 9308 eb70 ebbf df28 500d 7be8 96fa 16...p...(P.{...
0000810: e8b7 a5df c24d f0b8 3b78 6272 b748 1697 .....M..;xbr.H..
0000820: f019 2d6b 085b 9f94 4987 e624 3752 efb8 ..-k.[..I..$7R..

So I gave first aid to src_vm/disass.c:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
@@ -322,8 +322,15 @@
static uint16_t dis_inc(uint16_t addr)
{
uint8_t operande;
+ char OP, OP2;
+ OP = *(core.memory.vmem + addr);
+ OP2 = *(core.memory.vmem + addr + 1);
operande = *(core.memory.vmem + addr + 1);
+ if(addr > 0x8759)
+ fprintf(stdout, "%s0x%.4x%s: [DEBUG] .byte 0x%.2x\n", RED, addr, ENDC, (unsigned char)OP);
+ fprintf(stdout, "%s0x%.4x%s: [DEBUG] .byte 0x%.2x\n", RED, addr + 1, ENDC, (unsigned char)OP2);
+
fprintf(stdout, "%s0x%.4x%s: inc r%d\n", RED, addr, ENDC, operande);
return (addr + 2);

Awful… who cares?

1
2
3
4
0x87e8: [DEBUG] .byte 0x0a
0x87e9: [DEBUG] .byte 0x52
0x87e8: inc r82
0x87ea: .byte 0x3d (=)

First Attempt with KLEE

This is a failure case.

As we have seen so far, VMNDH-2k12 is open-sourced. So I tried to solve the challenge with source code-based symbolic execution tool–KLEE.

I modified src_vm/syscall_write.c for assertion:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
@@ -18,6 +18,8 @@
*/
#include "vmndh.h"
+#include <klee/klee.h>
+#include <string.h>
void syscall_write(void)
{
@@ -32,7 +34,12 @@
if (core.flagmode.noverbose == 0)
write(1, txt, strlen(txt));
+
+ if (strstr(arg2, "Thank") != NULL)
+ klee_assert(0);
+
core.regs.r0 = write(arg1, arg2, arg3);
+
if (core.flagmode.noverbose == 0)
write(1, "\n", 1);
}

Here is a modified Makefile:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
@@ -17,14 +17,15 @@
## Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
##
-DEBUG = no
+DEBUG = yes
RM = rm -f
INCLUDE = ./includes
SRC_DIR = ./src_vm
+KLEE_PATH = ../klee_src/include
NAME = vmndh
ifeq ($(DEBUG),yes)
- CFLAGS = -c -ggdb3 -Wextra -Wall -D _BSD_SOURCE -I$(INCLUDE)
+ CFLAGS = -c -ggdb3 -Wextra -Wall -D _BSD_SOURCE -I$(INCLUDE) -I$(KLEE_PATH) -emit-llvm -g
LDFLAGS =
CC = clang
else

I’d left all of it to KLEE and get to bed…

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
$ make
$ llvm-link src_vm/*.o -o vmndh.bc
$ klee --optimize --emit-all-errors --libc=uclibc --write-smt2s --posix-runtime vmndh.bc -file pepperidge_farm -sym-stdin 65
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/VMNDH-2k12/klee-out-1"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "__user_main" has inline asm
KLEE: WARNING ONCE: function "syscall_accept" has inline asm
KLEE: WARNING ONCE: function "syscall_bind" has inline asm
KLEE: WARNING ONCE: function "syscall_listen" has inline asm
KLEE: WARNING ONCE: function "syscall_recv" has inline asm
KLEE: WARNING ONCE: function "syscall_send" has inline asm
KLEE: WARNING ONCE: function "syscall_socket" has inline asm
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 44258832) at /home/klee/klee_src/runtime/POSIX/fd.c:1044
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
Enter your registration code: KLEE: WARNING ONCE: calling external: vprintf(57126208, 46345808) at /home/klee/klee_build/klee-uclibc/libc/stdio/fprintf.c:36
[SYSCALL output]: 64
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
...
KLEE: WARNING: killing 175 states (over memory cap)
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
...
Code does not match any known registered users
KLEE: done: total instructions = 5117896332
KLEE: done: completed paths = 81092
KLEE: done: generated tests = 81092

… It’s not going to be easy.

I also wrote solver with angr. Which symbolizes stdin, but… let’s not talk about it.

An example of insufficient SMTLIB2 representations is:

1
2
3
4
5
6
7
(set-logic QF_AUFBV )
(declare-fun model_version () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun stdin () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun stdin-stat () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (select stdin (_ bv25 32) ) ) (?B2 (select stdin (_ bv31 32) ) ) (?B3 (select stdin (_ bv18 32) ) ) (?B4 (select stdin (_ bv40 32) ) ) (?B5 (select stdin (_ bv36 32) ) ) (?B6 (select stdin (_ bv23 32) ) ) (?B7 (select stdin (_ bv27 32) ) ) (?B8 (select stdin (_ bv33 32) ) ) (?B9 (select stdin (_ bv6 32) ) ) (?B10 (select stdin (_ bv8 32) ) ) ) (let ( (?B13 ((_ zero_extend 16) ((_ zero_extend 8) ?B7 ) ) ) (?B14 ((_ zero_extend 16) ((_ zero_extend 8) ?B8 ) ) ) (?B12 ((_ zero_extend 16) ((_ zero_extend 8) ?B2 ) ) ) (?B11 ((_ zero_extend 16) ((_ zero_extend 8) ?B1 ) ) ) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= false (= (_ bv0 64) (bvand (concat (select stdin-stat (_ bv15 32) ) (concat (select stdin-stat (_ bv14 32) ) (concat (select stdin-stat (_ bv13 32) ) (concat (select stdin-stat (_ bv12 32) ) (concat (select stdin-stat (_ bv11 32) ) (concat (select stdin-stat (_ bv10 32) ) (concat (select stdin-stat (_ bv9 32) ) (select stdin-stat (_ bv8 32) ) ) ) ) ) ) ) ) (_ bv2147483647 64) ) ) ) (bvult (concat (select stdin-stat (_ bv63 32) ) (concat (select stdin-stat (_ bv62 32) ) (concat (select stdin-stat (_ bv61 32) ) (concat (select stdin-stat (_ bv60 32) ) (concat (select stdin-stat (_ bv59 32) ) (concat (select stdin-stat (_ bv58 32) ) (concat (select stdin-stat (_ bv57 32) ) (select stdin-stat (_ bv56 32) ) ) ) ) ) ) ) ) (_ bv65536 64) ) ) (= (_ bv1 32) (concat (select model_version (_ bv3 32) ) (concat (select model_version (_ bv2 32) ) (concat (select model_version (_ bv1 32) ) (select model_version (_ bv0 32) ) ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv0 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv1 32) ) ) ) (= (_ bv57 8) (select stdin (_ bv2 32) ) ) ) (= (_ bv70 8) (select stdin (_ bv3 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv4 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv5 32) ) ) ) (= false (= (_ bv48 8) ?B9 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B9 ) ) ) ) ) (= false (= (_ bv48 8) ?B10 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B10 ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv12 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv13 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv14 32) ) ) ) (= (_ bv57 8) (select stdin (_ bv15 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv16 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv17 32) ) ) ) (= false (= (_ bv48 8) ?B3 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B3 ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv20 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv21 32) ) ) ) (= (_ bv57 8) (select stdin (_ bv22 32) ) ) ) (= false (= (_ bv48 8) ?B6 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B6 ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv24 32) ) ) ) (= false (= (_ bv48 8) ?B1 ) ) ) (bvult (_ bv48 32) ?B11 ) ) (= false (= (_ bv57 8) ?B1 ) ) ) (= false (bvult (_ bv57 32) ?B11 ) ) ) (= (_ bv48 8) (select stdin (_ bv26 32) ) ) ) (= false (= (_ bv48 8) ?B7 ) ) ) (bvult (_ bv48 32) ?B13 ) ) (= false (= (_ bv57 8) ?B7 ) ) ) (= false (bvult (_ bv57 32) ?B13 ) ) ) (= (_ bv48 8) (select stdin (_ bv28 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv29 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv30 32) ) ) ) (= false (= (_ bv48 8) ?B2 ) ) ) (bvult (_ bv48 32) ?B12 ) ) (= false (= (_ bv57 8) ?B2 ) ) ) (= false (bvult (_ bv57 32) ?B12 ) ) ) (= (_ bv48 8) (select stdin (_ bv32 32) ) ) ) (= false (= (_ bv48 8) ?B8 ) ) ) (bvult (_ bv48 32) ?B14 ) ) (= false (= (_ bv57 8) ?B8 ) ) ) (bvult (_ bv57 32) ?B14 ) ) (= false (= (_ bv70 8) ?B8 ) ) ) (bvult (_ bv70 32) ?B14 ) ) (= false (= (_ bv48 8) ?B5 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B5 ) ) ) ) ) (= false (= (_ bv48 8) ?B4 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B4 ) ) ) ) ) ) ) )
(check-sat)
(exit)

Solution with Z3

Since there is no choice, I read all the disassembly. After some twists and turn, I realized that:

  • Pepperidge Farm checks character codes against transformed 0x20 bytes values.
  • 0x8247(x, y) returns x * 100 + y.

Now Z3 time. For example, subroutine 0x8269:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
0x8269: push r1
0x826d: pop r2
0x826f: mov r7, r0
0x8273: addb r0, #00
0x8277: call 0x8247
0x827b: mov r1, r0
0x827f: mov r0, r7
0x8283: addb r0, #14
0x8287: call 0x8247
0x828b: mov r2, r0
0x828f: movl r0, #0x87ec
0x8294: call 0x8247
0x8298: xorl r1, #4936
0x829d: add r1, r2
0x82a1: xor r0, r1
0x82a5: pop r2
0x82a7: pop r1
0x82a9: ret
...
0x87ec: .byte 0x7c (|)
0x87ed: .byte 0xf5

becomes:

1
s.add(((sub_8247(0) ^ 0x4936) + sub_8247(0x14)) ^ 0x7cf5 == 0)

This is satisfiable. But not enough. We need to add rest of constraints.

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
#!/usr/bin/env python
#coding: utf-8
import telnetlib, sys
from z3 import *
REMOTE = len(sys.argv) >= 2 and sys.argv[1] == 'r'
if REMOTE:
host = 'pepperidge-farm_edb4ad2f103a9efde038346d2cd86a1e.quals.shallweplayaga.me'
port = 2012
else:
host = '127.0.0.1'
port = 4000
values = [BitVec('x%d' % i, 8) for i in range(0x20)]
def sub_8247(x): return ZeroExt(8, values[x]) << 8 | ZeroExt(8, values[x + 1])
s = Solver()
# sub_8269
s.add(((sub_8247(0) ^ 0x4936) + sub_8247(0x14)) ^ 0x7cf5 == 0)
# sub_82aa
s.add(sub_8247(6) * sub_8247(8) * (sub_8247(2) ^ 0xfdf) ^ 0x3dd8 == 0)
# sub_8304
s.add(((sub_8247(4) ^ 0xc7df) + sub_8247(0xe) * sub_8247(0xc)) ^ 0xeb70 == 0)
# sub_835e
s.add(((sub_8247(6) ^ 0xc5db) + 0x14aa) ^ 0x500d == 0)
# sub_838b
s.add(sub_8247(8) * sub_8247(0x1e) ^ 0x7be8 == 0)
# sub_83c7
s.add((sub_8247(0xa) + sub_8247(6) + sub_8247(0xC)) ^ 0xdf28 == 0)
# sub_841c
s.add(((sub_8247(0xC) + 0x5432) | 0x3008) ^ 0x3b78 == 0)
# sub_8449
s.add((sub_8247(0xE) + 0x1212) ^ 0x1697 == 0)
# sub_8471
s.add((sub_8247(0x10) ^ 0x8703) ^ 0x3136 == 0)
# sub_8499
s.add(((sub_8247(0x12) + 0x4004) + (sub_8247(0x14) ^ 0xA52)) ^ 0x6272 == 0)
# sub_84df
s.add()
# sub_8502
s.add((sub_8247(0x16) + sub_8247(0x10)) ^ 0x9308 == 0)
# sub_853e
s.add(sub_8247(0x18) ^ 0x085b == 0)
# sub_8561
s.add(((sub_8247(0x1a) ^ 0x863c) + 0x1234) ^ 0x9113 == 0)
# sub_858e
s.add((sub_8247(0x1c) + sub_8247(8) + sub_8247(0x12)) ^ 0xf0b8 == 0)
# sub_85e3
s.add(((sub_8247(0x1e) & 0x0f00) + sub_8247(0)) ^ 0x9f94 == 0)
print s.check()
print s.model()
input = ''
for i in range(0x20):
try:
input += '%02x' % s.model()[values[i]].as_long()
except:
input += '??'
input = input.upper()
print input
t = telnetlib.Telnet(host, port)
t.write(input + '\n')
t.interact()

Even with halfway constraints, the process proceeds. So inscount with Pin or other dynamic binary instrumentation tools might be helpful.

Finally I got:

1
2
3
4
Enter your registration code: 90940C6017E5FEB82083F932E73E0485B635796DA353DCD3085BF8E356C87FF8
Thank you for your patronage!
Your username is: pepperidge
This is the flag: th0s3_wh0_l0ok_0nly_to_th3_p4stur3_ar3_cert4in_t0_miss_th3_futur3

The conclusive SMTLIB2 representation is:

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
; benchmark
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun x1 () (_ BitVec 8))
(declare-fun x0 () (_ BitVec 8))
(declare-fun x31 () (_ BitVec 8))
(declare-fun x30 () (_ BitVec 8))
(declare-fun x19 () (_ BitVec 8))
(declare-fun x18 () (_ BitVec 8))
(declare-fun x9 () (_ BitVec 8))
(declare-fun x8 () (_ BitVec 8))
(declare-fun x29 () (_ BitVec 8))
(declare-fun x28 () (_ BitVec 8))
(declare-fun x27 () (_ BitVec 8))
(declare-fun x26 () (_ BitVec 8))
(declare-fun x25 () (_ BitVec 8))
(declare-fun x24 () (_ BitVec 8))
(declare-fun x17 () (_ BitVec 8))
(declare-fun x16 () (_ BitVec 8))
(declare-fun x23 () (_ BitVec 8))
(declare-fun x22 () (_ BitVec 8))
(declare-fun x21 () (_ BitVec 8))
(declare-fun x20 () (_ BitVec 8))
(declare-fun x15 () (_ BitVec 8))
(declare-fun x14 () (_ BitVec 8))
(declare-fun x13 () (_ BitVec 8))
(declare-fun x12 () (_ BitVec 8))
(declare-fun x7 () (_ BitVec 8))
(declare-fun x6 () (_ BitVec 8))
(declare-fun x11 () (_ BitVec 8))
(declare-fun x10 () (_ BitVec 8))
(declare-fun x5 () (_ BitVec 8))
(declare-fun x4 () (_ BitVec 8))
(declare-fun x3 () (_ BitVec 8))
(declare-fun x2 () (_ BitVec 8))
(assert
(let ((?x206 (bvand (bvor (bvshl ((_ zero_extend 8) x30) (_ bv8 16)) ((_ zero_extend 8) x31)) (_ bv3840 16))))
(let ((?x209 (bvxor (bvadd ?x206 (bvor (bvshl ((_ zero_extend 8) x0) (_ bv8 16)) ((_ zero_extend 8) x1))) (_ bv40852 16))))
(let (($x210 (= ?x209 (_ bv0 16))))
(let ((?x82 (bvor (bvshl ((_ zero_extend 8) x8) (_ bv8 16)) ((_ zero_extend 8) x9))))
(let ((?x200 (bvadd (bvor (bvshl ((_ zero_extend 8) x28) (_ bv8 16)) ((_ zero_extend 8) x29)) ?x82)))
(let ((?x201 (bvadd ?x200 (bvor (bvshl ((_ zero_extend 8) x18) (_ bv8 16)) ((_ zero_extend 8) x19)))))
(let (($x204 (= (bvxor ?x201 (_ bv61624 16)) (_ bv0 16))))
(let ((?x190 (bvxor (bvor (bvshl ((_ zero_extend 8) x26) (_ bv8 16)) ((_ zero_extend 8) x27)) (_ bv34364 16))))
(let (($x195 (= (bvxor (bvadd ?x190 (_ bv4660 16)) (_ bv37139 16)) (_ bv0 16))))
(let ((?x183 (bvxor (bvor (bvshl ((_ zero_extend 8) x24) (_ bv8 16)) ((_ zero_extend 8) x25)) (_ bv2139 16))))
(let (($x184 (= ?x183 (_ bv0 16))))
(let ((?x174 (bvadd (bvor (bvshl ((_ zero_extend 8) x22) (_ bv8 16)) ((_ zero_extend 8) x23)) (bvor (bvshl ((_ zero_extend 8) x16) (_ bv8 16)) ((_ zero_extend 8) x17)))))
(let (($x177 (= (bvxor ?x174 (_ bv37640 16)) (_ bv0 16))))
(let ((?x165 (bvxor (bvor (bvshl ((_ zero_extend 8) x20) (_ bv8 16)) ((_ zero_extend 8) x21)) (_ bv2642 16))))
(let ((?x163 (bvadd (bvor (bvshl ((_ zero_extend 8) x18) (_ bv8 16)) ((_ zero_extend 8) x19)) (_ bv16388 16))))
(let (($x169 (= (bvxor (bvadd ?x163 ?x165) (_ bv25202 16)) (_ bv0 16))))
(let ((?x154 (bvxor (bvor (bvshl ((_ zero_extend 8) x16) (_ bv8 16)) ((_ zero_extend 8) x17)) (_ bv34563 16))))
(let (($x157 (= (bvxor ?x154 (_ bv12598 16)) (_ bv0 16))))
(let ((?x145 (bvadd (bvor (bvshl ((_ zero_extend 8) x14) (_ bv8 16)) ((_ zero_extend 8) x15)) (_ bv4626 16))))
(let (($x148 (= (bvxor ?x145 (_ bv5783 16)) (_ bv0 16))))
(let ((?x107 (bvor (bvshl ((_ zero_extend 8) x12) (_ bv8 16)) ((_ zero_extend 8) x13))))
(let (($x143 (= (bvxor (bvor (bvadd ?x107 (_ bv21554 16)) (_ bv12296 16)) (_ bv15224 16)) (_ bv0 16))))
(let ((?x78 (bvor (bvshl ((_ zero_extend 8) x6) (_ bv8 16)) ((_ zero_extend 8) x7))))
(let ((?x132 (bvadd (bvor (bvshl ((_ zero_extend 8) x10) (_ bv8 16)) ((_ zero_extend 8) x11)) ?x78)))
(let (($x136 (= (bvxor (bvadd ?x132 ?x107) (_ bv57128 16)) (_ bv0 16))))
(let ((?x124 (bvmul ?x82 (bvor (bvshl ((_ zero_extend 8) x30) (_ bv8 16)) ((_ zero_extend 8) x31)))))
(let (($x127 (= (bvxor ?x124 (_ bv31720 16)) (_ bv0 16))))
(let (($x119 (= (bvxor (bvadd (bvxor ?x78 (_ bv50651 16)) (_ bv5290 16)) (_ bv20493 16)) (_ bv0 16))))
(let ((?x108 (bvmul (bvor (bvshl ((_ zero_extend 8) x14) (_ bv8 16)) ((_ zero_extend 8) x15)) ?x107)))
(let ((?x109 (bvadd (bvxor (bvor (bvshl ((_ zero_extend 8) x4) (_ bv8 16)) ((_ zero_extend 8) x5)) (_ bv51167 16)) ?x108)))
(let (($x112 (= (bvxor ?x109 (_ bv60272 16)) (_ bv0 16))))
(let ((?x90 (bvmul (bvmul ?x78 ?x82) (bvxor (bvor (bvshl ((_ zero_extend 8) x2) (_ bv8 16)) ((_ zero_extend 8) x3)) (_ bv4063 16)))))
(let (($x93 (= (bvxor ?x90 (_ bv15832 16)) (_ bv0 16))))
(let ((?x50 (bvadd (bvxor (bvor (bvshl ((_ zero_extend 8) x0) (_ bv8 16)) ((_ zero_extend 8) x1)) (_ bv18742 16)) (bvor (bvshl ((_ zero_extend 8) x20) (_ bv8 16)) ((_ zero_extend 8) x21)))))
(let (($x54 (= (bvxor ?x50 (_ bv31989 16)) (_ bv0 16))))
(and $x54 $x93 $x112 $x119 $x127 $x136 $x143 $x148 $x157 $x169 $x177 $x184 $x195 $x204 $x210)))))))))))))))))))))))))))))))))))))
(check-sat)

Final Words

I enjoyed this challenge. It seems to be easy or medium-easy difficulty rating. If only I could have solved more difficult Reverse Engineering challenges during quals–liberty, godzilla, and so on.

Recently I read T. Blazytko et al. USENIX Security’17. The paper says the system named Syntia automatically deobfuscate binaries with program synthesis. Program synthesis is a method to synthesize some pieces of program from given I/O samples and possible operators–like this:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
#!/usr/bin/env python
#coding: utf-8
from z3 import *
x, y, h = BitVecs(['x', 'y', 'h'], 8)
# I/O samples
t1 = And(x == 1, y == 2)
t2 = And(x == 2, y == 4)
t3 = And(x == 3, y == 6)
phi_1 = Or(t1, t2, t3)
# h is subject to synthesize
phi_2 = y == x << h
s = Solver()
s.add(ForAll([x, y], Implies(phi_1, phi_2)))
print s.check() # sat
print s.model() # [h = 2]

This is just a simple example. In practical, program slicing and path pruning will be needed. Both symbolic execution and program synthesis depend on SMT solver, but according to the paper, program synthesis is more suitable for deobfuscation tasks… really? I’ll investigate further.

This post is for Honeypot Advent Calendar 2017.

Introduction

In May this year, Trend Micro researchers have announced interesting research results in the article titled Red on Red: The Attack Landscape of the Dark Web - TrendLabs Security Intelligence Blog. They had deployed a honeypot on the dark web and monitored attack activities. They’ve done great work, indeed.

Well then, with the aid of the screenshot in that article, probably I found the honeypot. May I introduce the how and why?

Dark Web OSINT

In March this year, when they would have created an presentation slide, I have been running the crawler for the dark web. My purpose was to create a pictorial book of Tor hidden services below:

The crawler is simple, just like saying “Hello, world!” to PhantomJS. It has only capability of taking a screenshot.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
service_args = [
# Do not insert blank to each of args.
'--proxy=127.0.0.1:9050',
'--proxy-type=socks5'
]
dcap = {
'phantomjs.page.settings.userAgent': 'Mozilla/5.0 (Windows NT 6.1; rv:31.0) Gecko/20100101 Firefox/31.0'
}
def get_title_with_screenshot(url):
driver = webdriver.PhantomJS(service_args = service_args, desired_capabilities = dcap)
driver.set_window_size(1024, 512)
driver.get('http://' + url + '.onion') # 'http://' is required.
driver.save_screenshot(url + '.png')
title = driver.title
driver.close()
return title

I have discovered 40,208 onion domains and confirmed 1,797 domains were active.

Image Processing

Thanks to collecting screenshots by chance, I was able to find a site similar to the screenshot in their article–with histgram calculation:

1
2
3
4
5
6
7
8
9
10
11
12
list = glob.glob('./images/*.png')
def cbir():
target_im = cv2.imread(sys.argv[1])
target_hist = cv2.calcHist([target_im], [0], None, [256], [0, 256])
for i in list:
comparing_im = cv2.imread(i)
comparing_hist = cv2.calcHist([comparing_im], [0], None, [256], [0, 256])
diff = cv2.compareHist(target_hist, comparing_hist, 0)
if diff > float(sys.argv[2]): # Threshold
print i, diff

Yet domain names are not posted in their articles, I believe this is it.

1
2
3
4
$ wget http://blog.trendmicro.com/trendlabs-security-intelligence/files/2017/05/red-on-red-1.jpg
$ cbir.py red-on-red-1.jpg
$ python cbir.py red-on-red-1.jpg 0.9
./images/s5**********jlp2.png 0.979927357262

The screenshot:

There are many clone sites in the dark web–for backup, or even for spying? s5**********jlp2.onion might be cloned and have maintained by others. Even in that case, the site is likely to be a honeypot.

Interestingly, I also found some posts like to induce to the site at r/onions. I believe these are done by researcher.

Last Words

We got a glimpse of deep in abyss. This is just an accidental case study. Needless to say, no insult intended.

My crawler and image processing scripts are available at ntddk/onionstack. Crawling of the dark web is accompanied by risk. After all, with ethical considerations, I’ve deleted screenshots I’d captured except for the honeypot.

If you interested in the dark web OSINT, Dark Web | Automating OSINT Blog will be a good starting point.

Anyway, keep safety.

Introduction

As you know, IDAPython is quite useful. And Triton concolic execution engine has python binding. Then… why not integrate them? I tried to stand on the shoulders of giants.

Backward Program Slicing

Roughly speaking, program slicing is a method to extract subset of program which is relevant to given statement. Here is an excerpt from M. Weiser. ICSE’81:

Starting from a subset of a program’s behavior, slicing reduces that program to a minimal form which still produces that behavior. The reduced program, called a “slice”, is an independent program guaranteed to faithfully represent the original program within the domain of the specified subset of behavior.

Kudos to Jonathan Salwan, we can easily apply backward program slicing to binary analysis process with minor modification of backward_slicing.py and proving_opaque_predicates.py. I wrote a simple, tiny glue between Triton and IDA Pro:

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
#!/usr/bin/env python
#coding: utf-8
from idc import *
from idaapi import *
from triton import *
ctx = TritonContext()
regs = {
'eax': REG.X86.EAX,
'ebx': REG.X86.EBX,
'ecx': REG.X86.ECX,
'edx': REG.X86.EDX,
}
def symbolization_init():
ctx.convertRegisterToSymbolicVariable(ctx.registers.eax)
ctx.convertRegisterToSymbolicVariable(ctx.registers.ebx)
ctx.convertRegisterToSymbolicVariable(ctx.registers.ecx)
ctx.convertRegisterToSymbolicVariable(ctx.registers.edx)
return
def opaque_predicate_detection(pc):
ctx.setArchitecture(ARCH.X86)
ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)
symbolization_init()
ast_ctx = ctx.getAstContext()
while True:
instruction = Instruction()
instruction.setAddress(pc)
opcode = GetManyBytes(pc, ItemSize(pc)) # Disassemble with IDA Pro
instruction.setOpcode(opcode)
ctx.processing(instruction) # Emulate instruction without Pintool
for se in instruction.getSymbolicExpressions():
se.setComment(str(instruction))
if str(instruction.getDisassembly()).split()[0] == 'cmp': # if instruction.isCompare():
reg = str(instruction.getOperands()[0]).split(':')[0] # Get first operand
if reg in regs:
Expr = ctx.getSymbolicRegisters()[regs[reg]]
slicing = ctx.sliceExpressions(Expr)
for k, v in sorted(slicing.items()):
print v.getComment()
print instruction
elif instruction.isBranch():
print instruction
if instruction.isConditionTaken():
print 'branch will taken'
else:
print 'branch will not taken'
break
pc = NextHead(pc)
print '-' * 50
def main():
ea = ScreenEA() # Get address corresponding to cursor
opaque_predicate_detection(ea)
if __name__ == '__main__':
view = main()

Showcase

The snippet extracts subset of program which is relevant to branch condition. We can run this from File -> Script file in IDA Pro menu.

Conditional Branch

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
.text:004074DD loc_4074DD:
.text:004074DD 040 mov dword ptr [edi+18h], 0Ah
.text:004074E4 040 mov dword ptr [edi+14h], 0
.text:004074EB 040 mov word ptr [edi+8], 8235h
.text:004074F1 040 mov dword ptr [edi+0Ch], 3E8h
.text:004074F8 040 mov dword ptr [edi+10h], 0BB8h
.text:004074FF 040 sub esp, 4
.text:00407502 044 mov [esp+40h+Memory], 0B8h ; Size ; cursor
.text:00407509 044 call ??2@YAPAXI@Z ; operator new(uint)
.text:0040750E 044 add esp, 4
.text:00407511 040 mov [esi+18h], eax
.text:00407514 040 mov eax, dword_591EE4
.text:00407519 040 mov ecx, dword_591EE0
.text:0040751F 040 imul eax, eax
.text:00407522 040 imul edx, eax, 7
.text:00407525 040 dec edx
.text:00407526 040 mov eax, ecx
.text:00407528 040 imul eax, eax
.text:0040752B 040 cmp edx, eax
.text:0040752D 040 jz short loc_407538

becomes:

1
2
3
4
5
6
7
0x407514: mov eax, dword ptr [0x591ee4]
0x40751f: imul eax, eax
0x407522: imul edx, eax, 7
0x407525: dec edx
0x40752b: cmp edx, eax
0x40752d: je 0x407538
branch will not taken

Unconditional Branch

1
2
3
4
5
6
7
8
9
.text:004078C3 loc_4078C3:
.text:004078C3 000 mov esp, edi ; cursor
.text:004078C5 000 mov eax, dword_591EAC
.text:004078CA 000 lea ecx, [eax+4]
.text:004078CD 000 mov edx, eax
.text:004078CF 000 sar edx, cl
.text:004078D1 000 lea eax, [eax+edx*2]
.text:004078D4 000 mov dword_591EAC, eax
.text:004078D9 000 jmp short loc_4

becomes:

1
2
0x4078d9: jmp 0x40789a
branch will taken

Looks nice.

Last Words

Triton’s emulation iteration is compatible to IDAPython manner. Therefore, The combination of IDA Pro and Triton is pretty good.

Cheers,

Introduction

IDAPython is a powerful feature of IDA Pro, and there are many open-sourced IDAPython projects. However, we cannot use every GUI-based IDAPython script due to some Qt-related breaking changes between IDA Pro 6.8 and 6.9 or later. The main problem is about migrating no longer supported PySide code to PyQt5.

Recently I ported PySide code within idasec–one of the most sophisticated deobfuscation frameworks, which tackles opaque predicates and call stack tampering in terms of infeasibility questions, by utilizing Backward-Bounded Dynamic Symbolic Execution proposed in the remarkably well written paper S. Bardin et al. IEEE S&P’17–to PyQt5.

That’s why I decided to write this blog post for a note to self and for someone trying to do similar thing.

Related Work

There are 2 guidances to migrate PySide code to PyQt5:

Please read them before. I only give supplemental information in addition to predecessors.

How to Migrate

Now let’s get started.

Change QtGui methods to QtWidgets

Most methods in QtGui migrated to QtWidgets. Therefore,

1
from PySide import QtGui, QtCore

becomes:

1
from PyQt5 import QtCore, QtGui, QtWidgets

As an example, QTextEdit described in Hex Blog. In additions, the methods to be rewritten are as follows:

  • QtWidgets.QLayout
  • QtWidgets.QVBoxLayout
  • QtWidgets.QHBoxLayout
  • QtWidgets.QWidget
  • QtWidgets.QTableWidget
  • QtWidgets.QListWidget
  • QtWidgets.QTabWidget
  • QtWidgets.QDockWidget
  • QtWidgets.QTreeWidget
  • QtWidgets.QTreeWidgetItem
  • QtWidgets.QPushButton
  • QtWidgets.QRadioButton
  • QtWidgets.QToolButton
  • QtWidgets.QButtonGroup
  • QtWidgets.QGroupBox
  • QtWidgets.QSpinBox
  • QtWidgets.QCheckBox
  • QtWidgets.QComboBox
  • QtWidgets.QTextEdit
  • QtWidgets.QLineEdit
  • QtWidgets.QApplication
  • QtWidgets.QLabel
  • QtWidgets.QSizePolicy
  • QtWidgets.QMenu
  • QtWidgets.QFrame
  • QtWidgets.QProgressBar
  • QtWidgets.QStyle
  • QtWidgets.QSpacerItem
  • QtWidgets.QScrollArea
  • QtWidgets.QSplitter
  • There might be more…

My experience says that other than the following 3 methods may be rewritten:

  • QtGui.QPixmap
  • QtGui.QIcon
  • QtGui.QFont

idacute may overwrite all of QtGui methods, so I think there still needs to be manual works.

Overwrite _fromUtf8

We also need to overwrite _fromUtf8.

1
2
3
4
try:
_fromUtf8 = QtCore.QString.fromUtf8
except AttributeError:
    _fromUtf8 = lambda s: s

Others

These issues are described by predecessors:

  • Handling SIGNAL
  • Change FormToPySideWidget to FormToPyQtWidget
  • Change setResizeMode to setSectionResizeMode

Conclusion

This time, I was able to run idasec on IDA Pro 7.0 with some bug fixes and dirty patches – like this cool video:

If you are an IDA Pro 7.0 user, note that other backward-compatibility issue described in IDA: IDAPython backward-compatibility with 6.95 APIs will occur.

Enjoy!

HAI DOMO VIRTUAL YOUTUBER KIZUNA AI DESU. I’m still working on my English.

 Security meets Machine Learningという勉強会にて,上記のタイトルで発表した.資料はこちら:

 謎の力が働いて会社からの発表になっておりますが,機械学習の研究をしているわけではありません.既存研究の再現実装を試みているとこれ中国語の部屋じゃんという気持ちになる.
 ともあれ,これまで各種資料はただSpeakerDeckに載せるだけだったのを今後はブログから一元的に参照できるようにします.

 なにもかも忘れかけている.

はじめに

 z3pyはSMTソルバZ3のPythonバインディング.たとえば

1
2
3
4
5
...
if(x * 2 + 3 * y == 4
&& x * 3 + y == -1){
puts("congrats!");
}

のようなプログラムに対して

1
2
3
4
5
6
7
8
9
10
11
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x * 2 + 3 * y == 4)
s.add(x * 3 + y == -1)
print(s.check())
print(s.model())

としてやれば期待される入力値[x = -1, y = 2]を算出できる.これだけではだからなに? という感じだが.シンボリック実行は各命令とメモリの状態からこの割当を自動生成するものだと思えばよい.これがangrやらTritonやらmiasmやらmanticoreやら,その他いまどきのバイナリ解析ツール群の基盤となっているというわけです.

参考になったサイト

 で,メモっとかないと忘れるので.SAT/SMTソルバのしくみやシンボリック実行全般まで広げると膨大になるということで,z3pyに限っています.前者については高速SATソルバーの原理 - 基盤(S)離散構造処理系プロジェクト[PDF]SAT/SMTソルバの仕組み - SlideShareを読むとよいでしょう.いまどきのSAT/SMTソルバにはVSIDSやらLubyリスタートやらいろいろな工夫が盛り込まれているが,とりあえずユーザとしてはDPLLとCDCLさえ抑えておけば問題ないはず.後者,シンボリック実行全般に関するおすすめの文献は秘密.Pythonバインディング以外の記事,angrやTritonなどサードパーティのツール群に関する記事も省いてある.

ウェブサイト 概要
CTF/Toolkit/z3py - 電気通信大学MMA 日本語で書かれた入門資料.これには書かれてないがBitVecSortも便利.
Theorem prover, symbolic execution and practical reverse-engineering z3pyのチュートリアル.まずはこの通りに手を動かす.
Breaking Kryptonite’s Obfuscation: A Static Analysis Approach Relying on Symbolic Execution シンボリック実行の最小構成の実装.
0vercl0k/z3-playground 上2つの資料で参照されているソースコード群.
Solving a simple crackme using Z3 – Aneesh Dogra’s Blog 簡単なcrackmeのwriteup.
Playing with Z3, hacking the serial check. – rosako’s blog 簡単なcrackmeのwriteup.
Using SAT and SMT to defeat simple hashing algorithms - LSE Blog オレオレハッシュ関数の解析.
Reversing the petya ransomware with constraint solvers ランサムウェアPetyaのSalsa実装の不備を突くdecryptor.
thomasjball/PyExZ3 シンボリック実行の実装例.z3公式からリンクが貼られている.symbolic/以下,z3_wrap.py, loader.pyが参考になる.
Quick introduction into SAT/SMT solvers and symbolic execution (DRAFT) [PDF] いろいろリンク貼ったけどこれだけ読めばいい.SMTソルバの紹介.数独の解き方.マインスイーパの自動化.デコンパイラ.難読化解除.シンボリック実行.ハッシュ関数の解析.全部載っている.Dennis Yurichev氏,Reverse Engineering for Beginnersも書いていて,慈善事業家か?

 はてなブックマークを使っていればよかったのではという気がしてきた.

おわりに

 z3py便利最高ですね.みなさんは便利最高ですか?
 これで次のようなCTFの問題を解くことができます:

問題 大会
Unbreakable Enterprise Product Activation Google CTF 2016
Ropsynth SECCON 2016 Online CTF
baby-re DEF CON CTF Qualifier 2016
amandhj DEF CON CTF Qualifier 2016
Pepperidge Farm DEF CON CTF Qualifier 2017

 まあ明らかにangr使ったほうが楽.とりあえずいくつかやってみただけで,ほかにもたくさんあると思う.
 Bareflank Hypervisorを読むのはいつになるかわかりません.

 いまさらながら,情報セキュリティ系論文紹介 Advent Calendar 2016あるいはBitVisor Advent Calendar 2016に投稿されるはずだった文章を供養する.

はじめに

 本稿では,シン,すなわち薄いハイパーバイザ (thin hypervisor) の動向を紹介する.
 薄いハイパーバイザとは,小規模であることを志向したハイパーバイザだ——ということにしておこう.小規模というのは,一部のイベントのみトラップするということだ.メリットとしては,実装・学習コストやオーバーヘッド,TCB (trusted computing base) を削減できる点が挙げられる.
 用語の初出はBitVisorの論文[T. Shinagawa, et al. VEE’09]だが,多くはWindows向けルートキットとして開発されたBlue Pillという手法[J. Rutkowska. Black Hat USA’06]の流れを汲んでいる.そのため,ブート時からゲストを掌握するのではなく,のちほど——あえてchain of trustの構築を放棄して——カーネルドライバとしてロードされるものが一般的である.そのほか,単一のゲストのみ対象とする,セキュリティを意識しているといった傾向が見られる.
 前編となる今回は,3種類の薄いハイパーバイザを見ていく.

ksm

リポジトリ https://github.com/asamy/ksm
形態 カーネルドライバ
仮想化支援機能 Intel VT-x with EPT
サポートしている環境 Windows 7/8/8.1/10, Linux
言語 C, アセンブリ言語
ライセンス GNU GPL v2

 ksmは高速,拡張可能かつ小規模であることを旨としているハイパーバイザで,アンチウイルスソフトウェアやサンドボックスへの利用を意識して開発されている.機能は以下の通り:

  • IDT Shadowing
  • EPT violation #VE (Broadwell以降)
  • EPTP switching VMFUNC (Haswell以降,もしサポートされていなければVMCALLで代替)
  • Builtin Userspace physical memory sandboxer (ビルドオプション)
  • Builtin Introspection engine (ビルドオプション)
  • APIC virtualization (実験的機能)
  • VMX Nesting (実験的機能)

 主なソースコードは以下の通り:

main_nt.c, main_linux.c カーネルドライバのエントリポイント,ioctlディスパッチ
ksm.c ハイパーバイザ全体の初期化
vmx.S, vmx.asm IDTやEPT violationのトラップ,ゲストのレジスタ退避
vcpu.c VMCSの読み書き
exit.c VMExitのハンドラ
um/um.c ユーザーランドのエージェント
sandbox.c サンドボックス機能
introspect.c イントロスペクション機能
epage.c EPTフック機能
mm.c メモリ管理
hotplug.c CPUホットプラグに関する処理

 カーネルドライバをロードし,ユーザーランドのエージェントからioctlを発行,サンドボックス機能またはイントロスペクション機能,EPT機能を呼び出すという流れになっている.詳細はDocumentation/SPEC.rstを参照のこと.

SimpleVisor

リポジトリ https://github.com/ionescu007/SimpleVisor
形態 カーネルドライバ
仮想化支援機能 Intel VT-x with EPT, AMD-V
サポートしている環境 Windows 8/8.1/10, UEFI
言語 C, アセンブリ言語
ライセンス 2 clause BSD

 SimpleVisorは,名前の通り極力シンプルであることをめざしたハイパーバイザだ.全体で1700行程度.開発者はWindows Internalsの著者のひとりで,README.mdにはこう書かれている:

Have you always been curious on how to build a hypervisor? Has Intel’s documentation (the many hundreds of pages) gotten you down? Have the samples you’ve found online just made things more confusing, or required weeks of reading through dozens of thousands of lines and code? If so, SimpleVisor might be the project for you.

 そういうわけで,SimpleVisorはIntel SDM (とくに,ハイパーバイザまわりはVol. 3C) の解読にうんざりした人向けだ.学習にはもってこい.CPUID, INVD, VMX, XSETBVのみトラップするようになっており,ネストには対応していない.しかし,XenやBochsでさえ追いついていない最新の仮想化支援機能にいちはやく追随しようとしている.
 主なソースコードは以下の通り:

nt/shvos.c カーネルドライバのエントリポイント
shv.c VMExit/VMEntryのコールバック関数の登録
shvvp.c コールバック関数の実体,仮想CPUの初期化
shvvmx.c VMCSの初期化
shvvmxhv.c VMExitのハンドラ
shvutil.c GDTの変換

 シンプル.

HyperPlatform

リポジトリ https://github.com/tandasat/HyperPlatform
形態 カーネルドライバ
仮想化支援機能 Intel VT-x with EPT
サポートしている環境 Windows 7/8.1/10
言語 C++, アセンブリ言語
ライセンス MIT

 HyperPlatformは,カーネルランドで動くコード,すなわちWindows向けルートキットやWindowsカーネル自体の解析を目的として開発されているハイパーバイザ.物理メモリと仮想メモリへのアクセス,関数呼び出し,命令単位のコード実行を監視できるようになっている[S. Tanda. REcon’16]
 主なソースコードは以下の通り:

driver.cpp カーネルドライバのエントリポイント,各種コールバック関数の登録
log.cpp ログ出力
global_object.cpp グローバル変数の初期化
performance.cpp パフォーマンス計測
util.cpp PTE_BASEの取得,メモリアドレス変換,VMCALLのラッパなど
power_callback.cpp 電源状態のコールバック関数
hotplug_callback.cpp CPUホットプラグのコールバック関数
vm.cpp 仮想CPUの初期化,VMCSの読み書き
ept.cpp EPTの構成
vmm.cpp 命令のトラップ,VMExitのハンドラ
Arch/x64/x64.asm, Arch/x86/x86.asm VMX命令呼び出しにともなう命令列
kernel_stl.cpp ntoskrnl経由でカーネルドライバからSTLを利用する

 エントリポイントから手続き的に書き下されていて,わかりやすい.ハイパーバイザとしての機能もさることながら,STLを強引に呼び出すハックがかっこいい.
 この拡張例には以下がある:

MemoryMon カーネルランドへのコード挿入を検知する
EopMon マルウェアによる特権昇格攻撃を検知する
DdiMon EPTを用いたAPIフック
GuardMon PatchGuardの挙動解析

 いずれもカーネルドライバのエントリポイントで追加機能を初期化するしくみ.
 やや温め納豆は遠くなりにけり.

おわりに

 いずれもSandy Bridge以降のいまどきの環境であれば動作する.
 卒業研究ではQEMUをベースとしたマルウェア解析環境を開発していたのだけど,やはり速度面に難があるし,このあたりの技術を再検討しないとなー.
 なお,今回取り上げなかったハイパーバイザには以下のようなものがある:

MoRE ルートキット文脈のハイパーバイザ.やや古い
HyperBone HyperPlatformと似た機能をもつ.やや古い
Noah 未踏のアレ.OS X上でLinuxバイナリを動かす.MacBook持ってないので試せないのだわ
Bareflank type 1, 2, ドライバいずれの形態のVMMもサポートしたライブラリ.しかもC++で書ける

 なかでもBareflankがヤバいので後編ではこれを読んでいきます.

 本稿はSFC-RG Advent Calendar 2016の4日目である.

はじめに

 あなたは研究の中間発表を終えて,今晩何を食べようか考えている.たしかに準備不足ではあったけれど,研究の前提をいまいち解さないファカルティの高飛車な質問にはうんざりしたし,今日くらいはパーッと気分転換したいものだ.そういうわけで,あなたは⊿館を飛び出して焼肉 ざんまい 湘南台店に行くことにした.

組合せ最適化

 さて,着席し,メニューを開いたあなたはしばし考える.限られた予算,限られた時間,限られた胃袋の容量——いったい何を頼めば最も満足できるだろうか?
 そんなとき,組合せ最適化が役に立つんです.騙されたと思って,メニューを必死に転記してみよう:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
import numpy as np, pandas as pd
menu = ['カルビ', '和牛カルビ', '和牛中落ちカルビ', 'ハラミ', '厚切りロース', 'ネギ牛タン塩', '牛タン塩',
'イベリコ豚', 'カシラ', '豚トロ', 'ネギ豚タン塩', '豚タン塩', '厚切りベーコン', 'ウインナー', 'チョリソ',
'ホルモン', 'シロコロホルモン', 'レバー', '白レバー', 'ハツ', 'ミノ',
'お得!! 三種盛り', '本日の塩三種盛り', '本日の味噌三種盛り']
price = [720, 950, 850, 720, 690, 950, 850,
600, 550, 580, 680, 580, 500, 380, 400,
550, 600, 550, 450, 550, 650,
1280, 780, 780]
n = len(menu)
np.random.seed(0)
df = pd.DataFrame({
'品目': menu,
'値段': price,
'満足度': np.random.randint(10, 20, n),
'焼き時間': np.random.randint(5, 10, n),
'量': np.random.randint(10, 20, n),
})
print(df)
値段 品目 満足度 焼き時間
0 720 カルビ 15 9 10
1 950 和牛カルビ 10 8 10
2 850 和牛中落ちカルビ 13 5 14
3 720 ハラミ 13 8 15
4 690 厚切りロース 17 5 15
5 950 ネギ牛タン塩 19 7 16
6 850 牛タン塩 13 8 18
7 600 イベリコ豚 15 5 14
8 550 カシラ 12 6 11
9 580 豚トロ 14 8 14
10 680 ネギ豚タン塩 17 8 19
11 580 豚タン塩 16 8 18
12 500 厚切りベーコン 18 5 11
13 380 ウインナー 18 6 11
14 400 チョリソ 11 6 17
15 550 ホルモン 16 6 19
16 600 シロコロホルモン 17 5 19
17 550 レバー 17 7 13
18 450 白レバー 18 9 16
19 550 ハツ 11 8 17
20 650 ミノ 15 8 12
21 1280 お得!! 三種盛り 19 7 10
22 780 本日の塩三種盛り 18 9 13
23 780 本日の味噌三種盛り 19 7 15

 メニューがpandasのデータフレームになった.取り急ぎ(?)満足度・焼き時間・量は乱数で埋めている.
 あなたはこのメニューの中から,最も満足度の高い組合せを見つけたい.それも,限られた予算,限られた時間,限られた胃袋の容量という条件を満たすような.ここではそのわがままを割当問題として解くことにする.

変数 $x_i \in \{0, 1\}$ i番目の料理を選ぶかどうか
目的関数 $\sum_i{満足度_i x_i}$ $\rightarrow$ 最大
制約条件 $\sum_i{予算_i x_i} \le 12000$ 予算制限
$\sum_i{焼き時間_i x_i} \le 120$ 時間制限
$150 \le \sum_i{量_i x_i} \le 200$ 分量制限

 こういった問題はpulpという整数計画法ライブラリを使って解くことができる:

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
from pulp import *
m = LpProblem(sense = LpMaximize) # 最大化問題
df['x'] = [LpVariable('x%d' % i, cat = LpBinary) for i in range(n)] # i番目の品目を選択するかしないか
m += lpDot(df.満足度, df.x) # 目的関数:満足度の最大化
m += lpDot(df.値段, df.x) <= 12000 # 制約条件:予算
m += lpDot(df.焼き時間, df.x) <= 120 # 制約条件:焼き時間
m += lpDot(df.量, df.x) >= 150 # 制約条件:量
m += lpDot(df.量, df.x) <= 200 # 制約条件:量
m.solve()
if m.status == 1:
df['val'] = df.x.apply(lambda v: value(v)) # 結果
print(df[df.val == 1].品目)
print('満足度 {}'.format(sum(df[df.val == 1].満足度)))
print('値段 {}'.format(sum(df[df.val == 1].値段)))
>>>
0 カルビ
4 厚切りロース
5 ネギ牛タン塩
7 イベリコ豚
8 カシラ
9 豚トロ
12 厚切りベーコン
13 ウインナー
16 シロコロホルモン
17 レバー
18 白レバー
20 ミノ
21 お得!! 三種盛り
22 本日の塩三種盛り
23 本日の味噌三種盛り
Name: 品目, dtype: object
満足度 251
値段 10060

 はい.順番はともかくとして,これらを食べれば満足できそうだ.
 ここまで考えたところで,あなたは今月の懐具合がよろしくないことを思い出す.なるべく出費を抑えて,それでいてある程度満足できるような品目の組合せはあるだろうか?
 これも同様に割当問題として考えられる.

変数 $x_i \in \{0, 1\}$ i番目の料理を選ぶかどうか
目的関数 $\sum_i{予算_i x_i}$ $\rightarrow$ 最小
制約条件 $\sum_i{満足度_i x_i} \le 200$ 満足度制限
$\sum_i{焼き時間_i x_i} \le 120$ 時間制限
$150 \le \sum_i{量_i x_i} \le 200$ 分量制限
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
m = LpProblem(sense = LpMinimize) # 最小化問題
a['v'] = [LpVariable('v%d' % i, cat = LpBinary) for i in range(n)] # i番目の品目を選択するかしないか
m += lpDot(df.値段, df.x) # 目的関数:予算の最小化
m += lpDot(df.満足度, df.x) >= 200 # 制約条件:満足度
m += lpDot(df.焼き時間, df.x) <= 120 # 制約条件:焼き時間
m += lpDot(df.量, df.x) >= 150 # 制約条件:量
m += lpDot(df.量, df.x) <= 200 # 制約条件:量
m.solve()
if m.status == 1:
df['val'] = df.x.apply(lambda v: value(v)) # 結果
print(df[df.val == 1].品目)
print('満足度 {}'.format(sum(df[df.val == 1].満足度)))
print('値段 {}'.format(sum(df[df.val == 1].値段)))
>>>
7 イベリコ豚
10 ネギ豚タン塩
11 豚タン塩
12 厚切りベーコン
13 ウインナー
14 チョリソ
15 ホルモン
16 シロコロホルモン
17 レバー
18 白レバー
22 本日の塩三種盛り
23 本日の味噌三種盛り
Name: 品目, dtype: object
満足度 200
値段 6850

 200の満足度でいいなら豚ばっか食ってろということらしい.

多腕バンディット問題

 いやいやちょっと待った.乱数でお茶を濁しているけど,あらゆる品目の満足度なんて知らないじゃないか.全品目を食べたことがあるならいざ知らず.それに,毎日同じ店で同じ食事をとるわけでもない.焼肉屋にしたって,湘南台には寅屋にえのもとにとあるわけだ.
 そういうわけで,あなたはいろいろな店に行き,いろいろな注文をして,なるべくどれを頼んでも満足度の高い食事のとれる店を見つけたいと考えた.しかしここで疑念が生まれる——いまの店でそこそこ満足できるなら,別の店を探さなくてもよいのではないか? しかしいまの店に行き続ける限り,別の店の食事を食べることはできないぞ.しかしそこがハズレだとしたら.さてどうしよう——業界用語でこれを探索利用のトレードオフ (exploration-exploitation tradeoff) という.

これまでの学習結果を利用 (exploitation) しようとすると,探索 (exploration) が減ってしまい,機会損失が増えてしまう.一方,探索を増やせば,学習した最良の行動とは異なる行動をとることが増えるため,得られる報酬が減ってしまう.学習した最良の行動との差が,探索のコストということになる.– 牧野,et al. 『これからの強化学習

 このトレードオフを解消する試みを多腕バンディット問題という.多腕バンディット問題は,複数のスロットマシンのレバー(腕)を次々と引いていき,最終的に得られる報酬を最大化するというもので,強化学習の一種といえる.各スロットマシンの報酬はそれぞれ一定の確率分布に従っている.言い換えれば,いろいろな店のメニューにある品目を試していき,最終的に得られる満足度を最大化していく,ということになる.もちろん,品目によって得られる満足度に違いはあるが,なるべく何を食べても満足度の高い店を絞り込んでいきたい.
 そのためのアルゴリズムのうち,ここでは$\epsilon$-GreedyとUCB1を紹介したい.

$\epsilon$-Greedy

 デフォルトで現在最良な選択肢を選ぶが,一定の確率でいま最良と思っていないような選択肢を選びにいく手法.

  • $\epsilon - 1$の確率で最適だと思われる選択肢を利用する
  • $\epsilon / 2$の確率で最適だと思われる選択肢を探索する
  • $\epsilon / 2$の確率で最悪だと思われる選択肢を探索する

 $\epsilon$ Greedyはつまり行きつけの店に入り浸るタイプのアルゴリズムだ.

UCB1

 それもいいが,実はいまの行きつけよりもっといい店なのに,一度行って微妙だったからといって行かないままになっている店がないだろうか? UCB1は,それぞれの店についてどれくらい知っているかを考慮に入れ,なるべく多くの店のことを知ろうとするアルゴリズムだ.具体的には,各店(腕)についてUCB (Upper Confidence Bound) という値を計算する.

 $\overline {x}_{j}+c\sqrt {\dfrac {2\log n} {x_{j}}}$

 ただし$\overline {x}_{j}$$_{j}$番目の店の満足度(報酬)の期待値,$n$はそれまでに店を回った回数の合計,$n_{j}$$_{j}$番目の店に行った回数,$c$は定数.UCB1は,この値が最大になる店に飛び込んでいく.あなたが好奇心旺盛なら,こちらのアルゴリズムを使って考えたほうがいいだろう.
 この手法のメリットとして,ベストでない店に行く回数を確率$1$$O(\log n)$以内に抑えられる.長々とした証明は論文を参照していただくとして,これは店に行く回数が十分大きい場合の理論限界に到達している.デメリットとしては,探索のためによくない店にあたってしまうことが多いという点が挙げられる.

実験

 では,$\epsilon$-GreedyとUCB1が最良の店を選ぶ過程はどうなっているだろうか? 『バンディットアルゴリズムによる最適化手法』のサンプルコードをPython3 + numpy向けに改変して実験.

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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
import pandas as pd
import numpy as np
import matplotlib.pyplot as plt
import random
import math
import seaborn as sns
class BernoulliArm():
def __init__(self, p):
self.p = p
def draw(self):
if random.random() > self.p:
return 0.0
else:
return 1.0
class EpsilonGreedy():
def __init__(self, epsilon, counts, values):
self.epsilon = epsilon
self.counts = counts
self.values = values
return
def initialize(self, n_arms):
self.counts = np.zeros(n_arms)
self.values = np.zeros(n_arms)
return
def select_arm(self):
if random.random() > self.epsilon:
return np.argmax(self.values)
else:
return np.random.randint(0, len(self.values))
def update(self, chosen_arm, reward):
self.counts[chosen_arm] += 1
n = self.counts[chosen_arm]
value = self.values[chosen_arm]
new_value = ((n-1) / float(n)) * value + (1 / float(n)) * reward
self.values[chosen_arm] = new_value
return
class UCB1():
def __init__(self, counts, values):
self.counts = counts
self.values = values
return
def initialize(self, n_arms):
self.counts = np.zeros(n_arms)
self.values = np.zeros(n_arms)
return
def select_arm(self):
n_arms = len(self.counts)
for arm in range(n_arms):
if self.counts[arm] == 0:
return arm
ucb_values = [0.0 for arm in range(n_arms)]
total_counts = sum(self.counts)
for arm in range(n_arms):
bonus = math.sqrt((2 * math.log(total_counts)) / float(self.counts[arm]))
ucb_values[arm] = self.values[arm] + bonus
return np.argmax(ucb_values)
def update(self, chosen_arm, reward):
self.counts[chosen_arm] = self.counts[chosen_arm] + 1
n = self.counts[chosen_arm]
value = self.values[chosen_arm]
new_value = ((n - 1) / float(n)) * value + (1 / float(n)) * reward
self.values[chosen_arm] = new_value
return
def test_algorithm(algo, arms, num_sims, horizon):
chosen_arms = np.zeros(num_sims * horizon)
rewards = np.zeros(num_sims * horizon)
cumulative_rewards = np.zeros(num_sims * horizon)
sim_nums = np.zeros(num_sims * horizon)
times = np.zeros(num_sims * horizon)
for sim in range(num_sims):
sim += 1
algo.initialize(len(arms))
for t in range(horizon):
t += 1
index = (sim - 1) * horizon + t - 1
sim_nums[index] = sim
times[index] = t
chosen_arm = algo.select_arm()
chosen_arms[index] = chosen_arm
reward = arms[chosen_arm].draw()
rewards[index] = reward
if t == 1:
cumulative_rewards[index] = reward
else:
cumulative_rewards[index] = cumulative_rewards[index - 1] + reward
algo.update(chosen_arm, reward)
return [sim_nums, times, chosen_arms, rewards, cumulative_rewards]
means = np.array([0.1, 0.1, 0.1, 0.1, 0.9])
n_arms = len(means) # 腕は5本
random.shuffle(means)
arms = [BernoulliArm(x) for x in means]
for epsilon in [0.1, 0.2, 0.3, 0.4, 0.5]: # epsilonを変えたらどうなるか?
algo = EpsilonGreedy(epsilon, [], [])
algo.initialize(n_arms)
results = test_algorithm(algo, arms, 5000, 500)
df = pd.DataFrame({"times": results[1], "rewards": results[3]})
grouped = df["rewards"].groupby(df["times"])
plt.plot(grouped.mean(), label="epsilon="+str(epsilon))
algo = UCB1([], [])
algo.initialize(n_arms)
results = test_algorithm(algo, arms, 5000, 500)
df = pd.DataFrame({"times": results[1], "rewards": results[3]})
grouped = df["rewards"].groupby(df["times"])
plt.plot(grouped.mean(), label="UCB1")
plt.legend(loc="best")
plt.show()

 好奇心旺盛な人は序盤それなりに苦労することがわかる.

おわりに

 こうしたナイーブな実装で焼肉の頼み方を最適化したり,店の巡り方を最適化できるかどうかというとまあ実際微妙(たとえば焼肉の各品目から得られる満足度は,限界効用逓減の法則に従ってすり減っていく)だが,日々の意思決定をアルゴリズム的に考えてみる遊びはそれなりにおもしろい.ソーシャルゲームにどう課金するか,というのもこの俎上に載せられる.
 『Algorithms to Live By: The Computer Science of Human Decisions』という本はそういう,情報系の人間がよくやる与太話をまじめに考察したものだ——書類はどのキャッシュアルゴリズムに従って並べるべきかとか.先に挙げた探索と利用のトレードオフについても述べられている.YouTubeで著者らの講演を観てほしい.

 はい.

参考文献

追記 (2016.12.06)

 今回のような設定では多腕バンディット問題というより最適腕識別として考えたほうがよさそう.多腕バンディット問題は累積報酬の最大化が目的だけれど,最適腕識別はどの腕が最良か発見するのが目的.将来の報酬が最大の腕を見つける,ということ.『バンディット問題の理論とアルゴリズム』を読めばいいんだとか.