Internprise Encryption

以下のファイルが与えられた。

These files were given:

davecrypt.js は、JavaScriptによる暗号化プログラムのようだった。
また、flag.txt の冒頭部分は、以下のようになっていた。

davecrypt.js looked like an encryption program written in JavaScript.
Also, the first part of flag.txt was:

00000000 c3 bb c3 96 c3 8b c3 8d 6b c2 80 c3 ae 12 c3 96 |........k.......| 00000010 6c 50 1d c2 9b c3 bb 6a 1e c3 96 14 c2 bd c3 a5 |lP.....j........| 00000020 17 c2 9e c3 b9 66 72 15 24 c3 9b 37 c3 a8 23 c3 |.....fr.$..7..#.| 00000030 84 21 c3 ba 74 c3 a0 c3 87 c3 b3 33 c3 89 3e 32 |.!..t......3..>2| 00000040 c4 80 c3 8f 66 2b c3 8f c3 8b 3a c3 93 03 c3 8d |....f+....:.....|

だいたい2バイトごとに c で始まるバイトがあり、その中に 6c など 0x80 未満のバイトが混ざっていることから、 flag.txt はUTF-8として解釈できそうだと推測した。
また、davecrypt.js は乱数や時刻を用いた処理を行う行を含むが、よく見るとこれらの行は復号代入演算子の右辺が常にゼロとなり、無視できることがわかる。
そこで、davecrypt.js のそれぞれの行に相当する処理を考え、Z3で入力を求める以下のプログラムを作成した。
なお、入力の各要素は 0xff 以下であると仮定した。

There are bytes beginning with c in about each 2 bytes. Also there are bytes less than 0x80 such as 6c. Therefore, I guessed that flag.txt can be decoded as UTF-8.
Also, davecrypt.js contains lines that uses random numbers and date, but I found that the lines can be ignored because the right-hand side of the compound assignment operators are always zero.
Based on these, I determined formulas corresponding to each lines of davecrypt.js and created this program to obtain the input using Z3.
Also note that I assumed that each elements of the input are 0xff or less.

solve.py

このプログラムを用いて flag.txt に対応する入力を求めると、flagのような文字列を含む内容が得られた。
この文字列から問題文の指示に従って ' を削除することで、flagが得られた。

Using this program, I determined the input corresponding to flag.txt. The result contained a string that looks like the flag.
I obtained the flag by removing ' from the string as requested in the challenge description.

sdctf{D0nt_b3_a_D4v3_ju5t_Use_AES_0r_S0me7h1ng}

San Diego CTF 2022