4

リバース エンジニアリングの演習の一環として、以下のプログラムを満たすユーザー名とパスワードを見つける Z3 ソルバーを作成しようとしています。誰もが参照している z3py チュートリアル (rise4fun) がダウンしているため、これは特に困難です。

#include <iostream>
#include <string>

using namespace std;

int main() {
    string name, pass;
    cout << "Name: ";
    cin >> name;

    cout << "Pass: ";
    cin >> pass;

    int sum = 0;
    for (size_t i = 0; i < name.size(); i++) {
        char c = name[i];
        if (c < 'A') {
            cout << "Lose: char is less than A" << endl;
            return 1;
        }
        if (c > 'Z') {
            sum += c - 32;
        } else {
            sum += c;
        }
    }
    int r1 = 0x5678 ^ sum;

    int r2 = 0;
    for (size_t i = 0; i < pass.size(); i++) {
        char c = pass[i];
        c -= 48;
        r2 *= 10;
        r2 += c;
    }
    r2 ^= 0x1234;

    cout << "r1: " << r1 << endl;
    cout << "r2: " << r2 << endl;
    if (r1 == r2) {
        cout << "Win" << endl;
    } else {
        cout << "Lose: r1 and r2 don't match" << endl;
    }
}

バイナリのアセンブリからそのコードを取得しました。間違っているかもしれませんが、ソルバーの作成に集中したいと思います。最初の部分から始めて、 を計算するだけですr1。これが私が持っているものです:

from z3 import *

s = Solver()
sum = Int('sum')
name = Array('name', IntSort(), IntSort())
for c in name:
    s.add(c < 65)
    if c > 90:
        sum += c - 32
    else:
        sum += c
r1 = Xor(sum, 0x5678)
print s.check()
print s.model()

私が主張しているのは、配列に「A」未満の文字がないということだけです。そのため、65 より大きい数値を持つ任意のサイズの配列が返されることを期待しています。

主に無限ループであるため、明らかにこれは完全に間違っています。また、合計が 0 に初期化されているかどうかわからないため、合計を正しく計算しているかどうかもわかりません。誰かがこの最初のループを機能させる方法を理解するのを手伝ってくれますか?

編集:上記の C++ コードに近い z3 スクリプトを取得できました。

from z3 import *

s = Solver()
sum = 0
name = Array('name', BitVecSort(32), BitVecSort(32))
i = Int('i')

for i in xrange(0, 1):
    s.add(name[i] >= 65)
    s.add(name[i] < 127)
    if name[i] > 90:
        sum += name[i] - 32
    else:
        sum += name[i]
r1 = sum ^ 0x5678

passwd = Array('passwd', BitVecSort(32), BitVecSort(32))
r2 = 0
for i in xrange(0, 5):
    s.add(passwd[i] < 127)
    s.add(passwd[i] >= 48)
    c = passwd[i] - 48
    r2 *= 10
    r2 += c
r2 ^= 0x1234

s.add(r1 == r2)

print s.check()
print s.model()

このコードにより、正しいユーザー名とパスワードを得ることができました。ただし、ユーザー名には 1、パスワードには 5 の長さをハードコーディングしました。長さをハードコードする必要がないように、スクリプトを変更するにはどうすればよいですか? また、プログラムを実行するたびに異なるソリューションを生成するにはどうすればよいでしょうか?

4

2 に答える 2

3

Z3 の配列には、必ずしも境界があるわけではありません。この場合、インデックス ソートは Int であり、これは無制限の整数 (マシン整数ではない) を意味します。その結果、for c in name列挙されるため、永久に実行されますname[0], name[1], name[2],...

元のプログラム (name.size()) に実際に境界があるように見えるので、その制限まで列挙するだけで十分です。それ以外の場合は、量指定子が必要になる場合があります。たとえば \forall x of Int sort です。name[x] < 65. もちろん、これには量指定子に関するすべての警告が伴います (たとえば、Z3 Guideを参照してください) 。

于 2014-05-19T17:09:43.820 に答える
2

長さを決定するとします。これがあなたができると思うことです：

length = Int('length')
x = Int('x')
s.add(ForAll(x,Implies(And(x>=0,x<length),And(passwd[x] < 127,passwd[x] >=48))))
于 2015-06-22T20:43:56.277 に答える