HITCON CTF 2020の“Tenet”を模倣したアセンブリー言語シミュレーター
注意
- ⛔️⛔️⛔️ この記事は映画Tenetのネタバレを微粒子レベルで含んでいます！ ⛔️⛔️⛔️
- まだ観ていない人は、この記事を読むかどうかは別としてとりあえずTenetを観てください
はじめに
友人からHITCON CTF 2020で“Tenet”という問題が出題されたと聞いた。すでに映画のTenetは何回か観て内容を知っていたのもあってか、その問題が非常におもしろかった。問題の詳細は後述するが、この問題の試行錯誤にはアセンブリー言語の特殊な動作環境が必要となるため、問題のコセンプトをある程度残しつつ、筆者のような普段はリバースエンジニアリングといったアンセンブリー言語関連に関わりが薄い状態でも問題のおもしろさを体験できるようなアセンブリー言語シミュレーターをScalaで作成した。またScala.jsを利用してWebアプリケーションにして公開もしている。この記事ではまずHITCON CTF 2020の問題であるTenetについて解説し、そのあとで開発したシミュレーターについて述べる。なお開発したシミュレーターのソースコードは下記のGitHubリポジトリーに置かれている。
この記事を読んで分かりにくい部分や改善するべき点を見つけた場合は、気軽に著者に連絡してほしい。
HITCON CTF 2020 Tenet
英語で書かれた問題の詳細は下記のページで読むことができる。
この問題ではTenetと呼ばれる次のようなサービスが動いている。
- 最大で2000Bytesのシェルコード[1]をユーザーから受けとり、それを実行する[2]
- 実行後にメモリー上にある「トークン」と呼ばれるデータが削除（
0でクリア）されていなければならない - その後、実行されたコードを逆に実行して（2）のトークンが元に戻っていれば最終的な成功となる
プレイヤーはまず、メモリー上にあるトークンを削除するような機械語を送ると、Tenetはそれを実行する。そのときにgdbのようなデバッガーがどのように機械語を実行したかを記録している。（2）の終了後に、デバッガーはレジスターなどを0で初期化して、記録した機械語を実行順とは逆に1ステップずつ実行していく。そして最後の逆実行が終わったときにメモリー上のトークンが復活していればOKという問題となっている。
Tenetシミュレーター
アセンブリーとかリバースエンジニアリングの知識があればもっと違った解き方ができるとは思うが、よくわからなかったので問題を解くための次のようなシミュレーターを作成した。
これは問題とはいくつか違う点があるので、この点について述べていく。
- 問題では特定のメモリーアドレス上に消去するべきトークンが存在するが、きちんとエミュレーションするのが面倒だったので最初から
EAXレジスターにロードされている- したがって順行時には終了時に
EAXレジスターが0となっていればOKとなる
- したがって順行時には終了時に
- また
EAXなどのレジスターがどういうビット数であれば正確なのか？ということもよくわからなかったし、そもそもScalaでビット演算を行うのが面倒そうだったのでScalaのInt型とした- なのでレジスターに対して直接
-1をかけ算するといったことができる - ただし消すべきトークンが
-113のような負の値となると面倒そうだったので、そうならないように乱数の絶対値を利用している
- なのでレジスターに対して直接
- シミュレーターなので当然ではあるが、実際の命令（オペコード）に比べて遥かに少ない命令しかサポートしていない
- 問題を教えてくれた友人はアーキテクチャー依存の非想定解で解いたらしいが、そういうことは当然不可能になる
- アセンブリー言語のオペコードについては相当曖昧な記憶で模倣したので、実際のオペコードとは挙動が違ったりすることがあるかもしれない
シミュレーターの使い方
上記のURLを開くとエディターと順行・逆行それぞれの実行後の状態が表示される。
このサンプルでは（特に意味のないコードが初期値としてセットされているため）次のような操作を行なっている。前述のとおりシミュレーターのレジスターEAXには乱数が入っているので、結果は実行により異なったものが表示される。
-
EAXレジスターの内容をEBXレジスターへコピーする -
EBXレジスターに-1をかけ算する -
EAXレジスターの内容をEBXレジスターへコピーする -
ECXが0と等しいか比較する
Forward execution resultには次のように表示されている。
Registers(eax = 10, ebx = 10, ecx = 0, flags = Flags(zero = true, carry = false))
乱数なので実行次第だが、ここでは乱数が10だったため、EAXとEBXが両方とも10となり、また0であるECXに対して0との比較を行なってそれが正しかったためzero flag = trueとなっている。
続いてこれを逆に実行するときに用いられたコードがBackward executions(AST) として表示されている。この例では実行結果はEAX = 0となっており、もともとの乱数である10に戻っておらず失敗であるためJudgementはNGとなっている。
このエディター部分に上手くアセンブリー言語を書いて、JudgementのところにOKを表示させるのが目標となる。
対応しているオペコード
シミュレーターが対応しているオペコードを次の表で示す。
| オペコード\オペランド | 1 | 2 |
|---|---|---|
| CMP | レジスター | 整数 |
| ADD | レジスター | 整数 |
| MUL | レジスター | 整数 |
| MOV | レジスター | レジスター |
| SET | レジスター | 整数 |
| JMP | ラベル名 | |
| JZ | ラベル名 | |
| LABEL | ラベル名 |
本当はMOVだけにSETの意味（レジスターに整数をセットする）を持たせたかったが、実装を簡単にするために多少違和感のある命令にした。
逆順の実行に関する注意
このシミュレーターでJMPやJZを利用すると分かることではあるが、逆順での実行は入力したアセンブリーを逆順に実行するわけではない。たとえば次のようなアセンブリーを入力してみる。
add ebx, 10
cmp ebx, 10
jz end
add ecx, 9999
Label: end
これの実行結果（順行）は次のようになる[3]。
Registers(eax = 4, ebx = 10, ecx = 0, flags = Flags(zero = true, carry = false))
EBXは最初常に0から開始となるため、そこに10を足して10と比較するので、必ずjzではジャンプとなりadd ecx, 9999は実行されない。すると逆順で実行する命令列は次のようになる。
Cmp(Ebx(),10)
Add(Ebx(),10)
この命令列はすでに逆順になっているため、逆実行ではレジスターを初期化した後に上から下へと実行される。これを見て分かるように次のようになっている。
- 実行されていない
add ecx, 9999に対応する処理が存在しない -
JZやラベルが消去されている- 問題では、逆順の実行でデバッガーのような存在が次に実行するべき命令を決定するため、このようなジャンプは全て無視される
つまり、逆順での実行においては、順行で実行された命令だけが逆に実行されることとなる。
解答例
次の場所にJudgementがOKとなる正解が書かれている。
- https://github.com/y-yu/tenet-simulator/blob/master/jvm/src/main/scala/tenet/simulator/Main.scala[4]
まとめ
問題の種類はリバース（エンジニアリング）となってはいるが、このような超適当なシミュレーターを作ってやってもある程度は再現できる程度にはアーキテクチャーに非依存な問題となっている。筆者も普段は暗号などの問題を解いているが、友人から聞いた話がおもしろかったのでやってみたという感じである。また記事の内容とは関係ないが、映画Tenetは非常によかった！
Discussion